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

More 'read'->'recv' conversion.

Browse Source
This commit is contained in:
Cas Cremers 2012-04-26 16:40:01 +02:00
parent 3a6d65463f
commit d713ac400d
80 changed files with 384 additions and 384 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
gui/Protocols/MultiProtocolAttacks/BKE.spdl
View File

@ -15,7 +15,7 @@ protocol bke(I,R)
var kir: SessionKey; var kir: SessionKey;
send_1 (I,R, { ni,I }pk(R) ); send_1 (I,R, { ni,I }pk(R) );
read_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); recv_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
send_3 (I,R, { hash(nr) }kir ); send_3 (I,R, { hash(nr) }kir );
claim_4 (I, Secret, kir ); claim_4 (I, Secret, kir );
//claim_5 (I, Niagree ); //claim_5 (I, Niagree );
@ -28,9 +28,9 @@ protocol bke(I,R)
fresh nr: Nonce; fresh nr: Nonce;
fresh kir: SessionKey; fresh kir: SessionKey;
read_1 (I,R, { ni,I }pk(R) ); recv_1 (I,R, { ni,I }pk(R) );
send_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); send_2 (R,I, { hash(ni),nr,R,kir }pk(I) );
read_3 (I,R, { hash(nr) }kir ); recv_3 (I,R, { hash(nr) }kir );
claim_7 (R, Secret, kir ); claim_7 (R, Secret, kir );
//claim_8 (R, Niagree ); //claim_8 (R, Niagree );
//claim_9 (R, Nisynch ); //claim_9 (R, Nisynch );

12
gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl
View File

@ -10,7 +10,7 @@
# a given term crypted with k(I,R) with k(R,I) # a given term crypted with k(I,R) with k(R,I)
# #
# Note: # Note:
# Read 4 by the Initatior has been placed after the synchronisation claim # Recv 4 by the Initatior has been placed after the synchronisation claim
# as it allows trivial synchronisation attacks otherwise (the message is # as it allows trivial synchronisation attacks otherwise (the message is
# completely fresh and can therefore always be replaced by an arbitrary value # completely fresh and can therefore always be replaced by an arbitrary value
# created by the intruder) which are not considered in SPORE # created by the intruder) which are not considered in SPORE
@ -26,7 +26,7 @@ protocol @swapkey(X)
{ {
var I,R: Agent; var I,R: Agent;
var T:Ticket; var T:Ticket;
read_!X1(X,X,I,R,{T}k(I,R)); recv_!X1(X,X,I,R,{T}k(I,R));
send_!X2(X,X,{T}k(R,I)); send_!X2(X,X,{T}k(R,I));
} }
} }
@ -41,12 +41,12 @@ protocol andrew-Concrete(I,R)
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,ni ); send_1(I,R, I,ni );
read_2(R,I, {ni,kir}k(I,R) ); recv_2(R,I, {ni,kir}k(I,R) );
send_3(I,R, {ni}kir); send_3(I,R, {ni}kir);
claim_I1(I,Secret,kir); claim_I1(I,Secret,kir);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
claim_I3(I,Empty,(Fresh,kir)); claim_I3(I,Empty,(Fresh,kir));
read_6(R,I, nr); recv_6(R,I, nr);
} }
role R role R
@ -55,9 +55,9 @@ protocol andrew-Concrete(I,R)
fresh nr: Nonce; fresh nr: Nonce;
fresh kir: SessionKey; fresh kir: SessionKey;
read_1(I,R, I,ni ); recv_1(I,R, I,ni );
send_2(R,I, {ni,kir}k(I,R) ); send_2(R,I, {ni,kir}k(I,R) );
read_3(I,R, {ni}kir); recv_3(I,R, {ni}kir);
send_6(R,I, nr); send_6(R,I, nr);
claim_R1(R,Secret,kir); claim_R1(R,Secret,kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);

8
gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl
View File

@ -24,9 +24,9 @@ protocol andrew-Ban(I,R)
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,{ni}k(I,R) ); send_1(I,R, I,{ni}k(I,R) );
read_2(R,I, {ni,nr}k(I,R) ); recv_2(R,I, {ni,nr}k(I,R) );
send_3(I,R, {nr}k(I,R) ); send_3(I,R, {nr}k(I,R) );
read_4(R,I, {kir,nr2,ni}k(I,R) ); recv_4(R,I, {kir,nr2,ni}k(I,R) );
claim_I1(I,Nisynch); claim_I1(I,Nisynch);
claim_I2(I,Niagree); claim_I2(I,Niagree);
claim_I3(I,Secret, kir); claim_I3(I,Secret, kir);
@ -39,9 +39,9 @@ protocol andrew-Ban(I,R)
fresh nr,nr2: Nonce; fresh nr,nr2: Nonce;
fresh kir: SessionKey; fresh kir: SessionKey;
read_1(I,R, I,{ni}k(I,R) ); recv_1(I,R, I,{ni}k(I,R) );
send_2(R,I, {ni,nr}k(I,R) ); send_2(R,I, {ni,nr}k(I,R) );
read_3(I,R, {nr}k(I,R) ); recv_3(I,R, {nr}k(I,R) );
send_4(R,I, {kir,nr2,ni}k(I,R) ); send_4(R,I, {kir,nr2,ni}k(I,R) );
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
claim_R2(R,Niagree); claim_R2(R,Niagree);

10
gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl
View File

@ -9,7 +9,7 @@
# So it is possile that certain attacks that use this property are not found # So it is possile that certain attacks that use this property are not found
# #
# Note: # Note:
# Read 4 by the Initatior has been placed after the synchronisation claim # Recv 4 by the Initatior has been placed after the synchronisation claim
# as it allows trivial synchronisation attacks otherwise (the message is # as it allows trivial synchronisation attacks otherwise (the message is
# completely fresh and can therefore always be replaced by an arbitrary value # completely fresh and can therefore always be replaced by an arbitrary value
# created by the intruder) which are not considered in SPORE # created by the intruder) which are not considered in SPORE
@ -31,12 +31,12 @@ protocol andrew-LoweBan(I,R)
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,ni ); send_1(I,R, I,ni );
read_2(R,I, {ni,kir,R}k(I,R) ); recv_2(R,I, {ni,kir,R}k(I,R) );
send_3(I,R, {ni}kir ); send_3(I,R, {ni}kir );
claim_I1(I,Nisynch); claim_I1(I,Nisynch);
claim_I2(I,Secret, kir); claim_I2(I,Secret, kir);
claim_I3(I,Empty, (Fresh,kir)); claim_I3(I,Empty, (Fresh,kir));
read_4(R,I, nr ); recv_4(R,I, nr );
} }
role R role R
@ -45,9 +45,9 @@ protocol andrew-LoweBan(I,R)
fresh nr: Nonce; fresh nr: Nonce;
fresh kir: SessionKey; fresh kir: SessionKey;
read_1(I,R, I,ni ); recv_1(I,R, I,ni );
send_2(R,I, {ni,kir,R}k(I,R) ); send_2(R,I, {ni,kir,R}k(I,R) );
read_3(I,R, {ni}kir ); recv_3(I,R, {ni}kir );
send_4(R,I, nr ); send_4(R,I, nr );
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
claim_R2(R,Secret, kir); claim_R2(R,Secret, kir);

8
gui/Protocols/MultiProtocolAttacks/boyd.spdl
View File

@ -25,7 +25,7 @@ protocol boyd(I,R,S)
var ks: Macseed; var ks: Macseed;
send_1 (I,S, I,R, ni ); send_1 (I,S, I,R, ni );
read_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr ); recv_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr );
send_4 (I,R, m(nr, m(ks,ni,nr)) ); send_4 (I,R, m(nr, m(ks,ni,nr)) );
claim_6 (I, Secret, m(ks,ni,nr) ); claim_6 (I, Secret, m(ks,ni,nr) );
@ -37,9 +37,9 @@ protocol boyd(I,R,S)
fresh nr: Nonce; fresh nr: Nonce;
var ks: Macseed; var ks: Macseed;
read_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni ); recv_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni );
send_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr ); send_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr );
read_4 (I,R, m(nr, m(ks,ni,nr)) ); recv_4 (I,R, m(nr, m(ks,ni,nr)) );
claim_10 (R, Secret, m(ks,ni,nr)); claim_10 (R, Secret, m(ks,ni,nr));
} }
@ -49,7 +49,7 @@ protocol boyd(I,R,S)
var ni,nr: Nonce; var ni,nr: Nonce;
fresh ks: Macseed; fresh ks: Macseed;
read_1 (I,S, I,R, ni ); recv_1 (I,S, I,R, ni );
send_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni ); send_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni );
} }
} }

6
gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl
View File

@ -19,7 +19,7 @@ protocol ccitt509-ban3(I,R)
var Xb,Nb,Yb: Nonce; var Xb,Nb,Yb: Nonce;
send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
read_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); recv_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
send_3(I,R, I,{R, Nb}sk(I)); send_3(I,R, I,{R, Nb}sk(I));
claim_4(I,Nisynch); claim_4(I,Nisynch);
} }
@ -29,9 +29,9 @@ protocol ccitt509-ban3(I,R)
var Na,Xa,Ya: Nonce; var Na,Xa,Ya: Nonce;
fresh Xb,Yb,Nb: Nonce; fresh Xb,Yb,Nb: Nonce;
read_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); recv_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
send_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); send_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
read_3(I,R, I,{R, Nb}sk(I)); recv_3(I,R, I,{R, Nb}sk(I));
claim_5(R,Nisynch); claim_5(R,Nisynch);
# There should also be Fresh Xa and Fresh Ya claims here # There should also be Fresh Xa and Fresh Ya claims here
} }

10
gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl
View File

@ -26,9 +26,9 @@ protocol denningSacco-Lowe(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,S, I,R ); send_1(I,S, I,R );
read_2(S,I, {R, Kir, T, W}k(I,S) ); recv_2(S,I, {R, Kir, T, W}k(I,S) );
send_3(I,R, W); send_3(I,R, W);
read_4(R,I, {Nr}Kir); recv_4(R,I, {Nr}Kir);
send_5(I,R, {{Nr}dec}Kir); send_5(I,R, {{Nr}dec}Kir);
claim_I1(I,Niagree); claim_I1(I,Niagree);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
@ -42,9 +42,9 @@ protocol denningSacco-Lowe(I,R,S)
var T: TimeStamp; var T: TimeStamp;
fresh Nr: Nonce; fresh Nr: Nonce;
read_3(I,R, {Kir,I,T}k(R,S)); recv_3(I,R, {Kir,I,T}k(R,S));
send_4(R,I, {Nr}Kir); send_4(R,I, {Nr}Kir);
read_5(I,R, {{Nr}dec}Kir); recv_5(I,R, {{Nr}dec}Kir);
claim_R1(R,Niagree); claim_R1(R,Niagree);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
claim_R3(R,Secret,Kir); claim_R3(R,Secret,Kir);
@ -57,7 +57,7 @@ protocol denningSacco-Lowe(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
fresh T: TimeStamp; fresh T: TimeStamp;
read_1(I,S, I,R ); recv_1(I,S, I,R );
send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
claim_x(S, Secret, Kir); claim_x(S, Secret, Kir);
} }

6
gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl
View File

@ -20,7 +20,7 @@ protocol denningSacco(I,R,S)
var T: TimeStamp; var T: TimeStamp;
send_1(I,S, I,R ); send_1(I,S, I,R );
read_2(S,I, {R, Kir, T, W}k(I,S) ); recv_2(S,I, {R, Kir, T, W}k(I,S) );
send_3(I,R, W); send_3(I,R, W);
claim_I1(I,Niagree); claim_I1(I,Niagree);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
@ -33,7 +33,7 @@ protocol denningSacco(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
var T: TimeStamp; var T: TimeStamp;
read_3(I,R, {Kir,I,T}k(R,S)); recv_3(I,R, {Kir,I,T}k(R,S));
claim_R1(R,Niagree); claim_R1(R,Niagree);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
claim_R3(R,Secret,Kir); claim_R3(R,Secret,Kir);
@ -46,7 +46,7 @@ protocol denningSacco(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
fresh T: TimeStamp; fresh T: TimeStamp;
read_1(I,S, I,R ); recv_1(I,S, I,R );
send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
} }
} }

10
gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl
View File

@ -19,7 +19,7 @@ protocol gongnonceb(I,R,S)
var kr: Keypart; var kr: Keypart;
send_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni ); send_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni );
read_4 (S,I, { S,I,R,kr,I }k(I,S), { R,I,ni }f(ki,kr), nr ); recv_4 (S,I, { S,I,R,kr,I }k(I,S), { R,I,ni }f(ki,kr), nr );
send_5 (I,R, { I,R,nr }f(ki,kr) ); send_5 (I,R, { I,R,nr }f(ki,kr) );
claim_6 (I, Secret, ki); claim_6 (I, Secret, ki);
@ -35,9 +35,9 @@ protocol gongnonceb(I,R,S)
fresh kr: Keypart; fresh kr: Keypart;
var ki: Keypart; var ki: Keypart;
read_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni ); recv_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni );
send_3 (R,S, { R,S,R,kr,I }k(R,S), { R,I, ni }f(ki,kr), nr ); send_3 (R,S, { R,S,R,kr,I }k(R,S), { R,I, ni }f(ki,kr), nr );
read_5 (I,R, { I,R,nr }f(ki,kr) ); recv_5 (I,R, { I,R,nr }f(ki,kr) );
claim_10 (R, Secret, ki); claim_10 (R, Secret, ki);
claim_11 (R, Secret, kr); claim_11 (R, Secret, kr);
@ -51,9 +51,9 @@ protocol gongnonceb(I,R,S)
var ki,kr: Keypart; var ki,kr: Keypart;
var T; var T;
read_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni ); recv_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni );
send_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni ); send_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni );
read_3 (R,S, { R,S,R,kr,I }k(R,S), T, nr ); recv_3 (R,S, { R,S,R,kr,I }k(R,S), T, nr );
send_4 (S,I, { S,I,R,kr,I }k(I,S), T, nr ); send_4 (S,I, { S,I,R,kr,I }k(I,S), T, nr );
} }
} }

10
gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl
View File

