4d7b744e1b
errors with --extravert: even if Alice is already occurring in the system, the name can be used. - Added explicit level 2 encryption bound. This is technically incorrect, but for now it should work.
54 lines
3.3 KiB
Plaintext
54 lines
3.3 KiB
Plaintext
- De-classification does not work as desired. The name Alice is used
|
|
even if it already occurs somehwere in the system, which is not what
|
|
we want.
|
|
- Heuristic could also punish more initiators.
|
|
- If no attack/state output is needed, maybe the attack heuristic should
|
|
be simpler (which means just weighting the trace length etc.) in order
|
|
to avoid uneccesary continuation of the search. Maybe even stop
|
|
altogether after finding *an* attack.
|
|
- For the TimeStamps etc, we can implement an 'auto-leak' of such local
|
|
constants. This should works also with a modifier of sorts (e.g.
|
|
'predictable') and such constants should be leaked to the intruder at
|
|
the start of the run, possibly by prefixing a send.
|
|
- The trace incremental search should start at something like 'distance of
|
|
first claim + SOMECONST * runs'. SOMECONST relates to the partial-order
|
|
induced trace prolonings.
|
|
- For now, CLP is non-working and not checked. Reconsider this later.
|
|
- Because the properties checked are related to the partial order reductions,
|
|
it makes sense to check 'all secrecy claims' or 'all synchronisation claims'
|
|
at once.
|
|
- Given originator assumptions and such, we might want to implement the
|
|
compiler, that for non-typed matching, it will ignore all type definitions
|
|
in the code (as in, putting them in stype, but still considering Function).
|
|
Then, for 'any agent' we can use stype silently. The modelchecker should
|
|
then always consider the types with -m0 and -m1.
|
|
- In a paper concerning the CASRUL compiler, they mention associativity for
|
|
the equality relations. Note that CASRUL restricts the intruder actions,
|
|
and sometimes uses approximations.
|
|
- MS and CE never mention associativity as a restriction.
|
|
- For now, clp stuff will use pairing and simple mgu. Maybe a -m3 switch will
|
|
add the associative variant later.
|
|
- MALLOC_TRACE is the environment variable that triggers mtrace() output.
|
|
- Several memory leak detectors are still in place, they can all be located by
|
|
searching for "lead" or "diff" and destroying the code.
|
|
- knowledgeAddTerm might be improved by scanning through key list only with
|
|
things that are newly added.
|
|
- Associativity and unification don't play together well; consider other
|
|
algorithms. Maybe a simple explore (x,y),z and explore x,(y,z) will do, e.g.
|
|
take any split point for both sequences.
|
|
- POR (-t3) is actually worse than -t2: sends first. After some pondering I
|
|
now know why. It's because simultaneous reads yield traces in which there
|
|
are attacks that are also in the ones where we have R0S0S0;R1 (i.e. is thus
|
|
equivalent with R0;R1;S0S0)
|
|
- Knowledge is monotonous. So, if we say 'R#0' cannot be triggered by some
|
|
knowledge, we can just use a pointer for it. If we do want to trigger it, we
|
|
need to compare two knowledge pointers. As they don't have a unique
|
|
representation, it is more difficult. For now, I will just forbid specific
|
|
branches of the read when a message is in some previous knowledge, which is
|
|
more precise.
|
|
- Comparisons with Casper are in order.
|
|
- It is a good idea to have any number of input files, and parse them all, to
|
|
combine scenarios. A command should be "require <file>", because that would
|
|
enable scenarios to load the required role definitions. It's require instead
|
|
of include, because of possible multiple occurrences.
|