- Todo list is now handled by the wiki:

http://www.win.tue.nl/~ccremers/twiki/bin/view.pl/Scyther/ScytherBug

src/todo.txt

@@ -1,120 +0,0 @@
-- Arachne AgentOfRun is playing up. Investigate start diamonds, and then
-  reinstate the untrusted actor pruning theorem. Probably the cause is in the
-  new roleInstance. Signals of this should be in a correct impl. of
-  agentOfRun.
-- Add some bug tracking thing to all this, because this list is becoming too
-  big.
-- PRIO 1 : fix Arachne Dot output. Start by having dot-comments with the
-  actual bindings list, to debug the stuff that happens.
-- PRIO 2 : resolve Arachne memory usage issue. Why is it using so much memory?
-  Recode stuff to memAlloc/memFree and determine max usage, leakage etc.
-- There is no good test on the correct workings of
-  add_goals/destruction of these. We can test this if after
-  termination, we have 0 goals; for this we need to store the
-  initially added goals as well. Furthermore, we can generate an
-  error when <0 goals occur.
-- Arachne seems to trip over claims with empty prec sets. Maybe we
-  simply should not test these.
-- soph segfaults at no switch or -r4 (-r3 is okay??) using non-debug version.
-- Splice/AS does not work well because priority key search stumbles over the
-  public key search stuff. That is a flaw in the heuristic: we should not look
-  for anything that is in the intruder knowledge already. In fact, it is a
-  problem with branching. We should not look for PK(X), even if X is a
-  variable. Priority should go to keys of which the constructor is not in M_0,
-  maybe that heuristic works.
-  However, there seems to be an infinite loop for this in the algorithm, which
-  I did not anticipate. Investigate!
-  *** Maybe self-loops are the problem. This has to do with tuple alternation
-  decoding. Consider re-introducing explicit intruder strands OR self-loop
-  pruning.
-- Make different error codes for compilation error/ other error. This can be
-  useful for scripts. However, it might shift some constants for the Elegast
-  scripts.
-- Consider where in Arachne dependency graph is used. If this is only for
-  pruning states, we can construct it there only. However, the base 'role
-  defs/bindings' graph might be re-used.
-- Problem with goal bindings: instantiation of variable with a tuple might
-  introduce a tuple goal, which is forbidden. We must find a way to deal with this.
-- For secrecy, one trusted agent and one untrusted agent suffices.
-  Implement this in the modelchecker.
-- Rewrite for untrusted roles, redesign this.
-- Add switch for arachne to prune encryption levels when using -m2.
-- Rewrite termMguTerm such that it iterates and adapt all functions
-  using it. This is to allow for associative tupling later.
-- valgrind -a; key level scanning memory leaks
-- Maybe a singular, preset M_0 sending node. Test for performance issues.
-- To store attacks for arachne, maybe the following is needed:
-  - The roles for each run
-  - The variable bindings for all (local) variables
-  - The goal bindings
-- Agent terms must have keylevel 0; enforce this!
-- './scyther -a ../spdl/nsl3.spdl --increment-runs' segfaults.
-- Select_goal should consider, for singular variables, whether their
-  type can be found in M_0. If so, the goal can be ignored.
-- 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. Investigate how this can be incorporated.
-  Investigate also whether this actually makes a difference.
-- 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.
-- 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).
-- Make --with-argtabledir= something switch, replacing
-  README/galious-configure.sh constructs.
-- Move initial intruder knowledge maybe into the title of the MSC.
-- Implement run knowledge, and use this in protocol compiler.
-- 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. Yes.
-- 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?