@ -17,7 +17,7 @@ protocol gongnonce(I,R,S)
var kr: Keypart; var kr: Keypart;
send_1 (I,R, I,R,ni ); send_1 (I,R, I,R,ni );
read_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr); recv_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr);
send_4 (I,S, { I,S,I, ki, R, nr }k(I,S) ); send_4 (I,S, { I,S,I, ki, R, nr }k(I,S) );
claim_6 (I, Secret, ki); claim_6 (I, Secret, ki);
@ -33,9 +33,9 @@ protocol gongnonce(I,R,S)
fresh kr: Keypart; fresh kr: Keypart;
var ki: Keypart; var ki: Keypart;
read_1 (I,R, I,R,ni ); recv_1 (I,R, I,R,ni );
send_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S)); send_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S));
read_5 (S,R, { S,R,I, ki, R, nr }k(R,S) ); recv_5 (S,R, { S,R,I, ki, R, nr }k(R,S) );
claim_10 (R, Secret, ki); claim_10 (R, Secret, ki);
claim_11 (R, Secret, kr); claim_11 (R, Secret, kr);
@ -48,9 +48,9 @@ protocol gongnonce(I,R,S)
var ni,nr: Nonce; var ni,nr: Nonce;
var ki,kr: Keypart; var ki,kr: Keypart;
read_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S)); recv_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S));
send_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr); send_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr);
read_4 (I,S, { I,S,I, ki, R, nr }k(I,S) ); recv_4 (I,S, { I,S,I, ki, R, nr }k(I,S) );
send_5 (S,R, { S,R,I, ki, R, nr }k(R,S) ); send_5 (S,R, { S,R,I, ki, R, nr }k(R,S) );
} }
} }

8
gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl
View File

@ -10,7 +10,7 @@ protocol isoiec11770213(I,R,S)
var kir: Sessionkey; var kir: Sessionkey;
send_1 (I,R, ni); send_1 (I,R, ni);
read_4 (R,I, { ni,kir,R }k(I,S) ); recv_4 (R,I, { ni,kir,R }k(I,S) );
claim_5 (I, Secret, kir); claim_5 (I, Secret, kir);
} }
@ -22,9 +22,9 @@ protocol isoiec11770213(I,R,S)
fresh kir: Sessionkey; fresh kir: Sessionkey;
var T; var T;
read_1 (I,R, ni); recv_1 (I,R, ni);
send_2 (R,S, { nr,ni,I,kir }k(R,S) ); send_2 (R,S, { nr,ni,I,kir }k(R,S) );
read_3 (S,R, { nr, I }k(R,S), T ); recv_3 (S,R, { nr, I }k(R,S), T );
send_4 (R,I, T ); send_4 (R,I, T );
claim_6 (R, Secret, kir); claim_6 (R, Secret, kir);
@ -35,7 +35,7 @@ protocol isoiec11770213(I,R,S)
var ni,nr: Nonce; var ni,nr: Nonce;
var kir: Sessionkey; var kir: Sessionkey;
read_2 (R,S, { nr,ni,I,kir }k(R,S) ); recv_2 (R,S, { nr,ni,I,kir }k(R,S) );
send_3 (S,R, { nr, I }k(R,S), { ni,kir,R }k(I,S) ); send_3 (S,R, { nr, I }k(R,S), { ni,kir,R }k(I,S) );
} }
} }

8
gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl
View File

@ -17,7 +17,7 @@ protocol kaochow-2(I,R,S)
var kir,kt: SessionKey; var kir,kt: SessionKey;
send_1 (I,S, I,R,ni); send_1 (I,S, I,R,ni);
read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr ); recv_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
send_4 (I,R, {nr,kir}kt ); send_4 (I,R, {nr,kir}kt );
claim_I1 (I, Nisynch); claim_I1 (I, Nisynch);
@ -33,9 +33,9 @@ protocol kaochow-2(I,R,S)
var kir,kt: SessionKey; var kir,kt: SessionKey;
var T: Ticket; var T: Ticket;
read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); recv_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) );
send_3 (R,I, R, T, {ni, kir}kt, nr ); send_3 (R,I, R, T, {ni, kir}kt, nr );
read_4 (I,R, {nr,kir}kt ); recv_4 (I,R, {nr,kir}kt );
claim_R1 (R, Nisynch); claim_R1 (R, Nisynch);
claim_R2 (R, Niagree); claim_R2 (R, Niagree);
@ -48,7 +48,7 @@ protocol kaochow-2(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh kir, kt: SessionKey; fresh kir, kt: SessionKey;
read_1 (I,S, I,R,ni); recv_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) );
} }
} }

8
gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl
View File

@ -20,7 +20,7 @@ protocol kaochow-3(I,R,S)
var T2: Ticket; var T2: Ticket;
send_1 (I,S, I,R,ni); send_1 (I,S, I,R,ni);
read_3 (R,I, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); recv_3 (R,I, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
send_4 (I,R, {nr,kir}kt, T2 ); send_4 (I,R, {nr,kir}kt, T2 );
claim_I1 (I, Nisynch); claim_I1 (I, Nisynch);
@ -37,9 +37,9 @@ protocol kaochow-3(I,R,S)
var T: Ticket; var T: Ticket;
fresh tr: TimeStamp; fresh tr: TimeStamp;
read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); recv_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) );
send_3 (R,I, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); send_3 (R,I, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) ); recv_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) );
claim_R1 (R, Nisynch); claim_R1 (R, Nisynch);
claim_R2 (R, Niagree); claim_R2 (R, Niagree);
@ -52,7 +52,7 @@ protocol kaochow-3(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh kir, kt: SessionKey; fresh kir, kt: SessionKey;
read_1 (I,S, I,R,ni); recv_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) );
} }
} }

8
gui/Protocols/MultiProtocolAttacks/kaochow.spdl
View File

@ -17,7 +17,7 @@ protocol kaochow(I,R,S)
var kir: SessionKey; var kir: SessionKey;
send_1 (I,S, I,R,ni); send_1 (I,S, I,R,ni);
read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr ); recv_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
send_4 (I,R, {nr}kir ); send_4 (I,R, {nr}kir );
claim_I1 (I, Nisynch); claim_I1 (I, Nisynch);
@ -33,9 +33,9 @@ protocol kaochow(I,R,S)
var kir: SessionKey; var kir: SessionKey;
var T; var T;
read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); recv_2 (S,R, T, { I,R,ni,kir }k(R,S) );
send_3 (R,I, T, {ni}kir, nr ); send_3 (R,I, T, {ni}kir, nr );
read_4 (I,R, {nr}kir ); recv_4 (I,R, {nr}kir );
claim_R1 (R, Nisynch); claim_R1 (R, Nisynch);
claim_R2 (R, Niagree); claim_R2 (R, Niagree);
@ -48,7 +48,7 @@ protocol kaochow(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh kir: SessionKey; fresh kir: SessionKey;
read_1 (I,S, I,R,ni); recv_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) ); send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) );
} }
} }

16
gui/Protocols/MultiProtocolAttacks/ksl.spdl
View File

@ -24,11 +24,11 @@ protocol ksl(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, Ni, I); send_1(I,R, Ni, I);
read_4(R,I, { Ni,R,Kir }k(I,S), T, Nc, {Ni}Kir ); recv_4(R,I, { Ni,R,Kir }k(I,S), T, Nc, {Ni}Kir );
send_5(I,R, { Nc }Kir ); send_5(I,R, { Nc }Kir );
send_6(I,R, Mi,T ); send_6(I,R, Mi,T );
read_7(R,I, Mr,{Mi}Kir ); recv_7(R,I, Mr,{Mi}Kir );
send_8(I,R, {Mr}Kir ); send_8(I,R, {Mr}Kir );
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
@ -46,15 +46,15 @@ protocol ksl(I,R,S)
fresh Tr: TimeStamp; fresh Tr: TimeStamp;
var T: Ticket; var T: Ticket;
read_1(I,R, Ni, I); recv_1(I,R, Ni, I);
send_2(R,S, Ni, I, Nr, R ); send_2(R,S, Ni, I, Nr, R );
read_3(S,R, { Nr, I, Kir }k(R,S), T ); recv_3(S,R, { Nr, I, Kir }k(R,S), T );
send_4(R,I, T, { Tr, I, Kir }Kbb, Nc, {Ni}Kir ); send_4(R,I, T, { Tr, I, Kir }Kbb, Nc, {Ni}Kir );
read_5(I,R, { Nc }Kir ); recv_5(I,R, { Nc }Kir );
read_6(I,R, Mi,{ Tr, I, Kir }Kbb ); recv_6(I,R, Mi,{ Tr, I, Kir }Kbb );
send_7(R,I, Mr,{Mi}Kir ); send_7(R,I, Mr,{Mi}Kir );
read_8(I,R, {Mr}Kir ); recv_8(I,R, {Mr}Kir );
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
@ -67,7 +67,7 @@ protocol ksl(I,R,S)
var Ni, Nr: Nonce; var Ni, Nr: Nonce;
fresh Kir: SessionKey; fresh Kir: SessionKey;
read_2(R,S, Ni, I, Nr, R ); recv_2(R,S, Ni, I, Nr, R );
send_3(S,R, { Nr, I, Kir }k(R,S), { Ni,R,Kir }k(I,S) ); send_3(S,R, { Nr, I, Kir }k(R,S), { Ni,R,Kir }k(I,S) );
} }
} }

14
gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl
View File

@ -27,11 +27,11 @@ protocol needhamschroedersk-amend(I,R,S)
var T,T2: Ticket; var T,T2: Ticket;
send_1(I,R,I); send_1(I,R,I);
read_2(R,I,T); recv_2(R,I,T);
send_3(I,S,(I,R,Ni,T)); send_3(I,S,(I,R,Ni,T));
read_4(S,I, {Ni,R,Kir,T2}k(I,S)); recv_4(S,I, {Ni,R,Kir,T2}k(I,S));
send_5(I,R,T2); send_5(I,R,T2);
read_6(R,I,{Nr}Kir); recv_6(R,I,{Nr}Kir);
send_7(I,R,{{Nr}dec}Kir); send_7(I,R,{{Nr}dec}Kir);
claim_I2(I,Secret,Kir); claim_I2(I,Secret,Kir);
@ -44,11 +44,11 @@ protocol needhamschroedersk-amend(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
read_1(I,R,I); recv_1(I,R,I);
send_2(R,I,{I,Nr}k(R,S)); send_2(R,I,{I,Nr}k(R,S));
read_5(I,R,{Kir,Nr,I}k(R,S)); recv_5(I,R,{Kir,Nr,I}k(R,S));
send_6(R,I,{Nr}Kir); send_6(R,I,{Nr}Kir);
read_7(I,R,{{Nr}dec}Kir); recv_7(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Nr); claim_R1(R,Secret,Nr);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir)); claim_R4(R,Empty,(Fresh,Kir));
@ -58,7 +58,7 @@ protocol needhamschroedersk-amend(I,R,S)
{ {
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
fresh Kir: SessionKey; fresh Kir: SessionKey;
read_3(I,S,(I,R,Ni,{I,Nr}k(R,S))); recv_3(I,S,(I,R,Ni,{I,Nr}k(R,S)));
send_4(S,I,{Ni,R,Kir,{Kir,Nr,I}k(R,S)}k(I,S)); send_4(S,I,{Ni,R,Kir,{Kir,Nr,I}k(R,S)}k(I,S));
} }

10
gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl
View File

@ -23,9 +23,9 @@ protocol needhamschroedersk(I,R,S)
var T: Ticket; var T: Ticket;
send_1(I,S,(I,R,Ni)); send_1(I,S,(I,R,Ni));
read_2(S,I, {Ni,R,Kir,T}k(I,S)); recv_2(S,I, {Ni,R,Kir,T}k(I,S));
send_3(I,R,T); send_3(I,R,T);
read_4(R,I,{Nr}Kir); recv_4(R,I,{Nr}Kir);
send_5(I,R,{{Nr}dec}Kir); send_5(I,R,{{Nr}dec}Kir);
claim_I2(I,Secret,Kir); claim_I2(I,Secret,Kir);
claim_I3(I,Nisynch); claim_I3(I,Nisynch);
@ -37,9 +37,9 @@ protocol needhamschroedersk(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
read_3(I,R,{Kir,I}k(R,S)); recv_3(I,R,{Kir,I}k(R,S));
send_4(R,I,{Nr}Kir); send_4(R,I,{Nr}Kir);
read_5(I,R,{{Nr}dec}Kir); recv_5(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir)); claim_R4(R,Empty,(Fresh,Kir));
@ -49,7 +49,7 @@ protocol needhamschroedersk(I,R,S)
{ {
var Ni: Nonce; var Ni: Nonce;
fresh Kir: SessionKey; fresh Kir: SessionKey;
read_1(I,S,(I,R,Ni)); recv_1(I,S,(I,R,Ni));
send_2(S,I,{Ni,R,Kir,{Kir,I}k(R,S)}k(I,S)); send_2(S,I,{Ni,R,Kir,{Kir,I}k(R,S)}k(I,S));
} }
} }

6
gui/Protocols/MultiProtocolAttacks/ns3.spdl
View File

@ -12,7 +12,7 @@ protocol ns3(I,R)
var nr: Nonce; var nr: Nonce;
send_1(I,R, {ni,I}pk(R) ); send_1(I,R, {ni,I}pk(R) );
read_2(R,I, {ni,nr}pk(I) ); recv_2(R,I, {ni,nr}pk(I) );
send_3(I,R, {nr}pk(R) ); send_3(I,R, {nr}pk(R) );
claim_i1(I,Secret,ni); claim_i1(I,Secret,ni);
@ -27,9 +27,9 @@ protocol ns3(I,R)
var ni: Nonce; var ni: Nonce;
fresh nr: Nonce; fresh nr: Nonce;
read_1(I,R, {ni,I}pk(R) ); recv_1(I,R, {ni,I}pk(R) );
send_2(R,I, {ni,nr}pk(I) ); send_2(R,I, {ni,nr}pk(I) );
read_3(I,R, {nr}pk(R) ); recv_3(I,R, {nr}pk(R) );
claim_r1(R,Secret,ni); claim_r1(R,Secret,ni);
claim_r2(R,Secret,nr); claim_r2(R,Secret,nr);

6
gui/Protocols/MultiProtocolAttacks/nsl3.spdl
View File

@ -12,7 +12,7 @@ protocol nsl3(I,R)
var nr: Nonce; var nr: Nonce;
send_1(I,R, {ni,I}pk(R) ); send_1(I,R, {ni,I}pk(R) );
read_2(R,I, {ni,nr,R}pk(I) ); recv_2(R,I, {ni,nr,R}pk(I) );
send_3(I,R, {nr}pk(R) ); send_3(I,R, {nr}pk(R) );
claim_i1(I,Secret,ni); claim_i1(I,Secret,ni);
@ -26,9 +26,9 @@ protocol nsl3(I,R)
var ni: Nonce; var ni: Nonce;
fresh nr: Nonce; fresh nr: Nonce;
read_1(I,R, {ni,I}pk(R) ); recv_1(I,R, {ni,I}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) ); send_2(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) ); recv_3(I,R, {nr}pk(R) );
claim_r1(R,Secret,ni); claim_r1(R,Secret,ni);
claim_r2(R,Secret,nr); claim_r2(R,Secret,nr);

