diff --git a/src/notes.txt b/src/notes.txt index fbf97fa..1c25e55 100644 --- a/src/notes.txt +++ b/src/notes.txt @@ -1,3 +1,7 @@ +- De-classification does not work as desired. The name Alice is used + even if it already occurs somehwere in the system, which is not what + we want. +- Heuristic could also punish more initiators. - If no attack/state output is needed, maybe the attack heuristic should be simpler (which means just weighting the trace length etc.) in order to avoid uneccesary continuation of the search. Maybe even stop diff --git a/src/prune_theorems.c b/src/prune_theorems.c index 25b6df7..9d28782 100644 --- a/src/prune_theorems.c +++ b/src/prune_theorems.c @@ -410,6 +410,15 @@ prune_theorems (const System sys) } } + // To be on the safe side, we currently limit the encryption level to two. This is not a problem for known attacks, but should be addressed more carefully at some point. + /** + * @todo Fix untyped variables reasoning + */ + if (term_encryption_level (b->term) > 2) + { + return true; + } + /** * Prune on the basis of hidelevel lemma */ diff --git a/src/system.c b/src/system.c index f72589e..dedf3f7 100644 --- a/src/system.c +++ b/src/system.c @@ -1426,6 +1426,7 @@ selfSession (const System sys, const int run) { // This agent was already in the seen list self_session = true; + break; } else { @@ -1466,7 +1467,7 @@ selfResponders (const System sys) run = 0; while (run < sys->maxruns) { - if (selfInitiator (sys, run)) + if (selfResponder (sys, run)) { count++; }