This commit is contained in:
Cas Cremers 2007-10-22 21:14:06 +02:00
parent 6e65138dca
commit a6370726ef
2 changed files with 0 additions and 78 deletions

View File

@ -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)

View File

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