8
gui/Protocols/MultiProtocolAttacks/otwayrees.spdl
View File

@ -19,7 +19,7 @@ protocol otwayrees(I,R,S)
var Kir : SessionKey; var Kir : SessionKey;
send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) ); send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) );
read_4(R,I, M,{Ni,Kir}k(I,S) ); recv_4(R,I, M,{Ni,Kir}k(I,S) );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch); claim_I2(I, Nisynch);
@ -33,9 +33,9 @@ protocol otwayrees(I,R,S)
var Kir : SessionKey; var Kir : SessionKey;
var T1,T2: Ticket; var T1,T2: Ticket;
read_1(I,R, M,I,R, T1 ); recv_1(I,R, M,I,R, T1 );
send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) ); send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) );
read_3(S,R, M, T2, { Nr,Kir }k(R,S) ); recv_3(S,R, M, T2, { Nr,Kir }k(R,S) );
send_4(R,I, M, T2 ); send_4(R,I, M, T2 );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
@ -49,7 +49,7 @@ protocol otwayrees(I,R,S)
var M : String; var M : String;
fresh Kir : SessionKey; fresh Kir : SessionKey;
read_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) ); recv_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) );
send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) ); send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) );
} }
} }

4
gui/Protocols/MultiProtocolAttacks/soph.spdl
View File

@ -6,7 +6,7 @@ protocol soph(I,R)
fresh ni: Nonce; fresh ni: Nonce;
send_1(I,R, {I,ni}pk(R) ); send_1(I,R, {I,ni}pk(R) );
read_2(R,I, ni ); recv_2(R,I, ni );
claim_3(I,Niagree); claim_3(I,Niagree);
} }
@ -14,7 +14,7 @@ protocol soph(I,R)
{ {
var ni: Nonce; var ni: Nonce;
read_1(I,R, {I,ni}pk(R) ); recv_1(I,R, {I,ni}pk(R) );
send_2(R,I, ni ); send_2(R,I, ni );
} }
} }

12
gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl
View File

@ -24,9 +24,9 @@ protocol spliceAS-CJ(I,R,S)
fresh L: LifeTime; fresh L: LifeTime;
send_1(I,S, I, R, N1 ); send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); recv_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
send_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); send_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
read_6(R,I, R, I, {{N2}inc}pk(I) ); recv_6(R,I, R, I, {{N2}inc}pk(I) );
claim_7(I, Secret, N2); claim_7(I, Secret, N2);
claim_9(I, Niagree); claim_9(I, Niagree);
@ -37,9 +37,9 @@ protocol spliceAS-CJ(I,R,S)
{ {
var N1,N3: Nonce; var N1,N3: Nonce;
read_1(I,S, I, R, N1 ); recv_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
read_4(R,S, R, I, N3 ); recv_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); send_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
} }
@ -53,9 +53,9 @@ protocol spliceAS-CJ(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh nr: Nonce; fresh nr: Nonce;
read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); recv_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 ); send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); recv_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
send_6(R,I, R, I, {{N2}inc}pk(I) ); send_6(R,I, R, I, {{N2}inc}pk(I) );
claim_8(R, Secret, N2); claim_8(R, Secret, N2);

12
gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl
View File

@ -19,9 +19,9 @@ protocol spliceAS-HC(I,R,S)
fresh L: LifeTime; fresh L: LifeTime;
send_1(I,S, I, R, N1 ); send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); recv_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
read_6(R,I, R, I, {R, {N2}inc}pk(I) ); recv_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_7(I, Secret, N2); claim_7(I, Secret, N2);
claim_9(I, Niagree); claim_9(I, Niagree);
@ -32,9 +32,9 @@ protocol spliceAS-HC(I,R,S)
{ {
var N1,N3: Nonce; var N1,N3: Nonce;
read_1(I,S, I, R, N1 ); recv_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
read_4(R,S, R, I, N3 ); recv_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); send_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) );
} }
@ -48,9 +48,9 @@ protocol spliceAS-HC(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh nr: Nonce; fresh nr: Nonce;
read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); recv_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 ); send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); recv_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) );
send_6(R,I, R, I, {R, {N2}inc}pk(I) ); send_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_8(R, Secret, N2); claim_8(R, Secret, N2);

12
gui/Protocols/MultiProtocolAttacks/splice-as.spdl
View File

@ -24,9 +24,9 @@ protocol spliceAS(I,R,S)
fresh L: LifeTime; fresh L: LifeTime;
send_1(I,S, I, R, N1 ); send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); recv_2(S,I, S, {S, I, N1, pk(R)}sk(S) );
send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
read_6(R,I, R, I, {R, {N2}inc}pk(I) ); recv_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_7(I, Secret, N2); claim_7(I, Secret, N2);
claim_9(I, Niagree); claim_9(I, Niagree);
@ -37,9 +37,9 @@ protocol spliceAS(I,R,S)
{ {
var N1,N3: Nonce; var N1,N3: Nonce;
read_1(I,S, I, R, N1 ); recv_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); send_2(S,I, S, {S, I, N1, pk(R)}sk(S) );
read_4(R,S, R, I, N3 ); recv_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); send_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
} }
@ -53,9 +53,9 @@ protocol spliceAS(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh nr: Nonce; fresh nr: Nonce;
read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); recv_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 ); send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); recv_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
send_6(R,I, R, I, {R, {N2}inc}pk(I) ); send_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_8(R, Secret, N2); claim_8(R, Secret, N2);

8
gui/Protocols/MultiProtocolAttacks/tmn.spdl
View File

@ -19,7 +19,7 @@ protocol tmn(I,R,S)
var Kr: SessionKey; var Kr: SessionKey;
send_1(I,S, R,{Ki}pk(S) ); send_1(I,S, R,{Ki}pk(S) );
read_4(S,I, R,{Kr}Ki ); recv_4(S,I, R,{Kr}Ki );
claim_I1(I,Secret,Kr); claim_I1(I,Secret,Kr);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
@ -30,7 +30,7 @@ protocol tmn(I,R,S)
{ {
fresh Kr: SessionKey; fresh Kr: SessionKey;
read_2(S,R, I ); recv_2(S,R, I );
send_3(R,S, I, { Kr }pk(S) ); send_3(R,S, I, { Kr }pk(S) );
claim_R1(R,Secret,Kr); claim_R1(R,Secret,Kr);
@ -42,9 +42,9 @@ protocol tmn(I,R,S)
{ {
var Ki,Kr: SessionKey; var Ki,Kr: SessionKey;
read_1(I,S, R,{Ki}pk(S) ); recv_1(I,S, R,{Ki}pk(S) );
send_2(S,R, I ); send_2(S,R, I );
read_3(R,S, I, { Kr }pk(S) ); recv_3(R,S, I, { Kr }pk(S) );
send_4(S,I, R,{Kr}Ki ); send_4(S,I, R,{Kr}Ki );
} }
} }

4
gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl
View File

@ -16,7 +16,7 @@ protocol wmfbrutus(A,B,S)
{ {
var kab : SesKey; var kab : SesKey;
read_2(S,B, { A, kab }k(B,S) ); recv_2(S,B, { A, kab }k(B,S) );
claim_3(B, Secret,kab); claim_3(B, Secret,kab);
} }
@ -25,7 +25,7 @@ protocol wmfbrutus(A,B,S)
{ {
var kab : SesKey; var kab : SesKey;
read_1(A,S, A, { B,kab }k(A,S) ); recv_1(A,S, A, { B,kab }k(A,S) );
send_2(S,B, { A, kab }k(B,S) ); send_2(S,B, { A, kab }k(B,S) );
} }
} }

10
gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl
View File

@ -6,7 +6,7 @@
# Note: # Note:
# According to SPORE there are no known attacks on this protocol, scyther # According to SPORE there are no known attacks on this protocol, scyther
# finds one however this has to do with the unusual assumption that every # finds one however this has to do with the unusual assumption that every
# agent can recognise and will reject to read messages that it has created # agent can recognise and will reject to recv messages that it has created
# itself. # itself.
usertype SessionKey; usertype SessionKey;
@ -27,7 +27,7 @@ protocol wmf-Lowe(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,S, I, {Ti, R, Kir}k(I,S)); send_1(I,S, I, {Ti, R, Kir}k(I,S));
read_3(R,I,{Nr}Kir); recv_3(R,I,{Nr}Kir);
send_4(I,R,{{Nr}succ}Kir); send_4(I,R,{{Nr}succ}Kir);
claim_I1(I,Secret,Kir); claim_I1(I,Secret,Kir);
@ -41,9 +41,9 @@ protocol wmf-Lowe(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
fresh Nr: Nonce; fresh Nr: Nonce;
read_2(S,R, {Ts, I, Kir}k(R,S) ); recv_2(S,R, {Ts, I, Kir}k(R,S) );
send_3(R,I, {Nr}Kir); send_3(R,I, {Nr}Kir);
read_4(I,R, {{Nr}succ}Kir); recv_4(I,R, {{Nr}succ}Kir);
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
@ -56,7 +56,7 @@ protocol wmf-Lowe(I,R,S)
fresh Ts: TimeStamp; fresh Ts: TimeStamp;
var Ti: TimeStamp; var Ti: TimeStamp;
read_1(I,S, I,{Ti, R, Kir}k(I,S) ); recv_1(I,S, I,{Ti, R, Kir}k(I,S) );
send_2(S,R, {Ts, I, Kir}k(R,S)); send_2(S,R, {Ts, I, Kir}k(R,S));
} }
} }

4
gui/Protocols/MultiProtocolAttacks/wmf.spdl
View File

@ -34,7 +34,7 @@ protocol wmf(I,R,S)
var Ts: TimeStamp; var Ts: TimeStamp;
var Kir: SessionKey; var Kir: SessionKey;
read_2(S,R, {S, Ts, I, Kir}k(R,S) ); recv_2(S,R, {S, Ts, I, Kir}k(R,S) );
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
@ -47,7 +47,7 @@ protocol wmf(I,R,S)
fresh Ts: TimeStamp; fresh Ts: TimeStamp;
var Ti: TimeStamp; var Ti: TimeStamp;
read_1(I,S, I,{I, Ti, R, Kir}k(I,S) ); recv_1(I,S, I,{I, Ti, R, Kir}k(I,S) );
send_2(S,R, {S, Ts, I, Kir}k(R,S)); send_2(S,R, {S, Ts, I, Kir}k(R,S));
} }
} }

10
gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl
View File

@ -11,7 +11,7 @@ protocol woolamPi-1(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); recv_2(R,I, Nr);
send_3(I,R, {I,R,Nr}k(I,S)); send_3(I,R, {I,R,Nr}k(I,S));
} }
@ -21,11 +21,11 @@ protocol woolamPi-1(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var T: Ticket; var T: Ticket;
read_1(I,R, I); recv_1(I,R, I);
send_2(R,I, Nr); send_2(R,I, Nr);
read_3(I,R, T); recv_3(I,R, T);
send_4(R,S, {I,R, T}k(R,S)); send_4(R,S, {I,R, T}k(R,S));
read_5(S,R, {I,R, Nr}k(R,S)); recv_5(S,R, {I,R, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
@ -34,7 +34,7 @@ protocol woolamPi-1(I,R,S)
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I,R, {I,R,Nr}k(I,S)}k(R,S)); recv_4(R,S, {I,R, {I,R,Nr}k(I,S)}k(R,S));
send_5(S,R, {I,R,Nr}k(R,S)); send_5(S,R, {I,R,Nr}k(R,S));
} }
} }

10
gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl
View File

@ -11,7 +11,7 @@ protocol woolamPi-2(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); recv_2(R,I, Nr);
send_3(I,R, {I,Nr}k(I,S)); send_3(I,R, {I,Nr}k(I,S));
} }
@ -21,11 +21,11 @@ protocol woolamPi-2(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var T: Ticket; var T: Ticket;
read_1(I,R, I); recv_1(I,R, I);
send_2(R,I, Nr); send_2(R,I, Nr);
read_3(I,R, T); recv_3(I,R, T);
send_4(R,S, {I, T}k(R,S)); send_4(R,S, {I, T}k(R,S));
read_5(S,R, {I, Nr}k(R,S)); recv_5(S,R, {I, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
@ -34,7 +34,7 @@ protocol woolamPi-2(I,R,S)
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I, {I,Nr}k(I,S)}k(R,S)); recv_4(R,S, {I, {I,Nr}k(I,S)}k(R,S));
send_5(S,R, {I,Nr}k(R,S)); send_5(S,R, {I,Nr}k(R,S));
} }
} }

10
gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl
View File

@ -11,7 +11,7 @@ protocol woolamPi-3(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); recv_2(R,I, Nr);
send_3(I,R, {Nr}k(I,S)); send_3(I,R, {Nr}k(I,S));
} }
@ -21,11 +21,11 @@ protocol woolamPi-3(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var T: Ticket; var T: Ticket;
read_1(I,R, I); recv_1(I,R, I);
send_2(R,I, Nr); send_2(R,I, Nr);
read_3(I,R, T); recv_3(I,R, T);
send_4(R,S, {I, T}k(R,S)); send_4(R,S, {I, T}k(R,S));
read_5(S,R, {I, Nr}k(R,S)); recv_5(S,R, {I, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
@ -34,7 +34,7 @@ protocol woolamPi-3(I,R,S)
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I, {Nr}k(I,S)}k(R,S)); recv_4(R,S, {I, {Nr}k(I,S)}k(R,S));
send_5(S,R, {I,Nr}k(R,S)); send_5(S,R, {I,Nr}k(R,S));
} }
} }

10
gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl
View File

@ -11,7 +11,7 @@ protocol woolamPi-f(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); recv_2(R,I, Nr);
send_3(I,R, {I,R,Nr}k(I,S)); send_3(I,R, {I,R,Nr}k(I,S));
} }
@ -21,11 +21,11 @@ protocol woolamPi-f(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var T: Ticket; var T: Ticket;
read_1(I,R, I); recv_1(I,R, I);
send_2(R,I, Nr); send_2(R,I, Nr);
read_3(I,R, T); recv_3(I,R, T);
send_4(R,S, {I, R, Nr, T}k(R,S)); send_4(R,S, {I, R, Nr, T}k(R,S));
read_5(S,R, {I, R, Nr}k(R,S)); recv_5(S,R, {I, R, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
@ -34,7 +34,7 @@ protocol woolamPi-f(I,R,S)
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S)); recv_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S));
send_5(S,R, {I, R, Nr}k(R,S)); send_5(S,R, {I, R, Nr}k(R,S));
} }
} }

