From 351d61932480e91bd094fb578a5d3c926cef60b6 Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 25 Feb 2005 14:54:28 +0000 Subject: [PATCH] - Out of the wiki, back into the source. --- src/bugs.txt | 119 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 119 insertions(+) create mode 100644 src/bugs.txt diff --git a/src/bugs.txt b/src/bugs.txt new file mode 100644 index 0000000..98e77b0 --- /dev/null +++ b/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! +
+ 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 [,] ]; + 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. +