- 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?