14
gui/Protocols/MultiProtocolAttacks/woo-lam.spdl
View File

@ -19,9 +19,9 @@ protocol woolam(I,R,S)
var N2: Nonce; var N2: Nonce;
send_1(I,R, I, N1); send_1(I,R, I, N1);
read_2(R,I, R, N2); recv_2(R,I, R, N2);
send_3(I,R, {I, R, N1, N2}k(I,S)); send_3(I,R, {I, R, N1, N2}k(I,S));
read_6(R,I, {R, N1, N2, Kir}k(I,S), {N1,N2}Kir); recv_6(R,I, {R, N1, N2, Kir}k(I,S), {N1,N2}Kir);
send_7(I,R, {N2}Kir); send_7(I,R, {N2}Kir);
@ -37,13 +37,13 @@ protocol woolam(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
var T1,T2: Ticket; var T1,T2: Ticket;
read_1(I,R, I, N1); recv_1(I,R, I, N1);
send_2(R,I, R, N2); send_2(R,I, R, N2);
read_3(I,R, T1); recv_3(I,R, T1);
send_4(R,S, T1, {I, R, N1, N2}k(R,S)); send_4(R,S, T1, {I, R, N1, N2}k(R,S));
read_5(S,R, T2, {I, N1, N2, Kir}k(R,S)); recv_5(S,R, T2, {I, N1, N2, Kir}k(R,S));
send_6(R,I, T2, {N1,N2}Kir); send_6(R,I, T2, {N1,N2}Kir);
read_7(I,R, {N2}Kir); recv_7(I,R, {N2}Kir);
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
@ -55,7 +55,7 @@ protocol woolam(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var N1,N2: Nonce; var N1,N2: Nonce;
read_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S)); recv_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S));
send_5(S,R, {R, N1, N2, Kir}k(I,S), {I, N1, N2, Kir}k(R,S)); send_5(S,R, {R, N1, N2, Kir}k(I,S), {I, N1, N2, Kir}k(R,S));
} }
} }

8
gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl
View File

@ -19,7 +19,7 @@ protocol yahalom-BAN-Paulson-modified(A,B,S)
var kab: SessionKey; var kab: SessionKey;
send_1(A,B, A,na); send_1(A,B, A,na);
read_3(S,A, nb, {B,kab,na}k(A,S), ticket ); recv_3(S,A, nb, {B,kab,na}k(A,S), ticket );
send_4(A,B, ticket, {nb}kab ); send_4(A,B, ticket, {nb}kab );
claim_5(A, Secret,kab); claim_5(A, Secret,kab);
} }
@ -31,9 +31,9 @@ protocol yahalom-BAN-Paulson-modified(A,B,S)
var ticket: Ticket; var ticket: Ticket;
var kab: SessionKey; var kab: SessionKey;
read_1(A,B, A,na); recv_1(A,B, A,na);
send_2(B,S, B, nb, {A,na}k(B,S) ); send_2(B,S, B, nb, {A,na}k(B,S) );
read_4(A,B, {A,B,kab,nb}k(B,S) , {nb}kab ); recv_4(A,B, {A,B,kab,nb}k(B,S) , {nb}kab );
claim_6(B, Secret,kab); claim_6(B, Secret,kab);
} }
@ -42,7 +42,7 @@ protocol yahalom-BAN-Paulson-modified(A,B,S)
fresh kab: SessionKey; fresh kab: SessionKey;
var na,nb: Nonce; var na,nb: Nonce;
read_2(B,S, B, nb, {A,na}k(B,S) ); recv_2(B,S, B, nb, {A,na}k(B,S) );
send_3(S,A, nb, {B,kab,na}k(A,S), {A,B,kab,nb}k(B,S) ); send_3(S,A, nb, {B,kab,na}k(A,S), {A,B,kab,nb}k(B,S) );
} }
} }

8
gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl
View File

@ -17,7 +17,7 @@ protocol yahalom-BAN-Paulson(A,B,S)
var kab: SessionKey; var kab: SessionKey;
send_1(A,B, A,na); send_1(A,B, A,na);
read_3(S,A, {B,kab,na,nb}k(A,S), ticket ); recv_3(S,A, {B,kab,na,nb}k(A,S), ticket );
send_4(A,B, ticket, {nb}kab ); send_4(A,B, ticket, {nb}kab );
claim_5(A, Secret,kab); claim_5(A, Secret,kab);
} }
@ -29,9 +29,9 @@ protocol yahalom-BAN-Paulson(A,B,S)
var ticket: Ticket; var ticket: Ticket;
var kab: SessionKey; var kab: SessionKey;
read_1(A,B, A,na); recv_1(A,B, A,na);
send_2(B,S, B, {A,na,nb}k(B,S) ); send_2(B,S, B, {A,na,nb}k(B,S) );
read_4(A,B, {A,kab}k(B,S) , {nb}kab ); recv_4(A,B, {A,kab}k(B,S) , {nb}kab );
claim_6(B, Secret,kab); claim_6(B, Secret,kab);
} }
@ -40,7 +40,7 @@ protocol yahalom-BAN-Paulson(A,B,S)
fresh kab: SessionKey; fresh kab: SessionKey;
var na,nb: Nonce; var na,nb: Nonce;
read_2(B,S, B, {A,na,nb}k(B,S) ); recv_2(B,S, B, {A,na,nb}k(B,S) );
send_3(S,A, {B,kab,na,nb}k(A,S), {A,kab}k(B,S) ); send_3(S,A, {B,kab,na,nb}k(A,S), {A,kab}k(B,S) );
} }
} }

8
gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl
View File

@ -18,7 +18,7 @@ protocol yahalom-BAN(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); recv_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
send_4(I,R, T, {Nr}Kir ); send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
@ -33,9 +33,9 @@ protocol yahalom-BAN(I,R,S)
var T: Ticket; var T: Ticket;
var Kir: SessionKey; var Kir: SessionKey;
read_1(I,R, I,Ni); recv_1(I,R, I,Ni);
send_2(R,S, R, Nr, {I,Ni}k(R,S) ); send_2(R,S, R, Nr, {I,Ni}k(R,S) );
read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir ); recv_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch); claim_R2(R, Nisynch);
@ -47,7 +47,7 @@ protocol yahalom-BAN(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, R, Nr, {I,Ni}k(R,S) ); recv_2(R,S, R, Nr, {I,Ni}k(R,S) );
send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,Kir,Nr}k(R,S) ); send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,Kir,Nr}k(R,S) );
} }
} }

10
gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl
View File

@ -17,7 +17,7 @@ protocol yahalom-Lowe(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, {R,Kir,Ni,Nr}k(I,S) ); recv_3(S,I, {R,Kir,Ni,Nr}k(I,S) );
send_5(I,R, {I, R, S, Nr}Kir ); send_5(I,R, {I, R, S, Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
@ -30,10 +30,10 @@ protocol yahalom-Lowe(I,R,S)
var Ni: Nonce; var Ni: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
read_1(I,R, I,Ni); recv_1(I,R, I,Ni);
send_2(R,S, {I,Ni,Nr}k(R,S) ); send_2(R,S, {I,Ni,Nr}k(R,S) );
read_4(S,R, {I,Kir}k(R,S)); recv_4(S,R, {I,Kir}k(R,S));
read_5(I,R, {I, R, S, Nr}Kir); recv_5(I,R, {I, R, S, Nr}Kir);
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch); claim_R2(R, Nisynch);
@ -44,7 +44,7 @@ protocol yahalom-Lowe(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, {I,Ni,Nr}k(R,S) ); recv_2(R,S, {I,Ni,Nr}k(R,S) );
send_3(S,I, {R,Kir,Ni,Nr}k(I,S)); send_3(S,I, {R,Kir,Ni,Nr}k(I,S));
send_4(S,R, {I,Kir}k(R,S)); send_4(S,R, {I,Kir}k(R,S));
} }

8
gui/Protocols/MultiProtocolAttacks/yahalom.spdl
View File

@ -17,7 +17,7 @@ protocol yahalom(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T ); recv_3(S,I, {R,Kir,Ni,Nr}k(I,S), T );
send_4(I,R, T, {Nr}Kir ); send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
@ -30,9 +30,9 @@ protocol yahalom(I,R,S)
var T: Ticket; var T: Ticket;
var Kir: SessionKey; var Kir: SessionKey;
read_1(I,R, I,Ni); recv_1(I,R, I,Ni);
send_2(R,S, R, {I,Ni,Nr}k(R,S) ); send_2(R,S, R, {I,Ni,Nr}k(R,S) );
read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir ); recv_4(I,R, {I,Kir}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
} }
@ -42,7 +42,7 @@ protocol yahalom(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, R, {I,Ni,Nr}k(R,S) ); recv_2(R,S, R, {I,Ni,Nr}k(R,S) );
send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) ); send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
claim(S, Secret, Ni); claim(S, Secret, Ni);

13
gui/Protocols/andrew-ban-concrete.spdl
View File

@ -10,7 +10,7 @@
# a given term crypted with k(I,R) with k(R,I) # a given term crypted with k(I,R) with k(R,I)
# #
# Note: # Note:
# Read 4 by the Initatior has been placed after the synchronisation claim # Recv 4 by the Initatior has been placed after the synchronisation claim
# as it allows trivial synchronisation attacks otherwise (the message is # as it allows trivial synchronisation attacks otherwise (the message is
# completely fresh and can therefore always be replaced by an arbitrary value # completely fresh and can therefore always be replaced by an arbitrary value
# created by the intruder) which are not considered in SPORE # created by the intruder) which are not considered in SPORE
@ -18,7 +18,6 @@
usertype SessionKey; usertype SessionKey;
const Fresh: Function; const Fresh: Function;
const Compromised: Function;
protocol @swapkey(X) protocol @swapkey(X)
{ {
@ -27,7 +26,7 @@ protocol @swapkey(X)
{ {
var I,R: Agent; var I,R: Agent;
var T:Ticket; var T:Ticket;
read_!X1(X,X,I,R,{T}k(I,R)); recv_!X1(X,X,I,R,{T}k(I,R));
send_!X2(X,X,{T}k(R,I)); send_!X2(X,X,{T}k(R,I));
} }
} }
@ -42,12 +41,12 @@ protocol andrew-Concrete(I,R)
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,ni ); send_1(I,R, I,ni );
read_2(R,I, {ni,kir}k(I,R) ); recv_2(R,I, {ni,kir}k(I,R) );
send_3(I,R, {ni}kir); send_3(I,R, {ni}kir);
claim_I1(I,Secret,kir); claim_I1(I,Secret,kir);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
claim_I3(I,Empty,(Fresh,kir)); claim_I3(I,Empty,(Fresh,kir));
read_6(R,I, nr); recv_6(R,I, nr);
} }
role R role R
@ -56,9 +55,9 @@ protocol andrew-Concrete(I,R)
fresh nr: Nonce; fresh nr: Nonce;
fresh kir: SessionKey; fresh kir: SessionKey;
read_1(I,R, I,ni ); recv_1(I,R, I,ni );
send_2(R,I, {ni,kir}k(I,R) ); send_2(R,I, {ni,kir}k(I,R) );
read_3(I,R, {ni}kir); recv_3(I,R, {ni}kir);
send_6(R,I, nr); send_6(R,I, nr);
claim_R1(R,Secret,kir); claim_R1(R,Secret,kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);

8
gui/Protocols/andrew-ban.spdl
View File

@ -24,9 +24,9 @@ protocol andrew-Ban(I,R)
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,{ni}k(I,R) ); send_1(I,R, I,{ni}k(I,R) );
read_2(R,I, {ni,nr}k(I,R) ); recv_2(R,I, {ni,nr}k(I,R) );
send_3(I,R, {nr}k(I,R) ); send_3(I,R, {nr}k(I,R) );
read_4(R,I, {kir,nr2,ni}k(I,R) ); recv_4(R,I, {kir,nr2,ni}k(I,R) );
claim_I1(I,Nisynch); claim_I1(I,Nisynch);
claim_I2(I,Niagree); claim_I2(I,Niagree);
claim_I3(I,Secret, kir); claim_I3(I,Secret, kir);
@ -40,9 +40,9 @@ protocol andrew-Ban(I,R)
fresh nr,nr2: Nonce; fresh nr,nr2: Nonce;
fresh kir: SessionKey; fresh kir: SessionKey;
read_1(I,R, I,{ni}k(I,R) ); recv_1(I,R, I,{ni}k(I,R) );
send_2(R,I, {ni,nr}k(I,R) ); send_2(R,I, {ni,nr}k(I,R) );
read_3(I,R, {nr}k(I,R) ); recv_3(I,R, {nr}k(I,R) );
send_4(R,I, {kir,nr2,ni}k(I,R) ); send_4(R,I, {kir,nr2,ni}k(I,R) );
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
claim_R2(R,Niagree); claim_R2(R,Niagree);

10
gui/Protocols/andrew-lowe-ban.spdl
View File

@ -9,7 +9,7 @@
# So it is possile that certain attacks that use this property are not found # So it is possile that certain attacks that use this property are not found
# #
# Note: # Note:
# Read 4 by the Initatior has been placed after the synchronisation claim # Recv 4 by the Initatior has been placed after the synchronisation claim
# as it allows trivial synchronisation attacks otherwise (the message is # as it allows trivial synchronisation attacks otherwise (the message is
# completely fresh and can therefore always be replaced by an arbitrary value # completely fresh and can therefore always be replaced by an arbitrary value
# created by the intruder) which are not considered in SPORE # created by the intruder) which are not considered in SPORE
@ -31,12 +31,12 @@ protocol andrew-LoweBan(I,R)
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,ni ); send_1(I,R, I,ni );
read_2(R,I, {ni,kir,R}k(I,R) ); recv_2(R,I, {ni,kir,R}k(I,R) );
send_3(I,R, {ni}kir ); send_3(I,R, {ni}kir );
claim_I1(I,Nisynch); claim_I1(I,Nisynch);
claim_I2(I,Secret, kir); claim_I2(I,Secret, kir);
claim_I3(I,Empty, (Fresh,kir)); claim_I3(I,Empty, (Fresh,kir));
read_4(R,I, nr ); recv_4(R,I, nr );
} }
role R role R
@ -45,9 +45,9 @@ protocol andrew-LoweBan(I,R)
fresh nr: Nonce; fresh nr: Nonce;
fresh kir: SessionKey; fresh kir: SessionKey;
read_1(I,R, I,ni ); recv_1(I,R, I,ni );
send_2(R,I, {ni,kir,R}k(I,R) ); send_2(R,I, {ni,kir,R}k(I,R) );
read_3(I,R, {ni}kir ); recv_3(I,R, {ni}kir );
send_4(R,I, nr ); send_4(R,I, nr );
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
claim_R2(R,Secret, kir); claim_R2(R,Secret, kir);

