- Out of the wiki, back into the source.

src/bugs.txt

@@ -0,0 +1,119 @@
+--+++ Crititcal Bugs
+
+   * soph segfaults at no switch or -r4 (-r3 is okay??) using non-debug version.
+   * './scyther -a ../spdl/nsl3.spdl --increment-runs' segfaults. The main reason is that the Archne engine uses runs in a different way.
+     Maybe it is best to disable --increment rules for non-ModelChecker verification.
+
+---+++ Bugs
+
+   * 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. This typically occurs in type flaw searches.
+   * Arachne seems to trip over claims with empty prec sets. Maybe we
+  simply should not test these.
+   * 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!
+  <br>
+  Maybe self-loops are the problem. This has to do with tuple alternation
+  decoding. Consider re-introducing explicit intruder strands OR self-loop
+  pruning.
+
+---+++ Would like to have
+
+---++++ ArachneEngine
+
+   * 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.
+   * 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.
+   * Add switch for arachne to prune encryption levels when using -m2.
+   * 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!
+   * 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.
+
+---++++ ModelChecker
+
+   * For secrecy, one trusted agent and one untrusted agent suffices.
+     Implement this in the modelchecker.
+   * Implement delayed protocol compiler (on run demand only) for the modelchecker?
+
+---++++ Misc
+
+   * 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.
+   * Rewrite termMguTerm such that it iterates and adapt all functions
+     using it. This is to allow for associative tupling later.
+   * 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).
+   * Move initial intruder knowledge maybe into the title of the MSC.
+   * Implement run knowledge, and use this in protocol compiler.
+   * Introduce 'Ticket' default type in the compiler, along with some
+     handling for that.
+   * 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.
+      1. 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.
+   * Woolam-ce gives nothing. But then again, it's a wrong impl.
+   * Global/protocol variables should not exist in the current system.
+   * 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.
+   * 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?
+
+---++++ ConstraintLogic (and thus obsolete)
+
+   * CLP: variables in keys must be branched: maybe even in three situations
+     (have key and contents, have inverse key and content, nothing)
+   * How should claims behave (trusted/untrusted) wrt uninstantiated
+     agents? Branch again? That's what is causing the nsl3-var problem.
+   * 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.
+   * 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.
+