53 lines
3.1 KiB
Plaintext
53 lines
3.1 KiB
Plaintext
- 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.
|
|
- I've started on sanitizing the --max-attacks switch. It now prunes as a
|
|
bound, but it also needs to limit per-claim, I guess.
|
|
- There is something weird when automatically generating claim labels
|
|
and trying to filter on them (try eg duplicates)
|
|
- --check is slightly f***ed up 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.
|