9
gui/Protocols/andrew.spdl
View File

@ -12,7 +12,6 @@
usertype SessionKey; usertype SessionKey;
const succ: Function; const succ: Function;
const Fresh: Function; const Fresh: Function;
const Compromised: Function;
protocol andrew(I,R) protocol andrew(I,R)
{ {
@ -23,9 +22,9 @@ protocol andrew(I,R)
var kir: SessionKey; var kir: SessionKey;
send_1(I,R, I,{ni}k(I,R) ); send_1(I,R, I,{ni}k(I,R) );
read_2(R,I, {succ(ni),nr}k(I,R) ); recv_2(R,I, {succ(ni),nr}k(I,R) );
send_3(I,R, {succ(nr)}k(I,R) ); send_3(I,R, {succ(nr)}k(I,R) );
read_4(R,I, {kir,nr2}k(I,R) ); recv_4(R,I, {kir,nr2}k(I,R) );
claim_I1(I,Secret,kir); claim_I1(I,Secret,kir);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
claim_I3(I,Niagree); claim_I3(I,Niagree);
@ -38,9 +37,9 @@ protocol andrew(I,R)
fresh nr,nr2: Nonce; fresh nr,nr2: Nonce;
fresh kir: SessionKey; fresh kir: SessionKey;
read_1(I,R, I,{ni}k(I,R) ); recv_1(I,R, I,{ni}k(I,R) );
send_2(R,I, {succ(ni),nr}k(I,R) ); send_2(R,I, {succ(ni),nr}k(I,R) );
read_3(I,R, {succ(nr)}k(I,R) ); recv_3(I,R, {succ(nr)}k(I,R) );
send_4(R,I, {kir,nr2}k(I,R) ); send_4(R,I, {kir,nr2}k(I,R) );
claim_R1(R,Secret,kir); claim_R1(R,Secret,kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);

4
gui/Protocols/ccitt509-1.spdl
View File

@ -19,7 +19,7 @@ protocol ccitt509-1(I,R)
fresh Na,Xa,Ya: Nonce; fresh Na,Xa,Ya: Nonce;
send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
# claim_2(I,Nisynch); # claim_2(I,Nisynch);
# This claim is useless as there are no preceding read events # This claim is useless as there are no preceding recv events
} }
role R role R
@ -27,7 +27,7 @@ protocol ccitt509-1(I,R)
var Ta: Timestamp; var Ta: Timestamp;
var Na,Xa,Ya: Nonce; var Na,Xa,Ya: Nonce;
read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); recv_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
claim_3(R,Nisynch); claim_3(R,Nisynch);
# There should also be Fresh Xa and Fresh Ya claims here # There should also be Fresh Xa and Fresh Ya claims here
} }

4
gui/Protocols/ccitt509-1c.spdl
View File

@ -18,7 +18,7 @@ protocol ccitt509-1c(I,R)
const Na,Xa,Ya: Nonce; const Na,Xa,Ya: Nonce;
send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
# claim_2(I,Nisynch); # claim_2(I,Nisynch);
# This claim is useless as there are no preceding read events # This claim is useless as there are no preceding receive events
} }
role R role R
@ -26,7 +26,7 @@ protocol ccitt509-1c(I,R)
var Ta: Timestamp; var Ta: Timestamp;
var Na,Xa,Ya: Nonce; var Na,Xa,Ya: Nonce;
read_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); recv_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
claim_3(R,Nisynch); claim_3(R,Nisynch);
# There should also be Fresh Xa and Fresh Ya claims here # There should also be Fresh Xa and Fresh Ya claims here
} }

6
gui/Protocols/ccitt509-3.spdl
View File

@ -19,7 +19,7 @@ protocol ccitt509-3(I,R)
fresh Na,Xa,Ya: Nonce; fresh Na,Xa,Ya: Nonce;
var Xb,Nb,Yb: Nonce; var Xb,Nb,Yb: Nonce;
send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
read_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); recv_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
send_3(I,R, I, {Nb}sk(I)); send_3(I,R, I, {Nb}sk(I));
claim_I1(I,Nisynch); claim_I1(I,Nisynch);
claim_I2(I,Secret,Ya); claim_I2(I,Secret,Ya);
@ -33,9 +33,9 @@ protocol ccitt509-3(I,R)
var Na,Xa,Ya: Nonce; var Na,Xa,Ya: Nonce;
fresh Xb,Yb,Nb: Nonce; fresh Xb,Yb,Nb: Nonce;
read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); recv_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
send_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); send_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
read_3(I,R, I, {Nb}sk(I)); recv_3(I,R, I, {Nb}sk(I));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
claim_R2(R,Secret,Ya); claim_R2(R,Secret,Ya);
claim_R3(R,Secret,Yb); claim_R3(R,Secret,Yb);

6
gui/Protocols/ccitt509-ban3.spdl
View File

@ -19,7 +19,7 @@ protocol ccitt509-ban3(I,R)
var Xb,Nb,Yb: Nonce; var Xb,Nb,Yb: Nonce;
send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
read_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); recv_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
send_3(I,R, I,{R, Nb}sk(I)); send_3(I,R, I,{R, Nb}sk(I));
claim_4(I,Nisynch); claim_4(I,Nisynch);
} }
@ -29,9 +29,9 @@ protocol ccitt509-ban3(I,R)
var Na,Xa,Ya: Nonce; var Na,Xa,Ya: Nonce;
const Xb,Yb,Nb: Nonce; const Xb,Yb,Nb: Nonce;
read_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); recv_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
send_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); send_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
read_3(I,R, I,{R, Nb}sk(I)); recv_3(I,R, I,{R, Nb}sk(I));
claim_5(R,Nisynch); claim_5(R,Nisynch);
# There should also be Fresh Xa and Fresh Ya claims here # There should also be Fresh Xa and Fresh Ya claims here
} }

12
gui/Protocols/denning-sacco-lowe.spdl
View File

@ -26,13 +26,13 @@ protocol denningSacco-Lowe(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,S, I,R ); send_1(I,S, I,R );
read_2(S,I, {R, Kir, T, W}k(I,S) ); recv_2(S,I, {R, Kir, T, W}k(I,S) );
send_3(I,R, W); send_3(I,R, W);
read_4(R,I, {Nr}Kir); recv_4(R,I, {Nr}Kir);
send_5(I,R, {{Nr}dec}Kir); send_5(I,R, {{Nr}dec}Kir);
claim_I1(I,Niagree); claim_I1(I,Niagree);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
claim_I3(I,Secret,Kir); claim_I3(I,SKR,Kir);
claim_I4(I,Empty,(Fresh,Kir)); claim_I4(I,Empty,(Fresh,Kir));
} }
@ -42,9 +42,9 @@ protocol denningSacco-Lowe(I,R,S)
var T: TimeStamp; var T: TimeStamp;
fresh Nr: Nonce; fresh Nr: Nonce;
read_3(I,R, {Kir,I,T}k(R,S)); recv_3(I,R, {Kir,I,T}k(R,S));
send_4(R,I, {Nr}Kir); send_4(R,I, {Nr}Kir);
read_5(I,R, {{Nr}dec}Kir); recv_5(I,R, {{Nr}dec}Kir);
claim_R1(R,Niagree); claim_R1(R,Niagree);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
claim_R3(R,Secret,Kir); claim_R3(R,Secret,Kir);
@ -57,7 +57,7 @@ protocol denningSacco-Lowe(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
fresh T: TimeStamp; fresh T: TimeStamp;
read_1(I,S, I,R ); recv_1(I,S, I,R );
send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
} }
} }

6
gui/Protocols/denning-sacco.spdl
View File

@ -20,7 +20,7 @@ protocol denningSacco(I,R,S)
var T: TimeStamp; var T: TimeStamp;
send_1(I,S, I,R ); send_1(I,S, I,R );
read_2(S,I, {R, Kir, T, W}k(I,S) ); recv_2(S,I, {R, Kir, T, W}k(I,S) );
send_3(I,R, W); send_3(I,R, W);
claim_I1(I,Niagree); claim_I1(I,Niagree);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
@ -33,7 +33,7 @@ protocol denningSacco(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
var T: TimeStamp; var T: TimeStamp;
read_3(I,R, {Kir,I,T}k(R,S)); recv_3(I,R, {Kir,I,T}k(R,S));
claim_R1(R,Niagree); claim_R1(R,Niagree);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
claim_R3(R,Secret,Kir); claim_R3(R,Secret,Kir);
@ -46,7 +46,7 @@ protocol denningSacco(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
fresh T: TimeStamp; fresh T: TimeStamp;
read_1(I,S, I,R ); recv_1(I,S, I,R );
send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
} }
} }

8
gui/Protocols/kaochow-v2.spdl
View File

@ -17,7 +17,7 @@ protocol kaochow-2(I,R,S)
var kir,kt: SessionKey; var kir,kt: SessionKey;
send_1 (I,S, I,R,ni); send_1 (I,S, I,R,ni);
read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr ); recv_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
send_4 (I,R, {nr,kir}kt ); send_4 (I,R, {nr,kir}kt );
claim_I1 (I, Nisynch); claim_I1 (I, Nisynch);
@ -33,9 +33,9 @@ protocol kaochow-2(I,R,S)
var kir,kt: SessionKey; var kir,kt: SessionKey;
var T: Ticket; var T: Ticket;
read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); recv_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) );
send_3 (R,I, R, T, {ni, kir}kt, nr ); send_3 (R,I, R, T, {ni, kir}kt, nr );
read_4 (I,R, {nr,kir}kt ); recv_4 (I,R, {nr,kir}kt );
claim_R1 (R, Nisynch); claim_R1 (R, Nisynch);
claim_R2 (R, Niagree); claim_R2 (R, Niagree);
@ -48,7 +48,7 @@ protocol kaochow-2(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh kir, kt: SessionKey; fresh kir, kt: SessionKey;
read_1 (I,S, I,R,ni); recv_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) );
} }
} }

8
gui/Protocols/kaochow-v3.spdl
View File

@ -20,7 +20,7 @@ protocol kaochow-3(I,R,S)
var T2: Ticket; var T2: Ticket;
send_1 (I,S, I,R,ni); send_1 (I,S, I,R,ni);
read_3 (R,I, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); recv_3 (R,I, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
send_4 (I,R, {nr,kir}kt, T2 ); send_4 (I,R, {nr,kir}kt, T2 );
claim_I1 (I, Nisynch); claim_I1 (I, Nisynch);
@ -37,9 +37,9 @@ protocol kaochow-3(I,R,S)
var T: Ticket; var T: Ticket;
fresh tr: TimeStamp; fresh tr: TimeStamp;
read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); recv_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) );
send_3 (R,I, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); send_3 (R,I, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) ); recv_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) );
claim_R1 (R, Nisynch); claim_R1 (R, Nisynch);
claim_R2 (R, Niagree); claim_R2 (R, Niagree);
@ -52,7 +52,7 @@ protocol kaochow-3(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh kir, kt: SessionKey; fresh kir, kt: SessionKey;
read_1 (I,S, I,R,ni); recv_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) );
} }
} }

8
gui/Protocols/kaochow.spdl
View File

@ -17,7 +17,7 @@ protocol kaochow(I,R,S)
var kir: SessionKey; var kir: SessionKey;
send_1 (I,S, I,R,ni); send_1 (I,S, I,R,ni);
read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr ); recv_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
send_4 (I,R, {nr}kir ); send_4 (I,R, {nr}kir );
claim_I1 (I, Nisynch); claim_I1 (I, Nisynch);
@ -33,9 +33,9 @@ protocol kaochow(I,R,S)
var kir: SessionKey; var kir: SessionKey;
var T; var T;
read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); recv_2 (S,R, T, { I,R,ni,kir }k(R,S) );
send_3 (R,I, T, {ni}kir, nr ); send_3 (R,I, T, {ni}kir, nr );
read_4 (I,R, {nr}kir ); recv_4 (I,R, {nr}kir );
claim_R1 (R, Nisynch); claim_R1 (R, Nisynch);
claim_R2 (R, Niagree); claim_R2 (R, Niagree);
@ -48,7 +48,7 @@ protocol kaochow(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh kir: SessionKey; fresh kir: SessionKey;
read_1 (I,S, I,R,ni); recv_1 (I,S, I,R,ni);
send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) ); send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) );
} }
} }

16
gui/Protocols/ksl-lowe.spdl
View File

@ -23,11 +23,11 @@ protocol ksl-Lowe(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, Ni, I); send_1(I,R, Ni, I);
read_4(R,I, { Ni,R,Kir }k(I,S), T, Nc, {R,Ni}Kir ); recv_4(R,I, { Ni,R,Kir }k(I,S), T, Nc, {R,Ni}Kir );
send_5(I,R, { Nc }Kir ); send_5(I,R, { Nc }Kir );
send_6(I,R, Mi,T ); send_6(I,R, Mi,T );
read_7(R,I, Mr,{Mi, R}Kir ); recv_7(R,I, Mr,{Mi, R}Kir );
send_8(I,R, {I,Mr}Kir ); send_8(I,R, {I,Mr}Kir );
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
@ -45,15 +45,15 @@ protocol ksl-Lowe(I,R,S)
fresh Tr: TimeStamp; fresh Tr: TimeStamp;
var T: Ticket; var T: Ticket;
read_1(I,R, Ni, I); recv_1(I,R, Ni, I);
send_2(R,S, Ni, I, Nr, R ); send_2(R,S, Ni, I, Nr, R );
read_3(S,R, { I, Nr, Kir }k(R,S), T ); recv_3(S,R, { I, Nr, Kir }k(R,S), T );
send_4(R,I, T, { Tr, I, Kir }Kbb, Nc, {R, Ni}Kir ); send_4(R,I, T, { Tr, I, Kir }Kbb, Nc, {R, Ni}Kir );
read_5(I,R, { Nc }Kir ); recv_5(I,R, { Nc }Kir );
read_6(I,R, Mi,{ Tr, I, Kir }Kbb ); recv_6(I,R, Mi,{ Tr, I, Kir }Kbb );
send_7(R,I, Mr,{Mi,R}Kir ); send_7(R,I, Mr,{Mi,R}Kir );
read_8(I,R, {I,Mr}Kir ); recv_8(I,R, {I,Mr}Kir );
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
@ -66,7 +66,7 @@ protocol ksl-Lowe(I,R,S)
var Ni, Nr: Nonce; var Ni, Nr: Nonce;
fresh Kir: SessionKey; fresh Kir: SessionKey;
read_2(R,S, Ni, I, Nr, R ); recv_2(R,S, Ni, I, Nr, R );
send_3(S,R, { I, Nr, Kir }k(R,S), { Ni,R,Kir }k(I,S) ); send_3(S,R, { I, Nr, Kir }k(R,S), { Ni,R,Kir }k(I,S) );
} }
} }

