scyther/src/todo.txt

84 lines
4.7 KiB
Plaintext
Raw Normal View History

2004-08-20 09:01:35 +01:00
- Fix 'never sent secrets' list, that are e.g. secret keys of regular agents
and such. The intruder can never learn these, we need this for pruning.
If a goal is such a term, we prune. Note that this results in a complicated
symbolic theorem, probably, with an implication. (sk => sk(untrusted)).
Investigate how this can be incorporated.
- Goal select should favour 'old' goals. Thus, best should be <= comparison,
because the list is appended at the head.
- Make 'generate_trace_bindings' to create the bindings for a given trace.
Note that there can be multiple solutions; for now, simply try to take the
shortest one.
2004-08-18 22:44:30 +01:00
- If there is a limit on the runs for Arachne, but this limit is never
reached, the proof is still complete. The same goes for other bounds. We
thus need a flag to indicate that a state was pruned because of a bound.
Then, we get more possible results for the output.
1. Correct and complete
2. Correct within bounds
3. Incorrect
2004-08-18 21:13:13 +01:00
- Fix term encryption level pruning for arachne, depending on the match type.
- Constraint logic now also has no checks for when a run is done by the
intruder (which should be excluded).
2004-07-12 10:26:25 +01:00
- Fix constants in intruder knowledge. Auto add single one of each type,
when typed expl. Add single constant when untyped. Fix this also in
semantics, and add proof to establish sufficiency.
- Fix function handling (signatures).
- Intruder should at least have one copy of each type that an agent can
construct, I think in any case. Proof needed for single identifier need.
Furthermore reduction if type flaw testing; only one constant needed.
2004-05-24 18:44:30 +01:00
- Make --with-argtabledir= something switch, replacing
README/galious-configure.sh constructs.
2004-05-13 15:59:03 +01:00
- Move initial intruder knowledge maybe into the title of the MSC.
- Implement run knowledge, and use this in protocol compiler.
2004-04-23 11:58:43 +01:00
- Timer output is broken for values e.g. above an hour. Fix or remove
altogether.
- ns3 doesn't even reach a claim in --cl and -t8. Check.
- in Runs.c, revise 'untrustedAgent' to cope with some weird exceptions.
- CLP: variables in keys must be branched: maybe even in three situations
(have key and contents, have inverse key and content, nothing)
- Implement delayed protocol compiler (on run demand only).
- Remove any remaining global variables, if any.
- Introduce 'Ticket' default type in the compiler, along with some
handling for that.
- How should claims behave (trusted/untrusted) wrt uninstantiated
agents? Branch again? That's what is causing the nsl3-var problem.
- The 'choose' operator must always be typed, I think.
- The woolam-ce is incorrect because it is illegal to have a variable
term in a key that is read, by CMV semantics. I don't know what it
means for CE semantics (yet).
- Idea: run bla.bla(params) [compromised <localterm> [,<localterm>] ];
1. These local terms are given to the intruder. Technically this
should only happen _after_ they are first sent in the run. Maybe add
this to send semantics: if termOccurs(sendterm, compromisedterm) then
add compromisedterm to M, remove compromisedterm from list of terms to
compromise.
2. All claims in the run are ignored (add untrusted flag to run)
Alternative: run x.x(x) untrusted; or just compromised, to give up
all constants.
Note this is not sufficient yet, because it does not consider any
partner runs. Maybe declare a 'compromised' section first; other runs
will only activate after these have completed. Note this is much more
expensive.
- Issue: how do untrusted claims work in the context of an intruder?
Claim must be checked if it can be solved such that at least one of
the agents is trusted.
- Woolam-ce gives nothing. But then again, it's a wrong impl.
- -m2 is much better with a lot of variables. Compare this to unfolding
of the runs with -t4 -m0/1.
- Global/protocol variables should not exist in the current system.
- Solve the 'version' issue. How is it defined?
- run nsl.initiator(alice, all Agent) constructs?
- 'all' would generate the roles with the corresponding type.
- or maybe for clarity/complexity control: use 'runs' for constructs
with 'all' in it.
- Constraints might be a part of a knowledge thing, because with we
might now have a number of local knowledge sets, each with their own
constraint sets. That doesn't make it easier though :( and will cause
some performance loss I suppose. Each local set has to remain
solveable as well.
- Maybe function application ought to be a different basic term type.
- After role construction, msc consistency can be checked.
- Reduce knowledge to a simple term list? That would simplify a number
of things, and also allow for easier addition of stuff.
- How is % notation handled in Casper?
- Vernam encryption?