From d713ac400da8703e9fbb6f08de2b3aa24673b250 Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Thu, 26 Apr 2012 16:40:01 +0200 Subject: [PATCH] More 'read'->'recv' conversion. --- gui/Protocols/MultiProtocolAttacks/BKE.spdl | 6 +++--- .../andrew-ban-concrete.spdl | 12 ++++++------ .../MultiProtocolAttacks/andrew-ban.spdl | 8 ++++---- .../MultiProtocolAttacks/andrew-lowe-ban.spdl | 10 +++++----- gui/Protocols/MultiProtocolAttacks/boyd.spdl | 8 ++++---- .../MultiProtocolAttacks/ccitt509-ban3.spdl | 6 +++--- .../MultiProtocolAttacks/denning-sacco-lowe.spdl | 10 +++++----- .../MultiProtocolAttacks/denning-sacco.spdl | 6 +++--- .../MultiProtocolAttacks/gong-nonce-b.spdl | 10 +++++----- .../MultiProtocolAttacks/gong-nonce.spdl | 10 +++++----- .../MultiProtocolAttacks/isoiec11770-2-13.spdl | 8 ++++---- .../MultiProtocolAttacks/kaochow-v2.spdl | 8 ++++---- .../MultiProtocolAttacks/kaochow-v3.spdl | 8 ++++---- gui/Protocols/MultiProtocolAttacks/kaochow.spdl | 8 ++++---- gui/Protocols/MultiProtocolAttacks/ksl.spdl | 16 ++++++++-------- .../needham-schroeder-sk-amend.spdl | 14 +++++++------- .../needham-schroeder-sk.spdl | 10 +++++----- gui/Protocols/MultiProtocolAttacks/ns3.spdl | 6 +++--- gui/Protocols/MultiProtocolAttacks/nsl3.spdl | 6 +++--- .../MultiProtocolAttacks/otwayrees.spdl | 8 ++++---- gui/Protocols/MultiProtocolAttacks/soph.spdl | 4 ++-- .../MultiProtocolAttacks/splice-as-cj.spdl | 12 ++++++------ .../MultiProtocolAttacks/splice-as-hc.spdl | 12 ++++++------ .../MultiProtocolAttacks/splice-as.spdl | 12 ++++++------ gui/Protocols/MultiProtocolAttacks/tmn.spdl | 8 ++++---- .../MultiProtocolAttacks/wmf-brutus.spdl | 4 ++-- gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl | 10 +++++----- gui/Protocols/MultiProtocolAttacks/wmf.spdl | 4 ++-- .../MultiProtocolAttacks/woo-lam-pi-1.spdl | 10 +++++----- .../MultiProtocolAttacks/woo-lam-pi-2.spdl | 10 +++++----- .../MultiProtocolAttacks/woo-lam-pi-3.spdl | 10 +++++----- .../MultiProtocolAttacks/woo-lam-pi-f.spdl | 10 +++++----- gui/Protocols/MultiProtocolAttacks/woo-lam.spdl | 14 +++++++------- .../yahalom-ban-paulson-modified.spdl | 8 ++++---- .../yahalom-ban-paulson.spdl | 8 ++++---- .../MultiProtocolAttacks/yahalom-ban.spdl | 8 ++++---- .../MultiProtocolAttacks/yahalom-lowe.spdl | 10 +++++----- gui/Protocols/MultiProtocolAttacks/yahalom.spdl | 8 ++++---- gui/Protocols/andrew-ban-concrete.spdl | 13 ++++++------- gui/Protocols/andrew-ban.spdl | 8 ++++---- gui/Protocols/andrew-lowe-ban.spdl | 10 +++++----- gui/Protocols/andrew.spdl | 9 ++++----- gui/Protocols/ccitt509-1.spdl | 4 ++-- gui/Protocols/ccitt509-1c.spdl | 4 ++-- gui/Protocols/ccitt509-3.spdl | 6 +++--- gui/Protocols/ccitt509-ban3.spdl | 6 +++--- gui/Protocols/denning-sacco-lowe.spdl | 12 ++++++------ gui/Protocols/denning-sacco.spdl | 6 +++--- gui/Protocols/kaochow-v2.spdl | 8 ++++---- gui/Protocols/kaochow-v3.spdl | 8 ++++---- gui/Protocols/kaochow.spdl | 8 ++++---- gui/Protocols/ksl-lowe.spdl | 16 ++++++++-------- gui/Protocols/ksl.spdl | 16 ++++++++-------- gui/Protocols/needham-schroeder-lowe.spdl | 14 +++++++------- gui/Protocols/needham-schroeder-sk-amend.spdl | 14 +++++++------- gui/Protocols/needham-schroeder-sk.spdl | 10 +++++----- gui/Protocols/needham-schroeder.spdl | 14 +++++++------- gui/Protocols/neumannstub-guttman-hwang.spdl | 14 +++++++------- gui/Protocols/neumannstub-guttman.spdl | 14 +++++++------- gui/Protocols/neumannstub-hwang.spdl | 14 +++++++------- gui/Protocols/neumannstub-keycompromise.spdl | 14 +++++++------- gui/Protocols/neumannstub.spdl | 14 +++++++------- gui/Protocols/otwayrees.spdl | 8 ++++---- gui/Protocols/smartright.spdl | 6 +++--- gui/Protocols/splice-as-cj.spdl | 12 ++++++------ gui/Protocols/splice-as-hc.spdl | 12 ++++++------ gui/Protocols/splice-as.spdl | 12 ++++++------ gui/Protocols/tmn.spdl | 8 ++++---- gui/Protocols/wmf-lowe.spdl | 10 +++++----- gui/Protocols/wmf.spdl | 4 ++-- gui/Protocols/woo-lam-pi-1.spdl | 10 +++++----- gui/Protocols/woo-lam-pi-2.spdl | 10 +++++----- gui/Protocols/woo-lam-pi-3.spdl | 10 +++++----- gui/Protocols/woo-lam-pi-f.spdl | 10 +++++----- gui/Protocols/woo-lam-pi.spdl | 10 +++++----- gui/Protocols/woo-lam.spdl | 16 +++++++++------- gui/Protocols/yahalom-ban.spdl | 8 ++++---- gui/Protocols/yahalom-lowe.spdl | 10 +++++----- gui/Protocols/yahalom-paulson.spdl | 8 ++++---- gui/Protocols/yahalom.spdl | 8 ++++---- 80 files changed, 384 insertions(+), 384 deletions(-) diff --git a/gui/Protocols/MultiProtocolAttacks/BKE.spdl b/gui/Protocols/MultiProtocolAttacks/BKE.spdl index 1afa87f..8342bd6 100644 --- a/gui/Protocols/MultiProtocolAttacks/BKE.spdl +++ b/gui/Protocols/MultiProtocolAttacks/BKE.spdl @@ -15,7 +15,7 @@ protocol bke(I,R) var kir: SessionKey; 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 ); claim_4 (I, Secret, kir ); //claim_5 (I, Niagree ); @@ -28,9 +28,9 @@ protocol bke(I,R) fresh nr: Nonce; 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) ); - read_3 (I,R, { hash(nr) }kir ); + recv_3 (I,R, { hash(nr) }kir ); claim_7 (R, Secret, kir ); //claim_8 (R, Niagree ); //claim_9 (R, Nisynch ); diff --git a/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl b/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl index c5389b3..48f52d8 100644 --- a/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl +++ b/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl @@ -10,7 +10,7 @@ # a given term crypted with k(I,R) with k(R,I) # # 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 # completely fresh and can therefore always be replaced by an arbitrary value # created by the intruder) which are not considered in SPORE @@ -26,7 +26,7 @@ protocol @swapkey(X) { var I,R: Agent; 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)); } } @@ -41,12 +41,12 @@ protocol andrew-Concrete(I,R) var kir: SessionKey; 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); claim_I1(I,Secret,kir); claim_I2(I,Nisynch); claim_I3(I,Empty,(Fresh,kir)); - read_6(R,I, nr); + recv_6(R,I, nr); } role R @@ -55,9 +55,9 @@ protocol andrew-Concrete(I,R) fresh nr: Nonce; fresh kir: SessionKey; - read_1(I,R, I,ni ); + recv_1(I,R, I,ni ); 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); claim_R1(R,Secret,kir); claim_R2(R,Nisynch); diff --git a/gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl b/gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl index 51f140e..5118604 100644 --- a/gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl +++ b/gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl @@ -24,9 +24,9 @@ protocol andrew-Ban(I,R) var kir: SessionKey; 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) ); - 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_I2(I,Niagree); claim_I3(I,Secret, kir); @@ -39,9 +39,9 @@ protocol andrew-Ban(I,R) fresh nr,nr2: Nonce; 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) ); - 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) ); claim_R1(R,Nisynch); claim_R2(R,Niagree); diff --git a/gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl b/gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl index bb00132..04e15f2 100644 --- a/gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl +++ b/gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl @@ -9,7 +9,7 @@ # So it is possile that certain attacks that use this property are not found # # 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 # completely fresh and can therefore always be replaced by an arbitrary value # created by the intruder) which are not considered in SPORE @@ -31,12 +31,12 @@ protocol andrew-LoweBan(I,R) var kir: SessionKey; 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 ); claim_I1(I,Nisynch); claim_I2(I,Secret, kir); claim_I3(I,Empty, (Fresh,kir)); - read_4(R,I, nr ); + recv_4(R,I, nr ); } role R @@ -45,9 +45,9 @@ protocol andrew-LoweBan(I,R) fresh nr: Nonce; 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) ); - read_3(I,R, {ni}kir ); + recv_3(I,R, {ni}kir ); send_4(R,I, nr ); claim_R1(R,Nisynch); claim_R2(R,Secret, kir); diff --git a/gui/Protocols/MultiProtocolAttacks/boyd.spdl b/gui/Protocols/MultiProtocolAttacks/boyd.spdl index a5b915d..0a9c755 100644 --- a/gui/Protocols/MultiProtocolAttacks/boyd.spdl +++ b/gui/Protocols/MultiProtocolAttacks/boyd.spdl @@ -25,7 +25,7 @@ protocol boyd(I,R,S) var ks: Macseed; 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)) ); claim_6 (I, Secret, m(ks,ni,nr) ); @@ -37,9 +37,9 @@ protocol boyd(I,R,S) fresh nr: Nonce; 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 ); - 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)); } @@ -49,7 +49,7 @@ protocol boyd(I,R,S) var ni,nr: Nonce; 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 ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl b/gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl index c633587..bdf146d 100644 --- a/gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl +++ b/gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl @@ -19,7 +19,7 @@ protocol ccitt509-ban3(I,R) var Xb,Nb,Yb: Nonce; 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)); claim_4(I,Nisynch); } @@ -29,9 +29,9 @@ protocol ccitt509-ban3(I,R) var Na,Xa,Ya: 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)); - read_3(I,R, I,{R, Nb}sk(I)); + recv_3(I,R, I,{R, Nb}sk(I)); claim_5(R,Nisynch); # There should also be Fresh Xa and Fresh Ya claims here } diff --git a/gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl b/gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl index 213c80d..d5c3182 100644 --- a/gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl +++ b/gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl @@ -26,9 +26,9 @@ protocol denningSacco-Lowe(I,R,S) var Nr: Nonce; 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); - read_4(R,I, {Nr}Kir); + recv_4(R,I, {Nr}Kir); send_5(I,R, {{Nr}dec}Kir); claim_I1(I,Niagree); claim_I2(I,Nisynch); @@ -42,9 +42,9 @@ protocol denningSacco-Lowe(I,R,S) var T: TimeStamp; 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); - read_5(I,R, {{Nr}dec}Kir); + recv_5(I,R, {{Nr}dec}Kir); claim_R1(R,Niagree); claim_R2(R,Nisynch); claim_R3(R,Secret,Kir); @@ -57,7 +57,7 @@ protocol denningSacco-Lowe(I,R,S) fresh Kir: SessionKey; 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)); claim_x(S, Secret, Kir); } diff --git a/gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl b/gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl index 8bcf846..00167e9 100644 --- a/gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl +++ b/gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl @@ -20,7 +20,7 @@ protocol denningSacco(I,R,S) var T: TimeStamp; 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); claim_I1(I,Niagree); claim_I2(I,Nisynch); @@ -33,7 +33,7 @@ protocol denningSacco(I,R,S) var Kir: SessionKey; 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_R2(R,Nisynch); claim_R3(R,Secret,Kir); @@ -46,7 +46,7 @@ protocol denningSacco(I,R,S) fresh Kir: SessionKey; 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)); } } diff --git a/gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl b/gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl index 6b9943e..09bde6d 100644 --- a/gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl +++ b/gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl @@ -19,7 +19,7 @@ protocol gongnonceb(I,R,S) var kr: Keypart; 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) ); claim_6 (I, Secret, ki); @@ -35,9 +35,9 @@ protocol gongnonceb(I,R,S) fresh kr: 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 ); - 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_11 (R, Secret, kr); @@ -51,9 +51,9 @@ protocol gongnonceb(I,R,S) var ki,kr: Keypart; 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 ); - 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 ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl b/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl index 9040e40..594e1b9 100644 --- a/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl +++ b/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl @@ -17,7 +17,7 @@ protocol gongnonce(I,R,S) var kr: Keypart; 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) ); claim_6 (I, Secret, ki); @@ -33,9 +33,9 @@ protocol gongnonce(I,R,S) fresh kr: 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)); - 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_11 (R, Secret, kr); @@ -48,9 +48,9 @@ protocol gongnonce(I,R,S) var ni,nr: Nonce; 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); - 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl b/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl index a8eac3b..5db1533 100644 --- a/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl +++ b/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl @@ -10,7 +10,7 @@ protocol isoiec11770213(I,R,S) var kir: Sessionkey; 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); } @@ -22,9 +22,9 @@ protocol isoiec11770213(I,R,S) fresh kir: Sessionkey; var T; - read_1 (I,R, ni); + recv_1 (I,R, ni); 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 ); claim_6 (R, Secret, kir); @@ -35,7 +35,7 @@ protocol isoiec11770213(I,R,S) var ni,nr: Nonce; 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl b/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl index be1c4c8..638a54b 100644 --- a/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl +++ b/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl @@ -17,7 +17,7 @@ protocol kaochow-2(I,R,S) var kir,kt: SessionKey; 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 ); claim_I1 (I, Nisynch); @@ -33,9 +33,9 @@ protocol kaochow-2(I,R,S) var kir,kt: SessionKey; 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 ); - read_4 (I,R, {nr,kir}kt ); + recv_4 (I,R, {nr,kir}kt ); claim_R1 (R, Nisynch); claim_R2 (R, Niagree); @@ -48,7 +48,7 @@ protocol kaochow-2(I,R,S) var ni: Nonce; 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl b/gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl index 0bfc94a..88cef24 100644 --- a/gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl +++ b/gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl @@ -20,7 +20,7 @@ protocol kaochow-3(I,R,S) var T2: Ticket; 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 ); claim_I1 (I, Nisynch); @@ -37,9 +37,9 @@ protocol kaochow-3(I,R,S) var T: Ticket; 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) ); - 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_R2 (R, Niagree); @@ -52,7 +52,7 @@ protocol kaochow-3(I,R,S) var ni: Nonce; 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/kaochow.spdl b/gui/Protocols/MultiProtocolAttacks/kaochow.spdl index 4126ec3..1c6c827 100644 --- a/gui/Protocols/MultiProtocolAttacks/kaochow.spdl +++ b/gui/Protocols/MultiProtocolAttacks/kaochow.spdl @@ -17,7 +17,7 @@ protocol kaochow(I,R,S) var kir: SessionKey; 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 ); claim_I1 (I, Nisynch); @@ -33,9 +33,9 @@ protocol kaochow(I,R,S) var kir: SessionKey; 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 ); - read_4 (I,R, {nr}kir ); + recv_4 (I,R, {nr}kir ); claim_R1 (R, Nisynch); claim_R2 (R, Niagree); @@ -48,7 +48,7 @@ protocol kaochow(I,R,S) var ni: Nonce; 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/ksl.spdl b/gui/Protocols/MultiProtocolAttacks/ksl.spdl index 58856fc..3595cf2 100644 --- a/gui/Protocols/MultiProtocolAttacks/ksl.spdl +++ b/gui/Protocols/MultiProtocolAttacks/ksl.spdl @@ -24,11 +24,11 @@ protocol ksl(I,R,S) var Kir: SessionKey; 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_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 ); claim_I1(I,Secret, Kir); @@ -46,15 +46,15 @@ protocol ksl(I,R,S) fresh Tr: TimeStamp; var T: Ticket; - read_1(I,R, Ni, I); + recv_1(I,R, Ni, I); 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 ); - 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 ); - read_8(I,R, {Mr}Kir ); + recv_8(I,R, {Mr}Kir ); claim_R1(R,Secret, Kir); claim_R2(R,Niagree); @@ -67,7 +67,7 @@ protocol ksl(I,R,S) var Ni, Nr: Nonce; 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl index 7c96390..189093d 100644 --- a/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl +++ b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl @@ -27,11 +27,11 @@ protocol needhamschroedersk-amend(I,R,S) var T,T2: Ticket; send_1(I,R,I); - read_2(R,I,T); + recv_2(R,I,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); - read_6(R,I,{Nr}Kir); + recv_6(R,I,{Nr}Kir); send_7(I,R,{{Nr}dec}Kir); claim_I2(I,Secret,Kir); @@ -44,11 +44,11 @@ protocol needhamschroedersk-amend(I,R,S) fresh Nr: Nonce; var Kir: SessionKey; - read_1(I,R,I); + recv_1(I,R,I); 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); - read_7(I,R,{{Nr}dec}Kir); + recv_7(I,R,{{Nr}dec}Kir); claim_R1(R,Secret,Nr); claim_R3(R,Nisynch); claim_R4(R,Empty,(Fresh,Kir)); @@ -58,7 +58,7 @@ protocol needhamschroedersk-amend(I,R,S) { var Ni,Nr: Nonce; 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)); } diff --git a/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl index 50c87d4..71a7e6c 100644 --- a/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl +++ b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl @@ -23,9 +23,9 @@ protocol needhamschroedersk(I,R,S) var T: Ticket; 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); - read_4(R,I,{Nr}Kir); + recv_4(R,I,{Nr}Kir); send_5(I,R,{{Nr}dec}Kir); claim_I2(I,Secret,Kir); claim_I3(I,Nisynch); @@ -37,9 +37,9 @@ protocol needhamschroedersk(I,R,S) fresh Nr: Nonce; 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); - read_5(I,R,{{Nr}dec}Kir); + recv_5(I,R,{{Nr}dec}Kir); claim_R1(R,Secret,Kir); claim_R3(R,Nisynch); claim_R4(R,Empty,(Fresh,Kir)); @@ -49,7 +49,7 @@ protocol needhamschroedersk(I,R,S) { var Ni: Nonce; 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)); } } diff --git a/gui/Protocols/MultiProtocolAttacks/ns3.spdl b/gui/Protocols/MultiProtocolAttacks/ns3.spdl index b860cbf..b83afa7 100644 --- a/gui/Protocols/MultiProtocolAttacks/ns3.spdl +++ b/gui/Protocols/MultiProtocolAttacks/ns3.spdl @@ -12,7 +12,7 @@ protocol ns3(I,R) var nr: Nonce; 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) ); claim_i1(I,Secret,ni); @@ -27,9 +27,9 @@ protocol ns3(I,R) var ni: 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) ); - read_3(I,R, {nr}pk(R) ); + recv_3(I,R, {nr}pk(R) ); claim_r1(R,Secret,ni); claim_r2(R,Secret,nr); diff --git a/gui/Protocols/MultiProtocolAttacks/nsl3.spdl b/gui/Protocols/MultiProtocolAttacks/nsl3.spdl index af99579..a4bfef5 100644 --- a/gui/Protocols/MultiProtocolAttacks/nsl3.spdl +++ b/gui/Protocols/MultiProtocolAttacks/nsl3.spdl @@ -12,7 +12,7 @@ protocol nsl3(I,R) var nr: Nonce; 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) ); claim_i1(I,Secret,ni); @@ -26,9 +26,9 @@ protocol nsl3(I,R) var ni: 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) ); - read_3(I,R, {nr}pk(R) ); + recv_3(I,R, {nr}pk(R) ); claim_r1(R,Secret,ni); claim_r2(R,Secret,nr); diff --git a/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl b/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl index 64b99dc..bed12ad 100644 --- a/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl +++ b/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl @@ -19,7 +19,7 @@ protocol otwayrees(I,R,S) var Kir : SessionKey; 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_I2(I, Nisynch); @@ -33,9 +33,9 @@ protocol otwayrees(I,R,S) var Kir : SessionKey; 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) ); - 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 ); claim_R1(R, Secret,Kir); @@ -49,7 +49,7 @@ protocol otwayrees(I,R,S) var M : String; 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/soph.spdl b/gui/Protocols/MultiProtocolAttacks/soph.spdl index c6e3223..3b10851 100644 --- a/gui/Protocols/MultiProtocolAttacks/soph.spdl +++ b/gui/Protocols/MultiProtocolAttacks/soph.spdl @@ -6,7 +6,7 @@ protocol soph(I,R) fresh ni: Nonce; send_1(I,R, {I,ni}pk(R) ); - read_2(R,I, ni ); + recv_2(R,I, ni ); claim_3(I,Niagree); } @@ -14,7 +14,7 @@ protocol soph(I,R) { var ni: Nonce; - read_1(I,R, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}pk(R) ); send_2(R,I, ni ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl b/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl index 87960b3..b393294 100644 --- a/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl +++ b/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl @@ -24,9 +24,9 @@ protocol spliceAS-CJ(I,R,S) fresh L: LifeTime; 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) ); - 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_9(I, Niagree); @@ -37,9 +37,9 @@ protocol spliceAS-CJ(I,R,S) { 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) ); - 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) ); } @@ -53,9 +53,9 @@ protocol spliceAS-CJ(I,R,S) var ni: 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 ); - 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) ); claim_8(R, Secret, N2); diff --git a/gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl b/gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl index 858e02a..2f975ad 100644 --- a/gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl +++ b/gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl @@ -19,9 +19,9 @@ protocol spliceAS-HC(I,R,S) fresh L: LifeTime; 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) ); - 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_9(I, Niagree); @@ -32,9 +32,9 @@ protocol spliceAS-HC(I,R,S) { 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) ); - 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) ); } @@ -48,9 +48,9 @@ protocol spliceAS-HC(I,R,S) var ni: 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 ); - 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) ); claim_8(R, Secret, N2); diff --git a/gui/Protocols/MultiProtocolAttacks/splice-as.spdl b/gui/Protocols/MultiProtocolAttacks/splice-as.spdl index 9890adb..b1d8e18 100644 --- a/gui/Protocols/MultiProtocolAttacks/splice-as.spdl +++ b/gui/Protocols/MultiProtocolAttacks/splice-as.spdl @@ -24,9 +24,9 @@ protocol spliceAS(I,R,S) fresh L: LifeTime; 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) ); - 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_9(I, Niagree); @@ -37,9 +37,9 @@ protocol spliceAS(I,R,S) { 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) ); - 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) ); } @@ -53,9 +53,9 @@ protocol spliceAS(I,R,S) var ni: 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 ); - 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) ); claim_8(R, Secret, N2); diff --git a/gui/Protocols/MultiProtocolAttacks/tmn.spdl b/gui/Protocols/MultiProtocolAttacks/tmn.spdl index 267d30f..c6fb55f 100644 --- a/gui/Protocols/MultiProtocolAttacks/tmn.spdl +++ b/gui/Protocols/MultiProtocolAttacks/tmn.spdl @@ -19,7 +19,7 @@ protocol tmn(I,R,S) var Kr: SessionKey; 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_I2(I,Nisynch); @@ -30,7 +30,7 @@ protocol tmn(I,R,S) { fresh Kr: SessionKey; - read_2(S,R, I ); + recv_2(S,R, I ); send_3(R,S, I, { Kr }pk(S) ); claim_R1(R,Secret,Kr); @@ -42,9 +42,9 @@ protocol tmn(I,R,S) { 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 ); - read_3(R,S, I, { Kr }pk(S) ); + recv_3(R,S, I, { Kr }pk(S) ); send_4(S,I, R,{Kr}Ki ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl b/gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl index 618acef..c22bdcc 100644 --- a/gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl +++ b/gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl @@ -16,7 +16,7 @@ protocol wmfbrutus(A,B,S) { 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); } @@ -25,7 +25,7 @@ protocol wmfbrutus(A,B,S) { 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl b/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl index 61c5b7f..0e0de87 100644 --- a/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl +++ b/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl @@ -6,7 +6,7 @@ # Note: # 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 -# 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. usertype SessionKey; @@ -27,7 +27,7 @@ protocol wmf-Lowe(I,R,S) var Nr: Nonce; 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); claim_I1(I,Secret,Kir); @@ -41,9 +41,9 @@ protocol wmf-Lowe(I,R,S) var Kir: SessionKey; 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); - read_4(I,R, {{Nr}succ}Kir); + recv_4(I,R, {{Nr}succ}Kir); claim_R1(R,Secret,Kir); claim_R2(R,Nisynch); @@ -56,7 +56,7 @@ protocol wmf-Lowe(I,R,S) fresh Ts: 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)); } } diff --git a/gui/Protocols/MultiProtocolAttacks/wmf.spdl b/gui/Protocols/MultiProtocolAttacks/wmf.spdl index 4c787a8..758843a 100644 --- a/gui/Protocols/MultiProtocolAttacks/wmf.spdl +++ b/gui/Protocols/MultiProtocolAttacks/wmf.spdl @@ -34,7 +34,7 @@ protocol wmf(I,R,S) var Ts: TimeStamp; 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_R2(R,Nisynch); @@ -47,7 +47,7 @@ protocol wmf(I,R,S) fresh Ts: 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)); } } diff --git a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl index d38c837..7e4e09d 100644 --- a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl @@ -11,7 +11,7 @@ protocol woolamPi-1(I,R,S) var Nr: Nonce; 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)); } @@ -21,11 +21,11 @@ protocol woolamPi-1(I,R,S) fresh Nr: Nonce; var T: Ticket; - read_1(I,R, I); + recv_1(I,R, I); 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)); - read_5(S,R, {I,R, Nr}k(R,S)); + recv_5(S,R, {I,R, Nr}k(R,S)); claim_R1(R,Nisynch); } @@ -34,7 +34,7 @@ protocol woolamPi-1(I,R,S) { 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)); } } diff --git a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl index 10b61d4..5d767d6 100644 --- a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl @@ -11,7 +11,7 @@ protocol woolamPi-2(I,R,S) var Nr: Nonce; send_1(I,R, I); - read_2(R,I, Nr); + recv_2(R,I, Nr); send_3(I,R, {I,Nr}k(I,S)); } @@ -21,11 +21,11 @@ protocol woolamPi-2(I,R,S) fresh Nr: Nonce; var T: Ticket; - read_1(I,R, I); + recv_1(I,R, I); send_2(R,I, Nr); - read_3(I,R, T); + recv_3(I,R, T); 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); } @@ -34,7 +34,7 @@ protocol woolamPi-2(I,R,S) { 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)); } } diff --git a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl index 65b074f..1db544e 100644 --- a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl @@ -11,7 +11,7 @@ protocol woolamPi-3(I,R,S) var Nr: Nonce; send_1(I,R, I); - read_2(R,I, Nr); + recv_2(R,I, Nr); send_3(I,R, {Nr}k(I,S)); } @@ -21,11 +21,11 @@ protocol woolamPi-3(I,R,S) fresh Nr: Nonce; var T: Ticket; - read_1(I,R, I); + recv_1(I,R, I); send_2(R,I, Nr); - read_3(I,R, T); + recv_3(I,R, T); 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); } @@ -34,7 +34,7 @@ protocol woolamPi-3(I,R,S) { 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)); } } diff --git a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl index 80f3312..22f028c 100644 --- a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl @@ -11,7 +11,7 @@ protocol woolamPi-f(I,R,S) var Nr: Nonce; 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)); } @@ -21,11 +21,11 @@ protocol woolamPi-f(I,R,S) fresh Nr: Nonce; var T: Ticket; - read_1(I,R, I); + recv_1(I,R, I); 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)); - read_5(S,R, {I, R, Nr}k(R,S)); + recv_5(S,R, {I, R, Nr}k(R,S)); claim_R1(R,Nisynch); } @@ -34,7 +34,7 @@ protocol woolamPi-f(I,R,S) { 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)); } } diff --git a/gui/Protocols/MultiProtocolAttacks/woo-lam.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam.spdl index f29e27c..7e28057 100644 --- a/gui/Protocols/MultiProtocolAttacks/woo-lam.spdl +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam.spdl @@ -19,9 +19,9 @@ protocol woolam(I,R,S) var N2: Nonce; 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)); - 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); @@ -37,13 +37,13 @@ protocol woolam(I,R,S) var Kir: SessionKey; var T1,T2: Ticket; - read_1(I,R, I, N1); + recv_1(I,R, I, N1); 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)); - 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); - read_7(I,R, {N2}Kir); + recv_7(I,R, {N2}Kir); claim_R1(R,Secret,Kir); claim_R2(R,Nisynch); @@ -55,7 +55,7 @@ protocol woolam(I,R,S) fresh Kir: SessionKey; 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)); } } diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl index ee9805b..13d62a6 100644 --- a/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl @@ -19,7 +19,7 @@ protocol yahalom-BAN-Paulson-modified(A,B,S) var kab: SessionKey; 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 ); claim_5(A, Secret,kab); } @@ -31,9 +31,9 @@ protocol yahalom-BAN-Paulson-modified(A,B,S) var ticket: Ticket; 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) ); - 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); } @@ -42,7 +42,7 @@ protocol yahalom-BAN-Paulson-modified(A,B,S) fresh kab: SessionKey; 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl index 40cfee7..7d312ec 100644 --- a/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl @@ -17,7 +17,7 @@ protocol yahalom-BAN-Paulson(A,B,S) var kab: SessionKey; 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 ); claim_5(A, Secret,kab); } @@ -29,9 +29,9 @@ protocol yahalom-BAN-Paulson(A,B,S) var ticket: Ticket; 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) ); - 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); } @@ -40,7 +40,7 @@ protocol yahalom-BAN-Paulson(A,B,S) fresh kab: SessionKey; 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl index 9119065..3fa5f84 100644 --- a/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl @@ -18,7 +18,7 @@ protocol yahalom-BAN(I,R,S) var Kir: SessionKey; 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 ); claim_I1(I, Secret,Kir); @@ -33,9 +33,9 @@ protocol yahalom-BAN(I,R,S) var T: Ticket; 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) ); - 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_R2(R, Nisynch); @@ -47,7 +47,7 @@ protocol yahalom-BAN(I,R,S) fresh Kir: SessionKey; 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) ); } } diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl index 921e30a..651389d 100644 --- a/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl @@ -17,7 +17,7 @@ protocol yahalom-Lowe(I,R,S) var Kir: SessionKey; 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 ); claim_I1(I, Secret,Kir); @@ -30,10 +30,10 @@ protocol yahalom-Lowe(I,R,S) var Ni: Nonce; 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) ); - read_4(S,R, {I,Kir}k(R,S)); - read_5(I,R, {I, R, S, Nr}Kir); + recv_4(S,R, {I,Kir}k(R,S)); + recv_5(I,R, {I, R, S, Nr}Kir); claim_R1(R, Secret,Kir); claim_R2(R, Nisynch); @@ -44,7 +44,7 @@ protocol yahalom-Lowe(I,R,S) fresh Kir: SessionKey; 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_4(S,R, {I,Kir}k(R,S)); } diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom.spdl index e949cc6..063817f 100644 --- a/gui/Protocols/MultiProtocolAttacks/yahalom.spdl +++ b/gui/Protocols/MultiProtocolAttacks/yahalom.spdl @@ -17,7 +17,7 @@ protocol yahalom(I,R,S) var Kir: SessionKey; 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 ); claim_I1(I, Secret,Kir); @@ -30,9 +30,9 @@ protocol yahalom(I,R,S) var T: Ticket; 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) ); - 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); } @@ -42,7 +42,7 @@ protocol yahalom(I,R,S) fresh Kir: SessionKey; 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) ); claim(S, Secret, Ni); diff --git a/gui/Protocols/andrew-ban-concrete.spdl b/gui/Protocols/andrew-ban-concrete.spdl index b85a74f..48f52d8 100644 --- a/gui/Protocols/andrew-ban-concrete.spdl +++ b/gui/Protocols/andrew-ban-concrete.spdl @@ -10,7 +10,7 @@ # a given term crypted with k(I,R) with k(R,I) # # 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 # completely fresh and can therefore always be replaced by an arbitrary value # created by the intruder) which are not considered in SPORE @@ -18,7 +18,6 @@ usertype SessionKey; const Fresh: Function; -const Compromised: Function; protocol @swapkey(X) { @@ -27,7 +26,7 @@ protocol @swapkey(X) { var I,R: Agent; 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)); } } @@ -42,12 +41,12 @@ protocol andrew-Concrete(I,R) var kir: SessionKey; 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); claim_I1(I,Secret,kir); claim_I2(I,Nisynch); claim_I3(I,Empty,(Fresh,kir)); - read_6(R,I, nr); + recv_6(R,I, nr); } role R @@ -56,9 +55,9 @@ protocol andrew-Concrete(I,R) fresh nr: Nonce; fresh kir: SessionKey; - read_1(I,R, I,ni ); + recv_1(I,R, I,ni ); 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); claim_R1(R,Secret,kir); claim_R2(R,Nisynch); diff --git a/gui/Protocols/andrew-ban.spdl b/gui/Protocols/andrew-ban.spdl index 663ab4c..9ebd566 100644 --- a/gui/Protocols/andrew-ban.spdl +++ b/gui/Protocols/andrew-ban.spdl @@ -24,9 +24,9 @@ protocol andrew-Ban(I,R) var kir: SessionKey; 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) ); - 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_I2(I,Niagree); claim_I3(I,Secret, kir); @@ -40,9 +40,9 @@ protocol andrew-Ban(I,R) fresh nr,nr2: Nonce; 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) ); - 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) ); claim_R1(R,Nisynch); claim_R2(R,Niagree); diff --git a/gui/Protocols/andrew-lowe-ban.spdl b/gui/Protocols/andrew-lowe-ban.spdl index bb00132..04e15f2 100644 --- a/gui/Protocols/andrew-lowe-ban.spdl +++ b/gui/Protocols/andrew-lowe-ban.spdl @@ -9,7 +9,7 @@ # So it is possile that certain attacks that use this property are not found # # 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 # completely fresh and can therefore always be replaced by an arbitrary value # created by the intruder) which are not considered in SPORE @@ -31,12 +31,12 @@ protocol andrew-LoweBan(I,R) var kir: SessionKey; 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 ); claim_I1(I,Nisynch); claim_I2(I,Secret, kir); claim_I3(I,Empty, (Fresh,kir)); - read_4(R,I, nr ); + recv_4(R,I, nr ); } role R @@ -45,9 +45,9 @@ protocol andrew-LoweBan(I,R) fresh nr: Nonce; 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) ); - read_3(I,R, {ni}kir ); + recv_3(I,R, {ni}kir ); send_4(R,I, nr ); claim_R1(R,Nisynch); claim_R2(R,Secret, kir); diff --git a/gui/Protocols/andrew.spdl b/gui/Protocols/andrew.spdl index 2597353..b2e663c 100644 --- a/gui/Protocols/andrew.spdl +++ b/gui/Protocols/andrew.spdl @@ -12,7 +12,6 @@ usertype SessionKey; const succ: Function; const Fresh: Function; -const Compromised: Function; protocol andrew(I,R) { @@ -23,9 +22,9 @@ protocol andrew(I,R) var kir: SessionKey; 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) ); - read_4(R,I, {kir,nr2}k(I,R) ); + recv_4(R,I, {kir,nr2}k(I,R) ); claim_I1(I,Secret,kir); claim_I2(I,Nisynch); claim_I3(I,Niagree); @@ -38,9 +37,9 @@ protocol andrew(I,R) fresh nr,nr2: Nonce; 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) ); - 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) ); claim_R1(R,Secret,kir); claim_R2(R,Nisynch); diff --git a/gui/Protocols/ccitt509-1.spdl b/gui/Protocols/ccitt509-1.spdl index 1308afb..29c665a 100644 --- a/gui/Protocols/ccitt509-1.spdl +++ b/gui/Protocols/ccitt509-1.spdl @@ -19,7 +19,7 @@ protocol ccitt509-1(I,R) fresh Na,Xa,Ya: Nonce; send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); # 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 @@ -27,7 +27,7 @@ protocol ccitt509-1(I,R) var Ta: Timestamp; 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); # There should also be Fresh Xa and Fresh Ya claims here } diff --git a/gui/Protocols/ccitt509-1c.spdl b/gui/Protocols/ccitt509-1c.spdl index 7adccd3..6ae4088 100644 --- a/gui/Protocols/ccitt509-1c.spdl +++ b/gui/Protocols/ccitt509-1c.spdl @@ -18,7 +18,7 @@ protocol ccitt509-1c(I,R) const Na,Xa,Ya: Nonce; send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); # 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 @@ -26,7 +26,7 @@ protocol ccitt509-1c(I,R) var Ta: Timestamp; 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); # There should also be Fresh Xa and Fresh Ya claims here } diff --git a/gui/Protocols/ccitt509-3.spdl b/gui/Protocols/ccitt509-3.spdl index cf5f926..9ad1d3f 100644 --- a/gui/Protocols/ccitt509-3.spdl +++ b/gui/Protocols/ccitt509-3.spdl @@ -19,7 +19,7 @@ protocol ccitt509-3(I,R) fresh Na,Xa,Ya: Nonce; var Xb,Nb,Yb: Nonce; 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)); claim_I1(I,Nisynch); claim_I2(I,Secret,Ya); @@ -33,9 +33,9 @@ protocol ccitt509-3(I,R) var Na,Xa,Ya: 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)); - read_3(I,R, I, {Nb}sk(I)); + recv_3(I,R, I, {Nb}sk(I)); claim_R1(R,Nisynch); claim_R2(R,Secret,Ya); claim_R3(R,Secret,Yb); diff --git a/gui/Protocols/ccitt509-ban3.spdl b/gui/Protocols/ccitt509-ban3.spdl index ec442f2..0cbc198 100644 --- a/gui/Protocols/ccitt509-ban3.spdl +++ b/gui/Protocols/ccitt509-ban3.spdl @@ -19,7 +19,7 @@ protocol ccitt509-ban3(I,R) var Xb,Nb,Yb: Nonce; 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)); claim_4(I,Nisynch); } @@ -29,9 +29,9 @@ protocol ccitt509-ban3(I,R) var Na,Xa,Ya: 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)); - read_3(I,R, I,{R, Nb}sk(I)); + recv_3(I,R, I,{R, Nb}sk(I)); claim_5(R,Nisynch); # There should also be Fresh Xa and Fresh Ya claims here } diff --git a/gui/Protocols/denning-sacco-lowe.spdl b/gui/Protocols/denning-sacco-lowe.spdl index 28d9132..ddf245a 100644 --- a/gui/Protocols/denning-sacco-lowe.spdl +++ b/gui/Protocols/denning-sacco-lowe.spdl @@ -26,13 +26,13 @@ protocol denningSacco-Lowe(I,R,S) var Nr: Nonce; 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); - read_4(R,I, {Nr}Kir); + recv_4(R,I, {Nr}Kir); send_5(I,R, {{Nr}dec}Kir); claim_I1(I,Niagree); claim_I2(I,Nisynch); - claim_I3(I,Secret,Kir); + claim_I3(I,SKR,Kir); claim_I4(I,Empty,(Fresh,Kir)); } @@ -42,9 +42,9 @@ protocol denningSacco-Lowe(I,R,S) var T: TimeStamp; 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); - read_5(I,R, {{Nr}dec}Kir); + recv_5(I,R, {{Nr}dec}Kir); claim_R1(R,Niagree); claim_R2(R,Nisynch); claim_R3(R,Secret,Kir); @@ -57,7 +57,7 @@ protocol denningSacco-Lowe(I,R,S) fresh Kir: SessionKey; 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)); } } diff --git a/gui/Protocols/denning-sacco.spdl b/gui/Protocols/denning-sacco.spdl index 32f76cb..d77402f 100644 --- a/gui/Protocols/denning-sacco.spdl +++ b/gui/Protocols/denning-sacco.spdl @@ -20,7 +20,7 @@ protocol denningSacco(I,R,S) var T: TimeStamp; 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); claim_I1(I,Niagree); claim_I2(I,Nisynch); @@ -33,7 +33,7 @@ protocol denningSacco(I,R,S) var Kir: SessionKey; 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_R2(R,Nisynch); claim_R3(R,Secret,Kir); @@ -46,7 +46,7 @@ protocol denningSacco(I,R,S) fresh Kir: SessionKey; 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)); } } diff --git a/gui/Protocols/kaochow-v2.spdl b/gui/Protocols/kaochow-v2.spdl index be1c4c8..638a54b 100644 --- a/gui/Protocols/kaochow-v2.spdl +++ b/gui/Protocols/kaochow-v2.spdl @@ -17,7 +17,7 @@ protocol kaochow-2(I,R,S) var kir,kt: SessionKey; 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 ); claim_I1 (I, Nisynch); @@ -33,9 +33,9 @@ protocol kaochow-2(I,R,S) var kir,kt: SessionKey; 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 ); - read_4 (I,R, {nr,kir}kt ); + recv_4 (I,R, {nr,kir}kt ); claim_R1 (R, Nisynch); claim_R2 (R, Niagree); @@ -48,7 +48,7 @@ protocol kaochow-2(I,R,S) var ni: Nonce; 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) ); } } diff --git a/gui/Protocols/kaochow-v3.spdl b/gui/Protocols/kaochow-v3.spdl index 0bfc94a..88cef24 100644 --- a/gui/Protocols/kaochow-v3.spdl +++ b/gui/Protocols/kaochow-v3.spdl @@ -20,7 +20,7 @@ protocol kaochow-3(I,R,S) var T2: Ticket; 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 ); claim_I1 (I, Nisynch); @@ -37,9 +37,9 @@ protocol kaochow-3(I,R,S) var T: Ticket; 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) ); - 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_R2 (R, Niagree); @@ -52,7 +52,7 @@ protocol kaochow-3(I,R,S) var ni: Nonce; 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) ); } } diff --git a/gui/Protocols/kaochow.spdl b/gui/Protocols/kaochow.spdl index 4126ec3..1c6c827 100644 --- a/gui/Protocols/kaochow.spdl +++ b/gui/Protocols/kaochow.spdl @@ -17,7 +17,7 @@ protocol kaochow(I,R,S) var kir: SessionKey; 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 ); claim_I1 (I, Nisynch); @@ -33,9 +33,9 @@ protocol kaochow(I,R,S) var kir: SessionKey; 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 ); - read_4 (I,R, {nr}kir ); + recv_4 (I,R, {nr}kir ); claim_R1 (R, Nisynch); claim_R2 (R, Niagree); @@ -48,7 +48,7 @@ protocol kaochow(I,R,S) var ni: Nonce; 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) ); } } diff --git a/gui/Protocols/ksl-lowe.spdl b/gui/Protocols/ksl-lowe.spdl index 468e8fe..29996d8 100644 --- a/gui/Protocols/ksl-lowe.spdl +++ b/gui/Protocols/ksl-lowe.spdl @@ -23,11 +23,11 @@ protocol ksl-Lowe(I,R,S) var Kir: SessionKey; 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_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 ); claim_I1(I,Secret, Kir); @@ -45,15 +45,15 @@ protocol ksl-Lowe(I,R,S) fresh Tr: TimeStamp; var T: Ticket; - read_1(I,R, Ni, I); + recv_1(I,R, Ni, I); 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 ); - 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 ); - read_8(I,R, {I,Mr}Kir ); + recv_8(I,R, {I,Mr}Kir ); claim_R1(R,Secret, Kir); claim_R2(R,Niagree); @@ -66,7 +66,7 @@ protocol ksl-Lowe(I,R,S) var Ni, Nr: Nonce; 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) ); } } diff --git a/gui/Protocols/ksl.spdl b/gui/Protocols/ksl.spdl index 75cfeb9..7cfca44 100644 --- a/gui/Protocols/ksl.spdl +++ b/gui/Protocols/ksl.spdl @@ -22,11 +22,11 @@ protocol ksl(I,R,S) var Kir: SessionKey; 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_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 ); claim_I1(I,Secret, Kir); @@ -44,15 +44,15 @@ protocol ksl(I,R,S) fresh Tr: TimeStamp; var T: Ticket; - read_1(I,R, Ni, I); + recv_1(I,R, Ni, I); 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 ); - 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 ); - read_8(I,R, {Mr}Kir ); + recv_8(I,R, {Mr}Kir ); claim_R1(R,Secret, Kir); claim_R2(R,Niagree); @@ -65,7 +65,7 @@ protocol ksl(I,R,S) var Ni, Nr: Nonce; 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) ); } } diff --git a/gui/Protocols/needham-schroeder-lowe.spdl b/gui/Protocols/needham-schroeder-lowe.spdl index 8abb407..fabb522 100644 --- a/gui/Protocols/needham-schroeder-lowe.spdl +++ b/gui/Protocols/needham-schroeder-lowe.spdl @@ -18,9 +18,9 @@ protocol needhamschroederpk-Lowe(I,R,S) var Nr: Nonce; 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)); - 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)); claim_I1(I,Secret,Ni); claim_I2(I,Secret,Nr); @@ -32,11 +32,11 @@ protocol needhamschroederpk-Lowe(I,R,S) fresh Nr: 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)); - 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)); - read_7(I,R,{Nr}pk(R)); + recv_7(I,R,{Nr}pk(R)); claim_R1(R,Secret,Nr); claim_R2(R,Secret,Ni); claim_R3(R,Nisynch); @@ -44,9 +44,9 @@ protocol needhamschroederpk-Lowe(I,R,S) role S { - read_1(I,S,(I,R)); + recv_1(I,S,(I,R)); 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)); } } diff --git a/gui/Protocols/needham-schroeder-sk-amend.spdl b/gui/Protocols/needham-schroeder-sk-amend.spdl index 7c96390..189093d 100644 --- a/gui/Protocols/needham-schroeder-sk-amend.spdl +++ b/gui/Protocols/needham-schroeder-sk-amend.spdl @@ -27,11 +27,11 @@ protocol needhamschroedersk-amend(I,R,S) var T,T2: Ticket; send_1(I,R,I); - read_2(R,I,T); + recv_2(R,I,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); - read_6(R,I,{Nr}Kir); + recv_6(R,I,{Nr}Kir); send_7(I,R,{{Nr}dec}Kir); claim_I2(I,Secret,Kir); @@ -44,11 +44,11 @@ protocol needhamschroedersk-amend(I,R,S) fresh Nr: Nonce; var Kir: SessionKey; - read_1(I,R,I); + recv_1(I,R,I); 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); - read_7(I,R,{{Nr}dec}Kir); + recv_7(I,R,{{Nr}dec}Kir); claim_R1(R,Secret,Nr); claim_R3(R,Nisynch); claim_R4(R,Empty,(Fresh,Kir)); @@ -58,7 +58,7 @@ protocol needhamschroedersk-amend(I,R,S) { var Ni,Nr: Nonce; 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)); } diff --git a/gui/Protocols/needham-schroeder-sk.spdl b/gui/Protocols/needham-schroeder-sk.spdl index 50c87d4..71a7e6c 100644 --- a/gui/Protocols/needham-schroeder-sk.spdl +++ b/gui/Protocols/needham-schroeder-sk.spdl @@ -23,9 +23,9 @@ protocol needhamschroedersk(I,R,S) var T: Ticket; 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); - read_4(R,I,{Nr}Kir); + recv_4(R,I,{Nr}Kir); send_5(I,R,{{Nr}dec}Kir); claim_I2(I,Secret,Kir); claim_I3(I,Nisynch); @@ -37,9 +37,9 @@ protocol needhamschroedersk(I,R,S) fresh Nr: Nonce; 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); - read_5(I,R,{{Nr}dec}Kir); + recv_5(I,R,{{Nr}dec}Kir); claim_R1(R,Secret,Kir); claim_R3(R,Nisynch); claim_R4(R,Empty,(Fresh,Kir)); @@ -49,7 +49,7 @@ protocol needhamschroedersk(I,R,S) { var Ni: Nonce; 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)); } } diff --git a/gui/Protocols/needham-schroeder.spdl b/gui/Protocols/needham-schroeder.spdl index 76db7c2..ea14854 100644 --- a/gui/Protocols/needham-schroeder.spdl +++ b/gui/Protocols/needham-schroeder.spdl @@ -18,9 +18,9 @@ protocol needhamschroederpk(I,R,S) var Nr: Nonce; 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)); - read_6(R,I, {Ni, Nr}pk(I)); + recv_6(R,I, {Ni, Nr}pk(I)); send_7(I,R, {Nr}pk(R)); claim_I1(I,Secret,Ni); claim_I2(I,Secret,Nr); @@ -32,11 +32,11 @@ protocol needhamschroederpk(I,R,S) fresh Nr: 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)); - 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)); - read_7(I,R,{Nr}pk(R)); + recv_7(I,R,{Nr}pk(R)); claim_R1(R,Secret,Nr); claim_R2(R,Secret,Ni); claim_R3(R,Nisynch); @@ -44,9 +44,9 @@ protocol needhamschroederpk(I,R,S) role S { - read_1(I,S,(I,R)); + recv_1(I,S,(I,R)); 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)); } } diff --git a/gui/Protocols/neumannstub-guttman-hwang.spdl b/gui/Protocols/neumannstub-guttman-hwang.spdl index f7266be..bcb48d2 100644 --- a/gui/Protocols/neumannstub-guttman-hwang.spdl +++ b/gui/Protocols/neumannstub-guttman-hwang.spdl @@ -26,7 +26,7 @@ protocol neustub-GuttmanHwang^Repeat(I,R,S) fresh Tr: TimeStamp; 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); claim_I1(I,Secret, Kir); claim_I2(I,Niagree); @@ -41,9 +41,9 @@ protocol neustub-GuttmanHwang^Repeat(I,R,S) var Kir: SessionKey; 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); - read_7(I,R,{I,Mr}Kir); + recv_7(I,R,{I,Mr}Kir); claim_R1(R,Secret, Kir); claim_R2(R,Niagree); claim_R3(R,Nisynch); @@ -65,7 +65,7 @@ protocol neustub-GuttmanHwang(I,R,S) var Kir: SessionKey; 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); claim_I1(I,Secret, Kir); @@ -82,9 +82,9 @@ protocol neustub-GuttmanHwang(I,R,S) fresh Tb: TimeStamp; 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)); - 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_R2(R,Niagree); @@ -98,7 +98,7 @@ protocol neustub-GuttmanHwang(I,R,S) fresh Kir: SessionKey; 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 ); } } diff --git a/gui/Protocols/neumannstub-guttman.spdl b/gui/Protocols/neumannstub-guttman.spdl index 06853b0..09e7f6e 100644 --- a/gui/Protocols/neumannstub-guttman.spdl +++ b/gui/Protocols/neumannstub-guttman.spdl @@ -26,7 +26,7 @@ protocol neustub^Repeat(I,R,S) fresh Tr: TimeStamp; 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); claim_I1(I,Secret, Kir); claim_I2(I,Niagree); @@ -41,9 +41,9 @@ protocol neustub^Repeat(I,R,S) var Kir: SessionKey; 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); - read_7(I,R,{I,Mr}Kir); + recv_7(I,R,{I,Mr}Kir); claim_R1(R,Secret, Kir); claim_R2(R,Niagree); claim_R3(R,Nisynch); @@ -65,7 +65,7 @@ protocol neustub(I,R,S) var Kir: SessionKey; 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); claim_I1(I,Secret, Kir); @@ -82,9 +82,9 @@ protocol neustub(I,R,S) fresh Tb: TimeStamp; 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); - 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_R2(R,Niagree); @@ -98,7 +98,7 @@ protocol neustub(I,R,S) fresh Kir: SessionKey; 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 ); } } diff --git a/gui/Protocols/neumannstub-hwang.spdl b/gui/Protocols/neumannstub-hwang.spdl index 67e598e..1546b40 100644 --- a/gui/Protocols/neumannstub-hwang.spdl +++ b/gui/Protocols/neumannstub-hwang.spdl @@ -25,10 +25,10 @@ protocol neustub-Hwang(I,R,S) var Kir: SessionKey; 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_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); claim_I1(I,Secret, Kir); @@ -45,12 +45,12 @@ protocol neustub-Hwang(I,R,S) fresh Tb: TimeStamp; 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)); - read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); - read_5(I,R,Mi,T); + recv_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); + recv_5(I,R,Mi,T); 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_R2(R,Niagree); @@ -64,7 +64,7 @@ protocol neustub-Hwang(I,R,S) fresh Kir: SessionKey; 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 ); } } diff --git a/gui/Protocols/neumannstub-keycompromise.spdl b/gui/Protocols/neumannstub-keycompromise.spdl index 25b15e9..d803150 100644 --- a/gui/Protocols/neumannstub-keycompromise.spdl +++ b/gui/Protocols/neumannstub-keycompromise.spdl @@ -26,7 +26,7 @@ protocol neustub^Repeat(I,R,S) fresh Tr: TimeStamp; 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); claim_I1(I,Secret, Kir); claim_I2(I,Niagree); @@ -41,9 +41,9 @@ protocol neustub^Repeat(I,R,S) var Kir: SessionKey; 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); - read_7(I,R,{Mr}Kir); + recv_7(I,R,{Mr}Kir); claim_R1(R,Secret, Kir); claim_R2(R,Niagree); claim_R3(R,Nisynch); @@ -65,7 +65,7 @@ protocol neustub(I,R,S) var Kir: SessionKey; 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); claim_I1(I,Secret, Kir); @@ -82,9 +82,9 @@ protocol neustub(I,R,S) fresh Tb: TimeStamp; 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); - 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_R2(R,Niagree); @@ -98,7 +98,7 @@ protocol neustub(I,R,S) fresh Kir: SessionKey; 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 ); } } diff --git a/gui/Protocols/neumannstub.spdl b/gui/Protocols/neumannstub.spdl index 3327abf..d1d0ee1 100644 --- a/gui/Protocols/neumannstub.spdl +++ b/gui/Protocols/neumannstub.spdl @@ -23,7 +23,7 @@ protocol neustub^Repeat(I,R,S) fresh Tr: TimeStamp; 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); claim_I1(I,Secret, Kir); claim_I2(I,Niagree); @@ -37,9 +37,9 @@ protocol neustub^Repeat(I,R,S) var Kir: SessionKey; 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); - read_7(I,R,{Mr}Kir); + recv_7(I,R,{Mr}Kir); claim_R1(R,Secret, Kir); claim_R2(R,Niagree); claim_R3(R,Nisynch); @@ -60,7 +60,7 @@ protocol neustub(I,R,S) var Kir: SessionKey; 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); claim_I1(I,Secret, Kir); @@ -76,9 +76,9 @@ protocol neustub(I,R,S) fresh Tb: TimeStamp; 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); - 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_R2(R,Niagree); @@ -91,7 +91,7 @@ protocol neustub(I,R,S) fresh Kir: SessionKey; 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 ); } } diff --git a/gui/Protocols/otwayrees.spdl b/gui/Protocols/otwayrees.spdl index 64b99dc..bed12ad 100644 --- a/gui/Protocols/otwayrees.spdl +++ b/gui/Protocols/otwayrees.spdl @@ -19,7 +19,7 @@ protocol otwayrees(I,R,S) var Kir : SessionKey; 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_I2(I, Nisynch); @@ -33,9 +33,9 @@ protocol otwayrees(I,R,S) var Kir : SessionKey; 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) ); - 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 ); claim_R1(R, Secret,Kir); @@ -49,7 +49,7 @@ protocol otwayrees(I,R,S) var M : String; 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) ); } } diff --git a/gui/Protocols/smartright.spdl b/gui/Protocols/smartright.spdl index da9be17..e3a9719 100644 --- a/gui/Protocols/smartright.spdl +++ b/gui/Protocols/smartright.spdl @@ -25,7 +25,7 @@ protocol smartright(I,R) var VoRi: Nonce; 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); } @@ -36,9 +36,9 @@ protocol smartright(I,R) var VoKey: SessionKey; 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); - read_3(I,R, VoR,{{VoRi}hash}VoKey); + recv_3(I,R, VoR,{{VoRi}hash}VoKey); claim_R1(R,Nisynch); } diff --git a/gui/Protocols/splice-as-cj.spdl b/gui/Protocols/splice-as-cj.spdl index 87960b3..b393294 100644 --- a/gui/Protocols/splice-as-cj.spdl +++ b/gui/Protocols/splice-as-cj.spdl @@ -24,9 +24,9 @@ protocol spliceAS-CJ(I,R,S) fresh L: LifeTime; 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) ); - 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_9(I, Niagree); @@ -37,9 +37,9 @@ protocol spliceAS-CJ(I,R,S) { 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) ); - 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) ); } @@ -53,9 +53,9 @@ protocol spliceAS-CJ(I,R,S) var ni: 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 ); - 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) ); claim_8(R, Secret, N2); diff --git a/gui/Protocols/splice-as-hc.spdl b/gui/Protocols/splice-as-hc.spdl index 858e02a..2f975ad 100644 --- a/gui/Protocols/splice-as-hc.spdl +++ b/gui/Protocols/splice-as-hc.spdl @@ -19,9 +19,9 @@ protocol spliceAS-HC(I,R,S) fresh L: LifeTime; 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) ); - 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_9(I, Niagree); @@ -32,9 +32,9 @@ protocol spliceAS-HC(I,R,S) { 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) ); - 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) ); } @@ -48,9 +48,9 @@ protocol spliceAS-HC(I,R,S) var ni: 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 ); - 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) ); claim_8(R, Secret, N2); diff --git a/gui/Protocols/splice-as.spdl b/gui/Protocols/splice-as.spdl index 9890adb..b1d8e18 100644 --- a/gui/Protocols/splice-as.spdl +++ b/gui/Protocols/splice-as.spdl @@ -24,9 +24,9 @@ protocol spliceAS(I,R,S) fresh L: LifeTime; 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) ); - 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_9(I, Niagree); @@ -37,9 +37,9 @@ protocol spliceAS(I,R,S) { 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) ); - 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) ); } @@ -53,9 +53,9 @@ protocol spliceAS(I,R,S) var ni: 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 ); - 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) ); claim_8(R, Secret, N2); diff --git a/gui/Protocols/tmn.spdl b/gui/Protocols/tmn.spdl index 267d30f..c6fb55f 100644 --- a/gui/Protocols/tmn.spdl +++ b/gui/Protocols/tmn.spdl @@ -19,7 +19,7 @@ protocol tmn(I,R,S) var Kr: SessionKey; 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_I2(I,Nisynch); @@ -30,7 +30,7 @@ protocol tmn(I,R,S) { fresh Kr: SessionKey; - read_2(S,R, I ); + recv_2(S,R, I ); send_3(R,S, I, { Kr }pk(S) ); claim_R1(R,Secret,Kr); @@ -42,9 +42,9 @@ protocol tmn(I,R,S) { 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 ); - read_3(R,S, I, { Kr }pk(S) ); + recv_3(R,S, I, { Kr }pk(S) ); send_4(S,I, R,{Kr}Ki ); } } diff --git a/gui/Protocols/wmf-lowe.spdl b/gui/Protocols/wmf-lowe.spdl index 61c5b7f..86b34e3 100644 --- a/gui/Protocols/wmf-lowe.spdl +++ b/gui/Protocols/wmf-lowe.spdl @@ -6,7 +6,7 @@ # Note: # 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 -# 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. usertype SessionKey; @@ -27,7 +27,7 @@ protocol wmf-Lowe(I,R,S) var Nr: Nonce; 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); claim_I1(I,Secret,Kir); @@ -41,9 +41,9 @@ protocol wmf-Lowe(I,R,S) var Kir: SessionKey; 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); - read_4(I,R, {{Nr}succ}Kir); + recv_4(I,R, {{Nr}succ}Kir); claim_R1(R,Secret,Kir); claim_R2(R,Nisynch); @@ -56,7 +56,7 @@ protocol wmf-Lowe(I,R,S) fresh Ts: 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)); } } diff --git a/gui/Protocols/wmf.spdl b/gui/Protocols/wmf.spdl index 4c787a8..758843a 100644 --- a/gui/Protocols/wmf.spdl +++ b/gui/Protocols/wmf.spdl @@ -34,7 +34,7 @@ protocol wmf(I,R,S) var Ts: TimeStamp; 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_R2(R,Nisynch); @@ -47,7 +47,7 @@ protocol wmf(I,R,S) fresh Ts: 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)); } } diff --git a/gui/Protocols/woo-lam-pi-1.spdl b/gui/Protocols/woo-lam-pi-1.spdl index d38c837..7e4e09d 100644 --- a/gui/Protocols/woo-lam-pi-1.spdl +++ b/gui/Protocols/woo-lam-pi-1.spdl @@ -11,7 +11,7 @@ protocol woolamPi-1(I,R,S) var Nr: Nonce; 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)); } @@ -21,11 +21,11 @@ protocol woolamPi-1(I,R,S) fresh Nr: Nonce; var T: Ticket; - read_1(I,R, I); + recv_1(I,R, I); 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)); - read_5(S,R, {I,R, Nr}k(R,S)); + recv_5(S,R, {I,R, Nr}k(R,S)); claim_R1(R,Nisynch); } @@ -34,7 +34,7 @@ protocol woolamPi-1(I,R,S) { 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)); } } diff --git a/gui/Protocols/woo-lam-pi-2.spdl b/gui/Protocols/woo-lam-pi-2.spdl index 10b61d4..5d767d6 100644 --- a/gui/Protocols/woo-lam-pi-2.spdl +++ b/gui/Protocols/woo-lam-pi-2.spdl @@ -11,7 +11,7 @@ protocol woolamPi-2(I,R,S) var Nr: Nonce; send_1(I,R, I); - read_2(R,I, Nr); + recv_2(R,I, Nr); send_3(I,R, {I,Nr}k(I,S)); } @@ -21,11 +21,11 @@ protocol woolamPi-2(I,R,S) fresh Nr: Nonce; var T: Ticket; - read_1(I,R, I); + recv_1(I,R, I); send_2(R,I, Nr); - read_3(I,R, T); + recv_3(I,R, T); 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); } @@ -34,7 +34,7 @@ protocol woolamPi-2(I,R,S) { 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)); } } diff --git a/gui/Protocols/woo-lam-pi-3.spdl b/gui/Protocols/woo-lam-pi-3.spdl index 65b074f..1db544e 100644 --- a/gui/Protocols/woo-lam-pi-3.spdl +++ b/gui/Protocols/woo-lam-pi-3.spdl @@ -11,7 +11,7 @@ protocol woolamPi-3(I,R,S) var Nr: Nonce; send_1(I,R, I); - read_2(R,I, Nr); + recv_2(R,I, Nr); send_3(I,R, {Nr}k(I,S)); } @@ -21,11 +21,11 @@ protocol woolamPi-3(I,R,S) fresh Nr: Nonce; var T: Ticket; - read_1(I,R, I); + recv_1(I,R, I); send_2(R,I, Nr); - read_3(I,R, T); + recv_3(I,R, T); 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); } @@ -34,7 +34,7 @@ protocol woolamPi-3(I,R,S) { 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)); } } diff --git a/gui/Protocols/woo-lam-pi-f.spdl b/gui/Protocols/woo-lam-pi-f.spdl index 80f3312..22f028c 100644 --- a/gui/Protocols/woo-lam-pi-f.spdl +++ b/gui/Protocols/woo-lam-pi-f.spdl @@ -11,7 +11,7 @@ protocol woolamPi-f(I,R,S) var Nr: Nonce; 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)); } @@ -21,11 +21,11 @@ protocol woolamPi-f(I,R,S) fresh Nr: Nonce; var T: Ticket; - read_1(I,R, I); + recv_1(I,R, I); 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)); - read_5(S,R, {I, R, Nr}k(R,S)); + recv_5(S,R, {I, R, Nr}k(R,S)); claim_R1(R,Nisynch); } @@ -34,7 +34,7 @@ protocol woolamPi-f(I,R,S) { 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)); } } diff --git a/gui/Protocols/woo-lam-pi.spdl b/gui/Protocols/woo-lam-pi.spdl index cb0878e..0c01c27 100644 --- a/gui/Protocols/woo-lam-pi.spdl +++ b/gui/Protocols/woo-lam-pi.spdl @@ -15,7 +15,7 @@ protocol woolamPi(I,R,S) var Nr: Nonce; send_1(I,R, I); - read_2(R,I, Nr); + recv_2(R,I, Nr); send_3(I,R, {Nr}k(I,S)); } @@ -25,11 +25,11 @@ protocol woolamPi(I,R,S) fresh Nr: Nonce; var T: Ticket; - read_1(I,R, I); + recv_1(I,R, I); send_2(R,I, Nr); - read_3(I,R, T); + recv_3(I,R, T); 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); } @@ -38,7 +38,7 @@ protocol woolamPi(I,R,S) { 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)); } } diff --git a/gui/Protocols/woo-lam.spdl b/gui/Protocols/woo-lam.spdl index ac7f36d..7e28057 100644 --- a/gui/Protocols/woo-lam.spdl +++ b/gui/Protocols/woo-lam.spdl @@ -19,9 +19,9 @@ protocol woolam(I,R,S) var N2: Nonce; 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)); - 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); @@ -37,13 +37,13 @@ protocol woolam(I,R,S) var Kir: SessionKey; var T1,T2: Ticket; - read_1(I,R, I, N1); + recv_1(I,R, I, N1); 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)); - 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); - read_7(I,R, {N2}Kir); + recv_7(I,R, {N2}Kir); claim_R1(R,Secret,Kir); claim_R2(R,Nisynch); @@ -55,8 +55,10 @@ protocol woolam(I,R,S) fresh Kir: SessionKey; 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)); } } + + diff --git a/gui/Protocols/yahalom-ban.spdl b/gui/Protocols/yahalom-ban.spdl index 4d40ac7..b865362 100644 --- a/gui/Protocols/yahalom-ban.spdl +++ b/gui/Protocols/yahalom-ban.spdl @@ -18,7 +18,7 @@ protocol yahalom-BAN(I,R,S) var Kir: SessionKey; 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 ); claim_I1(I, Secret,Kir); @@ -33,9 +33,9 @@ protocol yahalom-BAN(I,R,S) var T: Ticket; 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) ); - 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_R2(R, Nisynch); @@ -47,7 +47,7 @@ protocol yahalom-BAN(I,R,S) fresh Kir: SessionKey; 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) ); } } diff --git a/gui/Protocols/yahalom-lowe.spdl b/gui/Protocols/yahalom-lowe.spdl index f04aca9..308a62a 100644 --- a/gui/Protocols/yahalom-lowe.spdl +++ b/gui/Protocols/yahalom-lowe.spdl @@ -17,7 +17,7 @@ protocol yahalom-Lowe(I,R,S) var Kir: SessionKey; 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 ); claim_I1(I, Secret,Kir); @@ -30,10 +30,10 @@ protocol yahalom-Lowe(I,R,S) var Ni: Nonce; 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) ); - read_4(S,R, {I,Kir}k(R,S)); - read_5(I,R, {I, R, S, Nr}Kir); + recv_4(S,R, {I,Kir}k(R,S)); + recv_5(I,R, {I, R, S, Nr}Kir); claim_R1(R, Secret,Kir); claim_R2(R, Nisynch); @@ -44,7 +44,7 @@ protocol yahalom-Lowe(I,R,S) fresh Kir: SessionKey; 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_4(S,R, {I,Kir}k(R,S)); } diff --git a/gui/Protocols/yahalom-paulson.spdl b/gui/Protocols/yahalom-paulson.spdl index 0c4ce68..a8dfe1e 100644 --- a/gui/Protocols/yahalom-paulson.spdl +++ b/gui/Protocols/yahalom-paulson.spdl @@ -20,7 +20,7 @@ protocol yahalom-Paulson(I,R,S) var Kir: SessionKey; 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 ); claim_I1(I, Secret,Kir); @@ -35,9 +35,9 @@ protocol yahalom-Paulson(I,R,S) var T: Ticket; 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) ); - 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_R2(R, Nisynch); @@ -49,7 +49,7 @@ protocol yahalom-Paulson(I,R,S) fresh Kir: SessionKey; 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) ); } } diff --git a/gui/Protocols/yahalom.spdl b/gui/Protocols/yahalom.spdl index e949cc6..063817f 100644 --- a/gui/Protocols/yahalom.spdl +++ b/gui/Protocols/yahalom.spdl @@ -17,7 +17,7 @@ protocol yahalom(I,R,S) var Kir: SessionKey; 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 ); claim_I1(I, Secret,Kir); @@ -30,9 +30,9 @@ protocol yahalom(I,R,S) var T: Ticket; 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) ); - 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); } @@ -42,7 +42,7 @@ protocol yahalom(I,R,S) fresh Kir: SessionKey; 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) ); claim(S, Secret, Ni);