16
gui/Protocols/ksl.spdl
View File

@ -22,11 +22,11 @@ protocol ksl(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, Ni, I); send_1(I,R, Ni, I);
read_4(R,I, { Ni,R,Kir }k(I,S), T, Nc, {Ni}Kir ); recv_4(R,I, { Ni,R,Kir }k(I,S), T, Nc, {Ni}Kir );
send_5(I,R, { Nc }Kir ); send_5(I,R, { Nc }Kir );
send_6(I,R, Mi,T ); send_6(I,R, Mi,T );
read_7(R,I, Mr,{Mi}Kir ); recv_7(R,I, Mr,{Mi}Kir );
send_8(I,R, {Mr}Kir ); send_8(I,R, {Mr}Kir );
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
@ -44,15 +44,15 @@ protocol ksl(I,R,S)
fresh Tr: TimeStamp; fresh Tr: TimeStamp;
var T: Ticket; var T: Ticket;
read_1(I,R, Ni, I); recv_1(I,R, Ni, I);
send_2(R,S, Ni, I, Nr, R ); send_2(R,S, Ni, I, Nr, R );
read_3(S,R, { Nr, I, Kir }k(R,S), T ); recv_3(S,R, { Nr, I, Kir }k(R,S), T );
send_4(R,I, T, { Tr, I, Kir }Kbb, Nc, {Ni}Kir ); send_4(R,I, T, { Tr, I, Kir }Kbb, Nc, {Ni}Kir );
read_5(I,R, { Nc }Kir ); recv_5(I,R, { Nc }Kir );
read_6(I,R, Mi,{ Tr, I, Kir }Kbb ); recv_6(I,R, Mi,{ Tr, I, Kir }Kbb );
send_7(R,I, Mr,{Mi}Kir ); send_7(R,I, Mr,{Mi}Kir );
read_8(I,R, {Mr}Kir ); recv_8(I,R, {Mr}Kir );
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
@ -65,7 +65,7 @@ protocol ksl(I,R,S)
var Ni, Nr: Nonce; var Ni, Nr: Nonce;
fresh Kir: SessionKey; fresh Kir: SessionKey;
read_2(R,S, Ni, I, Nr, R ); recv_2(R,S, Ni, I, Nr, R );
send_3(S,R, { Nr, I, Kir }k(R,S), { Ni,R,Kir }k(I,S) ); send_3(S,R, { Nr, I, Kir }k(R,S), { Ni,R,Kir }k(I,S) );
} }
} }

14
gui/Protocols/needham-schroeder-lowe.spdl
View File

@ -18,9 +18,9 @@ protocol needhamschroederpk-Lowe(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,S, (I,R)); send_1(I,S, (I,R));
read_2(S,I, {pk(R), R}sk(S)); recv_2(S,I, {pk(R), R}sk(S));
send_3(I,R,{Ni,I}pk(R)); send_3(I,R,{Ni,I}pk(R));
read_6(R,I, {Ni,Nr,R}pk(I)); recv_6(R,I, {Ni,Nr,R}pk(I));
send_7(I,R, {Nr}pk(R)); send_7(I,R, {Nr}pk(R));
claim_I1(I,Secret,Ni); claim_I1(I,Secret,Ni);
claim_I2(I,Secret,Nr); claim_I2(I,Secret,Nr);
@ -32,11 +32,11 @@ protocol needhamschroederpk-Lowe(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
read_3(I,R,{Ni,I}pk(R)); recv_3(I,R,{Ni,I}pk(R));
send_4(R,S,(R,I)); send_4(R,S,(R,I));
read_5(S,R,{pk(I),I}sk(S)); recv_5(S,R,{pk(I),I}sk(S));
send_6(R,I,{Ni,Nr,R}pk(I)); send_6(R,I,{Ni,Nr,R}pk(I));
read_7(I,R,{Nr}pk(R)); recv_7(I,R,{Nr}pk(R));
claim_R1(R,Secret,Nr); claim_R1(R,Secret,Nr);
claim_R2(R,Secret,Ni); claim_R2(R,Secret,Ni);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
@ -44,9 +44,9 @@ protocol needhamschroederpk-Lowe(I,R,S)
role S role S
{ {
read_1(I,S,(I,R)); recv_1(I,S,(I,R));
send_2(S,I,{pk(R),R}sk(S)); send_2(S,I,{pk(R),R}sk(S));
read_4(R,S,(R,I)); recv_4(R,S,(R,I));
send_5(S,R,{pk(I),I}sk(S)); send_5(S,R,{pk(I),I}sk(S));
} }
} }

14
gui/Protocols/needham-schroeder-sk-amend.spdl
View File

@ -27,11 +27,11 @@ protocol needhamschroedersk-amend(I,R,S)
var T,T2: Ticket; var T,T2: Ticket;
send_1(I,R,I); send_1(I,R,I);
read_2(R,I,T); recv_2(R,I,T);
send_3(I,S,(I,R,Ni,T)); send_3(I,S,(I,R,Ni,T));
read_4(S,I, {Ni,R,Kir,T2}k(I,S)); recv_4(S,I, {Ni,R,Kir,T2}k(I,S));
send_5(I,R,T2); send_5(I,R,T2);
read_6(R,I,{Nr}Kir); recv_6(R,I,{Nr}Kir);
send_7(I,R,{{Nr}dec}Kir); send_7(I,R,{{Nr}dec}Kir);
claim_I2(I,Secret,Kir); claim_I2(I,Secret,Kir);
@ -44,11 +44,11 @@ protocol needhamschroedersk-amend(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
read_1(I,R,I); recv_1(I,R,I);
send_2(R,I,{I,Nr}k(R,S)); send_2(R,I,{I,Nr}k(R,S));
read_5(I,R,{Kir,Nr,I}k(R,S)); recv_5(I,R,{Kir,Nr,I}k(R,S));
send_6(R,I,{Nr}Kir); send_6(R,I,{Nr}Kir);
read_7(I,R,{{Nr}dec}Kir); recv_7(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Nr); claim_R1(R,Secret,Nr);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir)); claim_R4(R,Empty,(Fresh,Kir));
@ -58,7 +58,7 @@ protocol needhamschroedersk-amend(I,R,S)
{ {
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
fresh Kir: SessionKey; fresh Kir: SessionKey;
read_3(I,S,(I,R,Ni,{I,Nr}k(R,S))); recv_3(I,S,(I,R,Ni,{I,Nr}k(R,S)));
send_4(S,I,{Ni,R,Kir,{Kir,Nr,I}k(R,S)}k(I,S)); send_4(S,I,{Ni,R,Kir,{Kir,Nr,I}k(R,S)}k(I,S));
} }

10
gui/Protocols/needham-schroeder-sk.spdl
View File

@ -23,9 +23,9 @@ protocol needhamschroedersk(I,R,S)
var T: Ticket; var T: Ticket;
send_1(I,S,(I,R,Ni)); send_1(I,S,(I,R,Ni));
read_2(S,I, {Ni,R,Kir,T}k(I,S)); recv_2(S,I, {Ni,R,Kir,T}k(I,S));
send_3(I,R,T); send_3(I,R,T);
read_4(R,I,{Nr}Kir); recv_4(R,I,{Nr}Kir);
send_5(I,R,{{Nr}dec}Kir); send_5(I,R,{{Nr}dec}Kir);
claim_I2(I,Secret,Kir); claim_I2(I,Secret,Kir);
claim_I3(I,Nisynch); claim_I3(I,Nisynch);
@ -37,9 +37,9 @@ protocol needhamschroedersk(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
read_3(I,R,{Kir,I}k(R,S)); recv_3(I,R,{Kir,I}k(R,S));
send_4(R,I,{Nr}Kir); send_4(R,I,{Nr}Kir);
read_5(I,R,{{Nr}dec}Kir); recv_5(I,R,{{Nr}dec}Kir);
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
claim_R4(R,Empty,(Fresh,Kir)); claim_R4(R,Empty,(Fresh,Kir));
@ -49,7 +49,7 @@ protocol needhamschroedersk(I,R,S)
{ {
var Ni: Nonce; var Ni: Nonce;
fresh Kir: SessionKey; fresh Kir: SessionKey;
read_1(I,S,(I,R,Ni)); recv_1(I,S,(I,R,Ni));
send_2(S,I,{Ni,R,Kir,{Kir,I}k(R,S)}k(I,S)); send_2(S,I,{Ni,R,Kir,{Kir,I}k(R,S)}k(I,S));
} }
} }

14
gui/Protocols/needham-schroeder.spdl
View File

@ -18,9 +18,9 @@ protocol needhamschroederpk(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,S,(I,R)); send_1(I,S,(I,R));
read_2(S,I, {pk(R), R}sk(S)); recv_2(S,I, {pk(R), R}sk(S));
send_3(I,R,{Ni,I}pk(R)); send_3(I,R,{Ni,I}pk(R));
read_6(R,I, {Ni, Nr}pk(I)); recv_6(R,I, {Ni, Nr}pk(I));
send_7(I,R, {Nr}pk(R)); send_7(I,R, {Nr}pk(R));
claim_I1(I,Secret,Ni); claim_I1(I,Secret,Ni);
claim_I2(I,Secret,Nr); claim_I2(I,Secret,Nr);
@ -32,11 +32,11 @@ protocol needhamschroederpk(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var Ni: Nonce; var Ni: Nonce;
read_3(I,R,{Ni,I}pk(R)); recv_3(I,R,{Ni,I}pk(R));
send_4(R,S,(R,I)); send_4(R,S,(R,I));
read_5(S,R,{pk(I),I}sk(S)); recv_5(S,R,{pk(I),I}sk(S));
send_6(R,I,{Ni,Nr}pk(I)); send_6(R,I,{Ni,Nr}pk(I));
read_7(I,R,{Nr}pk(R)); recv_7(I,R,{Nr}pk(R));
claim_R1(R,Secret,Nr); claim_R1(R,Secret,Nr);
claim_R2(R,Secret,Ni); claim_R2(R,Secret,Ni);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
@ -44,9 +44,9 @@ protocol needhamschroederpk(I,R,S)
role S role S
{ {
read_1(I,S,(I,R)); recv_1(I,S,(I,R));
send_2(S,I,{pk(R),R}sk(S)); send_2(S,I,{pk(R),R}sk(S));
read_4(R,S,(R,I)); recv_4(R,S,(R,I));
send_5(S,R,{pk(I),I}sk(S)); send_5(S,R,{pk(I),I}sk(S));
} }
} }

14
gui/Protocols/neumannstub-guttman-hwang.spdl
View File

