Merge branch 'Todo'

This commit is contained in:
Cas Cremers 2007-09-18 16:09:05 +02:00
commit b013440c8b

View File

@ -1,72 +0,0 @@
- When saving a file after 'file changed' warning, an overwrite of the
same file should not necessarily generate a warning.
- Output (claim summary) might have a parameter summary somewhere.
- Error should have an additional line number parameter (that might be
-1 to ignore it) forcing people to use numbers :)
Format: "error: [%i] %s\n"
- Nested functions should be avoided: their implementation requires an
executable stack, which is bad for security purposes. However, many of
the iterator functions need to pass a function and possibly some
variables. Currently, the variables are handled by the nested function
mechanism (the iterated nested function and address variables of the
function it is part of), which would not work anymore. A possible
solution seems variable argument count functions, but this is fairly
cumbersome and might impact on performance. Alternatively, iterators
can be implemented as macros, which is probably the fastest, but maybe
less readable.
- The (currently not advised) switch --check is slightly off because
there is no good semantics for the --disable intruder check. As a
result, it is now too strict can cause correct protocols to fail. Fix.
- When *not* asking for attack output, maybe we should default to
--prune = 1. Then, if we ask for --xml output or --dot, we do:
if --prune == 1 then --prune == 2 now :) unless otherwise specified.
(This should be done after switch checking)
- Old version enforced some extra orders:
1. M_0 roles were ordered before any other roles.
2. Local constants order: if a run has a local variable instantiated by
somebody else's variable, that should occur then after the initial sending
of that value...
- Test 'sk(x)' in goals, somewhere before assessing a state (dus at the
beginning of iterate), immediately reduce to 'sk(Eve)'. Test with
--experimental. To that end, reintroduce a state-reporting switch.
- It is currently not well-defined to define inversekeys within a role:
this requires some work at instantiation, because instantiated term
couples should be added to the inverses list, and removed at
descruction.
- Simple timestamps could be added by prefixing send message before the
role, sending any timestamp constants out first to the intruder. These
should of course be hidden in the output somehow.
- Notes on the new attack group displays:
* We want to group runs into consistent protocol runs.
* Minimal req. for protocol run: equal \rho.
* If two runs are candidates for a role in a protocol run,
use a metric based on order and data. Maybe data is more important:
if equal data, than order might be irrelevant.
* Maybe we should refactor the xmlOut code first. In an extreme case,
we first factor out all logic, and ranking, and grouping, in to a
prepareAttackOutput structure; with a separate source file. Later we
can convert this to either ASCII or DOT or XML or something.
Now that I think of it; XML should be a plain state probably, and we
could add a switch to also output more detailed attack things (is
that relevant?)
- SConstruct file should check whether ctags actually exists (avoiding
errors)
- Proof output should be XML, with an external converter to dot format.
- Are the Arachne rules for keys that are variables sufficiently sane in
general? E.g. what is their inverse key? Intuition: one cannot know
what the inverse is of a non-instantiated key variable, given the
current semantics, if asymmetric keys are allowed. Consequence: the
current implementation is just fine, because asymmetric key variables
cannot be defined in the language. Thus, the rules are fine.
Investigate for future extensions what the consequences of this are.
- 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.
- knowledgeAddTerm might be improved by scanning through key list only with
things that are newly added.