diff --git a/src/design.txt b/src/design.txt deleted file mode 100644 index 97c40bb..0000000 --- a/src/design.txt +++ /dev/null @@ -1,47 +0,0 @@ -Design Issues for the Model Checker ------------------------------------ - -- For secrecy, we can trigger all sends at once. For synchronisation, - this is not the case. - -- Modules have to be split up sensibly. - - - Although 'knowledge' and 'term matching' seem to different items, - their intertwined workings suggest that they should be implemented - in parallel. - - - State generation (as in creating instances) might already allow for - a lot of static analysis. - -- We should make a list of required operations. Ingmar's work can serve - as a starting point. - -- For now, there will be no parser, and test cases will be input by - hand. - -- Synchronisation is more difficult to test, so we focus on secrecy - first. I've got some good ideas on Synchronisation testing though - (with narrowing sets of possible partners). Synchronisation is very - hard to prune, I presume. I have to prove that though ;) - -Sketch for secrecy: - -SimulateStep(F,M,constraints): - if Empty(F): - return - else: - for (s in PossibleSends): - add s.message to M - if (secrecy violated): - halt - remove s from F - ReadSets = supersetTransitions(F) - for (ReadSet in ReadSets): - for (s in ReadSet): - // dit is vaag - if NonMatch goto next ReadSet - constraint = F,M,match() - SimulateStep(F \ s,M,constraints) - - - diff --git a/src/hidelevel.txt b/src/hidelevel.txt deleted file mode 100644 index e547450..0000000 --- a/src/hidelevel.txt +++ /dev/null @@ -1,31 +0,0 @@ -Implemented: - -- scans -- test functions (in hidelevel.c) - -TODO: - -- use test functions (impossible for pruning, interesting for goal selection heuristic) -- state count display switch for comparisons -- consider adding info for goal stuff (only from M_0, not by create) - -******************************************************************* - -roivas:~scyther% ./scyther ccitt509-1c.spdl -Global constants: [te, ne, Eve, Bob, Alice, unhash, sk, hash, pk] - -Possibly interesting term: unhash; know 2147483647, prot 2147483647 -Possibly interesting term: sk; know 1, prot 2 - - -roivas:~scyther% ./scyther yahalom.spdl -warning: variable T was declared in role yahalom,R but never used in a read event. -Global constants: [Simon, Bob, Alice, Compromised, Fresh, k] - -Possibly interesting term: k; know 2147483647, prot 2 - - -roivas:~scyther% ./scyther ns3.spdl -Global constants: [Eve, sk, pk] - -Possibly interesting term: sk; know 1, prot 2147483647