@ -26,7 +26,7 @@ protocol neustub-GuttmanHwang^Repeat(I,R,S)
fresh Tr: TimeStamp; fresh Tr: TimeStamp;
send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); send_5(I,R,Mi,{I,Kir,Tr}k(R,S));
read_6(R,I,{Mi,Mr}Kir); recv_6(R,I,{Mi,Mr}Kir);
send_7(I,R,{I,Mr}Kir); send_7(I,R,{I,Mr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
claim_I2(I,Niagree); claim_I2(I,Niagree);
@ -41,9 +41,9 @@ protocol neustub-GuttmanHwang^Repeat(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
var Mi: Nonce; var Mi: Nonce;
read_5(I,R,Mi,{I,Kir,Tr}k(R,S)); recv_5(I,R,Mi,{I,Kir,Tr}k(R,S));
send_6(R,I,{Mi,Mr}Kir); send_6(R,I,{Mi,Mr}Kir);
read_7(I,R,{I,Mr}Kir); recv_7(I,R,{I,Mr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
@ -65,7 +65,7 @@ protocol neustub-GuttmanHwang(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I, Ni); send_1(I,R, I, Ni);
read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); recv_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_!4(I,R,T,{Nr}Kir); send_!4(I,R,T,{Nr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
@ -82,9 +82,9 @@ protocol neustub-GuttmanHwang(I,R,S)
fresh Tb: TimeStamp; fresh Tb: TimeStamp;
var T: Ticket; var T: Ticket;
read_1(I,R, I, Ni); recv_1(I,R, I, Ni);
send_!2(R,S, R, {I, Ni, Tb ,Nr}k(R,S)); send_!2(R,S, R, {I, Ni, Tb ,Nr}k(R,S));
read_!4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); recv_!4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
@ -98,7 +98,7 @@ protocol neustub-GuttmanHwang(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Tb: TimeStamp; var Tb: TimeStamp;
read_!2(R,S, R, {I,Ni,Tb,Nr}k(R,S)); recv_!2(R,S, R, {I,Ni,Tb,Nr}k(R,S));
send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
} }
} }

14
gui/Protocols/neumannstub-guttman.spdl
View File

@ -26,7 +26,7 @@ protocol neustub^Repeat(I,R,S)
fresh Tr: TimeStamp; fresh Tr: TimeStamp;
send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); send_5(I,R,Mi,{I,Kir,Tr}k(R,S));
read_6(R,I,{Mi,Mr}Kir); recv_6(R,I,{Mi,Mr}Kir);
send_7(I,R,{I,Mr}Kir); send_7(I,R,{I,Mr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
claim_I2(I,Niagree); claim_I2(I,Niagree);
@ -41,9 +41,9 @@ protocol neustub^Repeat(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
var Mi: Nonce; var Mi: Nonce;
read_5(I,R,Mi,{I,Kir,Tr}k(R,S)); recv_5(I,R,Mi,{I,Kir,Tr}k(R,S));
send_6(R,I,{Mi,Mr}Kir); send_6(R,I,{Mi,Mr}Kir);
read_7(I,R,{I,Mr}Kir); recv_7(I,R,{I,Mr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
@ -65,7 +65,7 @@ protocol neustub(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I, Ni); send_1(I,R, I, Ni);
read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); recv_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_4(I,R,T,{Nr}Kir); send_4(I,R,T,{Nr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
@ -82,9 +82,9 @@ protocol neustub(I,R,S)
fresh Tb: TimeStamp; fresh Tb: TimeStamp;
var T: Ticket; var T: Ticket;
read_1(I,R, I, Ni); recv_1(I,R, I, Ni);
send_!2(R,S, R, {I, Ni, Tb}k(R,S),Nr); send_!2(R,S, R, {I, Ni, Tb}k(R,S),Nr);
read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); recv_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
@ -98,7 +98,7 @@ protocol neustub(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Tb: TimeStamp; var Tb: TimeStamp;
read_!2(R,S, R, {I,Ni,Tb}k(R,S), Nr); recv_!2(R,S, R, {I,Ni,Tb}k(R,S), Nr);
send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
} }
} }

14
gui/Protocols/neumannstub-hwang.spdl
View File

@ -25,10 +25,10 @@ protocol neustub-Hwang(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I, Ni); send_1(I,R, I, Ni);
read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); recv_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_4(I,R,T,{Nr}Kir); send_4(I,R,T,{Nr}Kir);
send_5(I,R,Mi,T); send_5(I,R,Mi,T);
read_6(R,I,Mr,{Mi}Kir); recv_6(R,I,Mr,{Mi}Kir);
send_7(I,R,{Mr}Kir); send_7(I,R,{Mr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
@ -45,12 +45,12 @@ protocol neustub-Hwang(I,R,S)
fresh Tb: TimeStamp; fresh Tb: TimeStamp;
var T: Ticket; var T: Ticket;
read_1(I,R, I, Ni); recv_1(I,R, I, Ni);
send_!2(R,S, R, {I, Ni, Tb, Nr}k(R,S)); send_!2(R,S, R, {I, Ni, Tb, Nr}k(R,S));
read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); recv_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
read_5(I,R,Mi,T); recv_5(I,R,Mi,T);
send_6(R,I,Mr,{Mi}Kir); send_6(R,I,Mr,{Mi}Kir);
read_7(I,R,{Mr}Kir); recv_7(I,R,{Mr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
@ -64,7 +64,7 @@ protocol neustub-Hwang(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Tb: TimeStamp; var Tb: TimeStamp;
read_!2(R,S, R, {I,Ni,Tb,Nr}k(R,S)); recv_!2(R,S, R, {I,Ni,Tb,Nr}k(R,S));
send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
} }
} }

14
gui/Protocols/neumannstub-keycompromise.spdl
View File

@ -26,7 +26,7 @@ protocol neustub^Repeat(I,R,S)
fresh Tr: TimeStamp; fresh Tr: TimeStamp;
send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); send_5(I,R,Mi,{I,Kir,Tr}k(R,S));
read_6(R,I,Mr,{Mi}Kir); recv_6(R,I,Mr,{Mi}Kir);
send_7(I,R,{Mr}Kir); send_7(I,R,{Mr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
claim_I2(I,Niagree); claim_I2(I,Niagree);
@ -41,9 +41,9 @@ protocol neustub^Repeat(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
var Mi: Nonce; var Mi: Nonce;
read_5(I,R,Mi,{I,Kir,Tr}k(R,S)); recv_5(I,R,Mi,{I,Kir,Tr}k(R,S));
send_6(R,I,Mr,{Mi}Kir); send_6(R,I,Mr,{Mi}Kir);
read_7(I,R,{Mr}Kir); recv_7(I,R,{Mr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
@ -65,7 +65,7 @@ protocol neustub(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I, Ni); send_1(I,R, I, Ni);
read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); recv_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_4(I,R,T,{Nr}Kir); send_4(I,R,T,{Nr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
@ -82,9 +82,9 @@ protocol neustub(I,R,S)
fresh Tb: TimeStamp; fresh Tb: TimeStamp;
var T: Ticket; var T: Ticket;
read_1(I,R, I, Ni); recv_1(I,R, I, Ni);
send_2(R,S, R, {I, Ni, Tb}k(R,S),Nr); send_2(R,S, R, {I, Ni, Tb}k(R,S),Nr);
read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); recv_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
@ -98,7 +98,7 @@ protocol neustub(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Tb: TimeStamp; var Tb: TimeStamp;
read_2(R,S, R, {I,Ni,Tb}k(R,S), Nr); recv_2(R,S, R, {I,Ni,Tb}k(R,S), Nr);
send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
} }
} }

14
gui/Protocols/neumannstub.spdl
View File

@ -23,7 +23,7 @@ protocol neustub^Repeat(I,R,S)
fresh Tr: TimeStamp; fresh Tr: TimeStamp;
send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); send_5(I,R,Mi,{I,Kir,Tr}k(R,S));
read_6(R,I,Mr,{Mi}Kir); recv_6(R,I,Mr,{Mi}Kir);
send_7(I,R,{Mr}Kir); send_7(I,R,{Mr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
claim_I2(I,Niagree); claim_I2(I,Niagree);
@ -37,9 +37,9 @@ protocol neustub^Repeat(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
var Mi: Nonce; var Mi: Nonce;
read_5(I,R,Mi,{I,Kir,Tr}k(R,S)); recv_5(I,R,Mi,{I,Kir,Tr}k(R,S));
send_6(R,I,Mr,{Mi}Kir); send_6(R,I,Mr,{Mi}Kir);
read_7(I,R,{Mr}Kir); recv_7(I,R,{Mr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
claim_R3(R,Nisynch); claim_R3(R,Nisynch);
@ -60,7 +60,7 @@ protocol neustub(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I, Ni); send_1(I,R, I, Ni);
read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); recv_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
send_4(I,R,T,{Nr}Kir); send_4(I,R,T,{Nr}Kir);
claim_I1(I,Secret, Kir); claim_I1(I,Secret, Kir);
@ -76,9 +76,9 @@ protocol neustub(I,R,S)
fresh Tb: TimeStamp; fresh Tb: TimeStamp;
var T: Ticket; var T: Ticket;
read_1(I,R, I, Ni); recv_1(I,R, I, Ni);
send_!2(R,S, R, {I, Ni, Tb}k(R,S),Nr); send_!2(R,S, R, {I, Ni, Tb}k(R,S),Nr);
read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); recv_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
claim_R1(R,Secret, Kir); claim_R1(R,Secret, Kir);
claim_R2(R,Niagree); claim_R2(R,Niagree);
@ -91,7 +91,7 @@ protocol neustub(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Tb: TimeStamp; var Tb: TimeStamp;
read_!2(R,S, R, {I,Ni,Tb}k(R,S), Nr); recv_!2(R,S, R, {I,Ni,Tb}k(R,S), Nr);
send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
} }
} }

8
gui/Protocols/otwayrees.spdl
View File

@ -19,7 +19,7 @@ protocol otwayrees(I,R,S)
var Kir : SessionKey; var Kir : SessionKey;
send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) ); send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) );
read_4(R,I, M,{Ni,Kir}k(I,S) ); recv_4(R,I, M,{Ni,Kir}k(I,S) );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
claim_I2(I, Nisynch); claim_I2(I, Nisynch);
@ -33,9 +33,9 @@ protocol otwayrees(I,R,S)
var Kir : SessionKey; var Kir : SessionKey;
var T1,T2: Ticket; var T1,T2: Ticket;
read_1(I,R, M,I,R, T1 ); recv_1(I,R, M,I,R, T1 );
send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) ); send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) );
read_3(S,R, M, T2, { Nr,Kir }k(R,S) ); recv_3(S,R, M, T2, { Nr,Kir }k(R,S) );
send_4(R,I, M, T2 ); send_4(R,I, M, T2 );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
@ -49,7 +49,7 @@ protocol otwayrees(I,R,S)
var M : String; var M : String;
fresh Kir : SessionKey; fresh Kir : SessionKey;
read_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) ); recv_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) );
send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) ); send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) );
} }
} }

6
gui/Protocols/smartright.spdl
View File

@ -25,7 +25,7 @@ protocol smartright(I,R)
var VoRi: Nonce; var VoRi: Nonce;
send_1(I,R, {VoKey,{CW}VoR}k(I,R)); send_1(I,R, {VoKey,{CW}VoR}k(I,R));
read_2(R,I, VoRi); recv_2(R,I, VoRi);
send_3(I,R, VoR, {{VoRi}hash}VoKey); send_3(I,R, VoR, {{VoRi}hash}VoKey);
} }
@ -36,9 +36,9 @@ protocol smartright(I,R)
var VoKey: SessionKey; var VoKey: SessionKey;
fresh VoRi: Nonce; fresh VoRi: Nonce;
read_1(I,R, {VoKey,T}k(I,R)); recv_1(I,R, {VoKey,T}k(I,R));
send_2(R,I, VoRi); send_2(R,I, VoRi);
read_3(I,R, VoR,{{VoRi}hash}VoKey); recv_3(I,R, VoR,{{VoRi}hash}VoKey);
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }

12
gui/Protocols/splice-as-cj.spdl
View File

@ -24,9 +24,9 @@ protocol spliceAS-CJ(I,R,S)
fresh L: LifeTime; fresh L: LifeTime;
send_1(I,S, I, R, N1 ); send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); recv_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
send_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); send_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
read_6(R,I, R, I, {{N2}inc}pk(I) ); recv_6(R,I, R, I, {{N2}inc}pk(I) );
claim_7(I, Secret, N2); claim_7(I, Secret, N2);
claim_9(I, Niagree); claim_9(I, Niagree);
@ -37,9 +37,9 @@ protocol spliceAS-CJ(I,R,S)
{ {
var N1,N3: Nonce; var N1,N3: Nonce;
read_1(I,S, I, R, N1 ); recv_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
read_4(R,S, R, I, N3 ); recv_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); send_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
} }
@ -53,9 +53,9 @@ protocol spliceAS-CJ(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh nr: Nonce; fresh nr: Nonce;
read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); recv_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 ); send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); recv_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
send_6(R,I, R, I, {{N2}inc}pk(I) ); send_6(R,I, R, I, {{N2}inc}pk(I) );
claim_8(R, Secret, N2); claim_8(R, Secret, N2);

12
gui/Protocols/splice-as-hc.spdl
View File

@ -19,9 +19,9 @@ protocol spliceAS-HC(I,R,S)
fresh L: LifeTime; fresh L: LifeTime;
send_1(I,S, I, R, N1 ); send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); recv_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
read_6(R,I, R, I, {R, {N2}inc}pk(I) ); recv_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_7(I, Secret, N2); claim_7(I, Secret, N2);
claim_9(I, Niagree); claim_9(I, Niagree);
@ -32,9 +32,9 @@ protocol spliceAS-HC(I,R,S)
{ {
var N1,N3: Nonce; var N1,N3: Nonce;
read_1(I,S, I, R, N1 ); recv_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) );
read_4(R,S, R, I, N3 ); recv_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); send_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) );
} }
@ -48,9 +48,9 @@ protocol spliceAS-HC(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh nr: Nonce; fresh nr: Nonce;
read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); recv_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 ); send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); recv_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) );
send_6(R,I, R, I, {R, {N2}inc}pk(I) ); send_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_8(R, Secret, N2); claim_8(R, Secret, N2);

12
gui/Protocols/splice-as.spdl
View File

@ -24,9 +24,9 @@ protocol spliceAS(I,R,S)
fresh L: LifeTime; fresh L: LifeTime;
send_1(I,S, I, R, N1 ); send_1(I,S, I, R, N1 );
read_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); recv_2(S,I, S, {S, I, N1, pk(R)}sk(S) );
send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
read_6(R,I, R, I, {R, {N2}inc}pk(I) ); recv_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_7(I, Secret, N2); claim_7(I, Secret, N2);
claim_9(I, Niagree); claim_9(I, Niagree);
@ -37,9 +37,9 @@ protocol spliceAS(I,R,S)
{ {
var N1,N3: Nonce; var N1,N3: Nonce;
read_1(I,S, I, R, N1 ); recv_1(I,S, I, R, N1 );
send_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); send_2(S,I, S, {S, I, N1, pk(R)}sk(S) );
read_4(R,S, R, I, N3 ); recv_4(R,S, R, I, N3 );
send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); send_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
} }
@ -53,9 +53,9 @@ protocol spliceAS(I,R,S)
var ni: Nonce; var ni: Nonce;
fresh nr: Nonce; fresh nr: Nonce;
read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); recv_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
send_4(R,S, R, I, N3 ); send_4(R,S, R, I, N3 );
read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); recv_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
send_6(R,I, R, I, {R, {N2}inc}pk(I) ); send_6(R,I, R, I, {R, {N2}inc}pk(I) );
claim_8(R, Secret, N2); claim_8(R, Secret, N2);

8
gui/Protocols/tmn.spdl
View File

@ -19,7 +19,7 @@ protocol tmn(I,R,S)
var Kr: SessionKey; var Kr: SessionKey;
send_1(I,S, R,{Ki}pk(S) ); send_1(I,S, R,{Ki}pk(S) );
read_4(S,I, R,{Kr}Ki ); recv_4(S,I, R,{Kr}Ki );
claim_I1(I,Secret,Kr); claim_I1(I,Secret,Kr);
claim_I2(I,Nisynch); claim_I2(I,Nisynch);
@ -30,7 +30,7 @@ protocol tmn(I,R,S)
{ {
fresh Kr: SessionKey; fresh Kr: SessionKey;
read_2(S,R, I ); recv_2(S,R, I );
send_3(R,S, I, { Kr }pk(S) ); send_3(R,S, I, { Kr }pk(S) );
claim_R1(R,Secret,Kr); claim_R1(R,Secret,Kr);
@ -42,9 +42,9 @@ protocol tmn(I,R,S)
{ {
var Ki,Kr: SessionKey; var Ki,Kr: SessionKey;
read_1(I,S, R,{Ki}pk(S) ); recv_1(I,S, R,{Ki}pk(S) );
send_2(S,R, I ); send_2(S,R, I );
read_3(R,S, I, { Kr }pk(S) ); recv_3(R,S, I, { Kr }pk(S) );
send_4(S,I, R,{Kr}Ki ); send_4(S,I, R,{Kr}Ki );
} }
} }

10
gui/Protocols/wmf-lowe.spdl
View File

@ -6,7 +6,7 @@
# Note: # Note:
# According to SPORE there are no known attacks on this protocol, scyther # According to SPORE there are no known attacks on this protocol, scyther
# finds one however this has to do with the unusual assumption that every # finds one however this has to do with the unusual assumption that every
# agent can recognise and will reject to read messages that it has created # agent can recognise and will reject to messages that it has created
# itself. # itself.
usertype SessionKey; usertype SessionKey;
@ -27,7 +27,7 @@ protocol wmf-Lowe(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,S, I, {Ti, R, Kir}k(I,S)); send_1(I,S, I, {Ti, R, Kir}k(I,S));
read_3(R,I,{Nr}Kir); recv_3(R,I,{Nr}Kir);
send_4(I,R,{{Nr}succ}Kir); send_4(I,R,{{Nr}succ}Kir);
claim_I1(I,Secret,Kir); claim_I1(I,Secret,Kir);
@ -41,9 +41,9 @@ protocol wmf-Lowe(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
fresh Nr: Nonce; fresh Nr: Nonce;
read_2(S,R, {Ts, I, Kir}k(R,S) ); recv_2(S,R, {Ts, I, Kir}k(R,S) );
send_3(R,I, {Nr}Kir); send_3(R,I, {Nr}Kir);
read_4(I,R, {{Nr}succ}Kir); recv_4(I,R, {{Nr}succ}Kir);
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
@ -56,7 +56,7 @@ protocol wmf-Lowe(I,R,S)
fresh Ts: TimeStamp; fresh Ts: TimeStamp;
var Ti: TimeStamp; var Ti: TimeStamp;
read_1(I,S, I,{Ti, R, Kir}k(I,S) ); recv_1(I,S, I,{Ti, R, Kir}k(I,S) );
send_2(S,R, {Ts, I, Kir}k(R,S)); send_2(S,R, {Ts, I, Kir}k(R,S));
} }
} }

