andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fix the protocol name in denning-sacco-lowe

Browse Source
This commit is contained in:
gijs 2005-05-10 14:08:51 +00:00
parent 934eb3fd2a
commit 0930556f2e
1 changed files with 7 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
spdl/SPORE/denning-sacco-lowe.spdl
View File

@ -19,7 +19,7 @@ secret k: Function;
usertype PseudoFunction; usertype PseudoFunction;
const dec: PseudoFunction; const dec: PseudoFunction;
protocol denningSacco(I,R,S) protocol denningSaccoLowe(I,R,S)
{ {
role I role I
{ {
@ -72,9 +72,9 @@ compromised k(Eve,Simon);
# Note because the modelchecker does not support tickets this might not # Note because the modelchecker does not support tickets this might not
# be very useful # be very useful
run denningSacco.I(Agent,Agent,Simon); run denningSaccoLowe.I(Agent,Agent,Simon);
run denningSacco.R(Agent,Agent,Simon); run denningSaccoLowe.R(Agent,Agent,Simon);
run denningSacco.S(Agent,Agent,Simon); run denningSaccoLowe.S(Agent,Agent,Simon);
run denningSacco.I(Agent,Agent,Simon); run denningSaccoLowe.I(Agent,Agent,Simon);
run denningSacco.R(Agent,Agent,Simon); run denningSaccoLowe.R(Agent,Agent,Simon);
run denningSacco.S(Agent,Agent,Simon); run denningSaccoLowe.S(Agent,Agent,Simon);