4
gui/Protocols/wmf.spdl
View File

@ -34,7 +34,7 @@ protocol wmf(I,R,S)
var Ts: TimeStamp; var Ts: TimeStamp;
var Kir: SessionKey; var Kir: SessionKey;
read_2(S,R, {S, Ts, I, Kir}k(R,S) ); recv_2(S,R, {S, Ts, I, Kir}k(R,S) );
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
@ -47,7 +47,7 @@ protocol wmf(I,R,S)
fresh Ts: TimeStamp; fresh Ts: TimeStamp;
var Ti: TimeStamp; var Ti: TimeStamp;
read_1(I,S, I,{I, Ti, R, Kir}k(I,S) ); recv_1(I,S, I,{I, Ti, R, Kir}k(I,S) );
send_2(S,R, {S, Ts, I, Kir}k(R,S)); send_2(S,R, {S, Ts, I, Kir}k(R,S));
} }
} }

10
gui/Protocols/woo-lam-pi-1.spdl
View File

@ -11,7 +11,7 @@ protocol woolamPi-1(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); recv_2(R,I, Nr);
send_3(I,R, {I,R,Nr}k(I,S)); send_3(I,R, {I,R,Nr}k(I,S));
} }
@ -21,11 +21,11 @@ protocol woolamPi-1(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var T: Ticket; var T: Ticket;
read_1(I,R, I); recv_1(I,R, I);
send_2(R,I, Nr); send_2(R,I, Nr);
read_3(I,R, T); recv_3(I,R, T);
send_4(R,S, {I,R, T}k(R,S)); send_4(R,S, {I,R, T}k(R,S));
read_5(S,R, {I,R, Nr}k(R,S)); recv_5(S,R, {I,R, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
@ -34,7 +34,7 @@ protocol woolamPi-1(I,R,S)
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I,R, {I,R,Nr}k(I,S)}k(R,S)); recv_4(R,S, {I,R, {I,R,Nr}k(I,S)}k(R,S));
send_5(S,R, {I,R,Nr}k(R,S)); send_5(S,R, {I,R,Nr}k(R,S));
} }
} }

10
gui/Protocols/woo-lam-pi-2.spdl
View File

@ -11,7 +11,7 @@ protocol woolamPi-2(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); recv_2(R,I, Nr);
send_3(I,R, {I,Nr}k(I,S)); send_3(I,R, {I,Nr}k(I,S));
} }
@ -21,11 +21,11 @@ protocol woolamPi-2(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var T: Ticket; var T: Ticket;
read_1(I,R, I); recv_1(I,R, I);
send_2(R,I, Nr); send_2(R,I, Nr);
read_3(I,R, T); recv_3(I,R, T);
send_4(R,S, {I, T}k(R,S)); send_4(R,S, {I, T}k(R,S));
read_5(S,R, {I, Nr}k(R,S)); recv_5(S,R, {I, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
@ -34,7 +34,7 @@ protocol woolamPi-2(I,R,S)
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I, {I,Nr}k(I,S)}k(R,S)); recv_4(R,S, {I, {I,Nr}k(I,S)}k(R,S));
send_5(S,R, {I,Nr}k(R,S)); send_5(S,R, {I,Nr}k(R,S));
} }
} }

10
gui/Protocols/woo-lam-pi-3.spdl
View File

@ -11,7 +11,7 @@ protocol woolamPi-3(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); recv_2(R,I, Nr);
send_3(I,R, {Nr}k(I,S)); send_3(I,R, {Nr}k(I,S));
} }
@ -21,11 +21,11 @@ protocol woolamPi-3(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var T: Ticket; var T: Ticket;
read_1(I,R, I); recv_1(I,R, I);
send_2(R,I, Nr); send_2(R,I, Nr);
read_3(I,R, T); recv_3(I,R, T);
send_4(R,S, {I, T}k(R,S)); send_4(R,S, {I, T}k(R,S));
read_5(S,R, {I, Nr}k(R,S)); recv_5(S,R, {I, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
@ -34,7 +34,7 @@ protocol woolamPi-3(I,R,S)
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I, {Nr}k(I,S)}k(R,S)); recv_4(R,S, {I, {Nr}k(I,S)}k(R,S));
send_5(S,R, {I,Nr}k(R,S)); send_5(S,R, {I,Nr}k(R,S));
} }
} }

10
gui/Protocols/woo-lam-pi-f.spdl
View File

@ -11,7 +11,7 @@ protocol woolamPi-f(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); recv_2(R,I, Nr);
send_3(I,R, {I,R,Nr}k(I,S)); send_3(I,R, {I,R,Nr}k(I,S));
} }
@ -21,11 +21,11 @@ protocol woolamPi-f(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var T: Ticket; var T: Ticket;
read_1(I,R, I); recv_1(I,R, I);
send_2(R,I, Nr); send_2(R,I, Nr);
read_3(I,R, T); recv_3(I,R, T);
send_4(R,S, {I, R, Nr, T}k(R,S)); send_4(R,S, {I, R, Nr, T}k(R,S));
read_5(S,R, {I, R, Nr}k(R,S)); recv_5(S,R, {I, R, Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
@ -34,7 +34,7 @@ protocol woolamPi-f(I,R,S)
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S)); recv_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S));
send_5(S,R, {I, R, Nr}k(R,S)); send_5(S,R, {I, R, Nr}k(R,S));
} }
} }

10
gui/Protocols/woo-lam-pi.spdl
View File

@ -15,7 +15,7 @@ protocol woolamPi(I,R,S)
var Nr: Nonce; var Nr: Nonce;
send_1(I,R, I); send_1(I,R, I);
read_2(R,I, Nr); recv_2(R,I, Nr);
send_3(I,R, {Nr}k(I,S)); send_3(I,R, {Nr}k(I,S));
} }
@ -25,11 +25,11 @@ protocol woolamPi(I,R,S)
fresh Nr: Nonce; fresh Nr: Nonce;
var T: Ticket; var T: Ticket;
read_1(I,R, I); recv_1(I,R, I);
send_2(R,I, Nr); send_2(R,I, Nr);
read_3(I,R, T); recv_3(I,R, T);
send_4(R,S, {I, T}k(R,S)); send_4(R,S, {I, T}k(R,S));
read_5(S,R, {Nr}k(R,S)); recv_5(S,R, {Nr}k(R,S));
claim_R1(R,Nisynch); claim_R1(R,Nisynch);
} }
@ -38,7 +38,7 @@ protocol woolamPi(I,R,S)
{ {
var Nr: Nonce; var Nr: Nonce;
read_4(R,S, {I,{Nr}k(I,S)}k(R,S)); recv_4(R,S, {I,{Nr}k(I,S)}k(R,S));
send_5(S,R, {Nr}k(R,S)); send_5(S,R, {Nr}k(R,S));
} }
} }

16
gui/Protocols/woo-lam.spdl
View File

@ -19,9 +19,9 @@ protocol woolam(I,R,S)
var N2: Nonce; var N2: Nonce;
send_1(I,R, I, N1); send_1(I,R, I, N1);
read_2(R,I, R, N2); recv_2(R,I, R, N2);
send_3(I,R, {I, R, N1, N2}k(I,S)); send_3(I,R, {I, R, N1, N2}k(I,S));
read_6(R,I, {R, N1, N2, Kir}k(I,S), {N1,N2}Kir); recv_6(R,I, {R, N1, N2, Kir}k(I,S), {N1,N2}Kir);
send_7(I,R, {N2}Kir); send_7(I,R, {N2}Kir);
@ -37,13 +37,13 @@ protocol woolam(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
var T1,T2: Ticket; var T1,T2: Ticket;
read_1(I,R, I, N1); recv_1(I,R, I, N1);
send_2(R,I, R, N2); send_2(R,I, R, N2);
read_3(I,R, T1); recv_3(I,R, T1);
send_4(R,S, T1, {I, R, N1, N2}k(R,S)); send_4(R,S, T1, {I, R, N1, N2}k(R,S));
read_5(S,R, T2, {I, N1, N2, Kir}k(R,S)); recv_5(S,R, T2, {I, N1, N2, Kir}k(R,S));
send_6(R,I, T2, {N1,N2}Kir); send_6(R,I, T2, {N1,N2}Kir);
read_7(I,R, {N2}Kir); recv_7(I,R, {N2}Kir);
claim_R1(R,Secret,Kir); claim_R1(R,Secret,Kir);
claim_R2(R,Nisynch); claim_R2(R,Nisynch);
@ -55,8 +55,10 @@ protocol woolam(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var N1,N2: Nonce; var N1,N2: Nonce;
read_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S)); recv_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S));
send_5(S,R, {R, N1, N2, Kir}k(I,S), {I, N1, N2, Kir}k(R,S)); send_5(S,R, {R, N1, N2, Kir}k(I,S), {I, N1, N2, Kir}k(R,S));
} }
} }

8
gui/Protocols/yahalom-ban.spdl
View File

@ -18,7 +18,7 @@ protocol yahalom-BAN(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); recv_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
send_4(I,R, T, {Nr}Kir ); send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
@ -33,9 +33,9 @@ protocol yahalom-BAN(I,R,S)
var T: Ticket; var T: Ticket;
var Kir: SessionKey; var Kir: SessionKey;
read_1(I,R, I,Ni); recv_1(I,R, I,Ni);
send_2(R,S, R, Nr, {I,Ni}k(R,S) ); send_2(R,S, R, Nr, {I,Ni}k(R,S) );
read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir ); recv_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch); claim_R2(R, Nisynch);
@ -47,7 +47,7 @@ protocol yahalom-BAN(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, R, Nr, {I,Ni}k(R,S) ); recv_2(R,S, R, Nr, {I,Ni}k(R,S) );
send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,Kir,Nr}k(R,S) ); send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,Kir,Nr}k(R,S) );
} }
} }

10
gui/Protocols/yahalom-lowe.spdl
View File

@ -17,7 +17,7 @@ protocol yahalom-Lowe(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, {R,Kir,Ni,Nr}k(I,S) ); recv_3(S,I, {R,Kir,Ni,Nr}k(I,S) );
send_5(I,R, {I, R, S, Nr}Kir ); send_5(I,R, {I, R, S, Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
@ -30,10 +30,10 @@ protocol yahalom-Lowe(I,R,S)
var Ni: Nonce; var Ni: Nonce;
var Kir: SessionKey; var Kir: SessionKey;
read_1(I,R, I,Ni); recv_1(I,R, I,Ni);
send_2(R,S, {I,Ni,Nr}k(R,S) ); send_2(R,S, {I,Ni,Nr}k(R,S) );
read_4(S,R, {I,Kir}k(R,S)); recv_4(S,R, {I,Kir}k(R,S));
read_5(I,R, {I, R, S, Nr}Kir); recv_5(I,R, {I, R, S, Nr}Kir);
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch); claim_R2(R, Nisynch);
@ -44,7 +44,7 @@ protocol yahalom-Lowe(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, {I,Ni,Nr}k(R,S) ); recv_2(R,S, {I,Ni,Nr}k(R,S) );
send_3(S,I, {R,Kir,Ni,Nr}k(I,S)); send_3(S,I, {R,Kir,Ni,Nr}k(I,S));
send_4(S,R, {I,Kir}k(R,S)); send_4(S,R, {I,Kir}k(R,S));
} }

8
gui/Protocols/yahalom-paulson.spdl
View File

@ -20,7 +20,7 @@ protocol yahalom-Paulson(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); recv_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
send_4(I,R, T, {Nr}Kir ); send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
@ -35,9 +35,9 @@ protocol yahalom-Paulson(I,R,S)
var T: Ticket; var T: Ticket;
var Kir: SessionKey; var Kir: SessionKey;
read_1(I,R, I,Ni); recv_1(I,R, I,Ni);
send_2(R,S, R, Nr, {I,Ni}k(R,S) ); send_2(R,S, R, Nr, {I,Ni}k(R,S) );
read_4(I,R, {I,R, Kir, Nr}k(R,S) , {Nr}Kir ); recv_4(I,R, {I,R, Kir, Nr}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
claim_R2(R, Nisynch); claim_R2(R, Nisynch);
@ -49,7 +49,7 @@ protocol yahalom-Paulson(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, R, Nr, {I,Ni}k(R,S) ); recv_2(R,S, R, Nr, {I,Ni}k(R,S) );
send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,R,Kir,Nr}k(R,S) ); send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,R,Kir,Nr}k(R,S) );
} }
} }

8
gui/Protocols/yahalom.spdl
View File

@ -17,7 +17,7 @@ protocol yahalom(I,R,S)
var Kir: SessionKey; var Kir: SessionKey;
send_1(I,R, I,Ni); send_1(I,R, I,Ni);
read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T ); recv_3(S,I, {R,Kir,Ni,Nr}k(I,S), T );
send_4(I,R, T, {Nr}Kir ); send_4(I,R, T, {Nr}Kir );
claim_I1(I, Secret,Kir); claim_I1(I, Secret,Kir);
@ -30,9 +30,9 @@ protocol yahalom(I,R,S)
var T: Ticket; var T: Ticket;
var Kir: SessionKey; var Kir: SessionKey;
read_1(I,R, I,Ni); recv_1(I,R, I,Ni);
send_2(R,S, R, {I,Ni,Nr}k(R,S) ); send_2(R,S, R, {I,Ni,Nr}k(R,S) );
read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir ); recv_4(I,R, {I,Kir}k(R,S) , {Nr}Kir );
claim_R1(R, Secret,Kir); claim_R1(R, Secret,Kir);
} }
@ -42,7 +42,7 @@ protocol yahalom(I,R,S)
fresh Kir: SessionKey; fresh Kir: SessionKey;
var Ni,Nr: Nonce; var Ni,Nr: Nonce;
read_2(R,S, R, {I,Ni,Nr}k(R,S) ); recv_2(R,S, R, {I,Ni,Nr}k(R,S) );
send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) ); send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
claim(S, Secret, Ni); claim(S, Secret, Ni);