diff --git a/protocols/Demo/ns3.spdl b/protocols/Demo/ns3.spdl index 7954e31..c9235c5 100644 --- a/protocols/Demo/ns3.spdl +++ b/protocols/Demo/ns3.spdl @@ -12,7 +12,7 @@ protocol ns3(I,R) var nr: Nonce; send_1(I,R, {I,ni}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); @@ -26,9 +26,9 @@ protocol ns3(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}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/protocols/Demo/nsl3-broken.spdl b/protocols/Demo/nsl3-broken.spdl index b06cb69..c635f91 100644 --- a/protocols/Demo/nsl3-broken.spdl +++ b/protocols/Demo/nsl3-broken.spdl @@ -13,7 +13,7 @@ protocol nsl3-broken(I,R) var nr: Nonce; send_1(I,R, {R,ni}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); @@ -27,9 +27,9 @@ protocol nsl3-broken(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {R,ni}pk(R) ); + recv_1(I,R, {R,ni}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/protocols/Demo/nsl3-updated-both.spdl b/protocols/Demo/nsl3-updated-both.spdl index 4e706c2..076166e 100644 --- a/protocols/Demo/nsl3-updated-both.spdl +++ b/protocols/Demo/nsl3-updated-both.spdl @@ -13,7 +13,7 @@ protocol nsl3-broken(I,R) var nr: Nonce; send_1(I,R, {R,ni}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); @@ -27,9 +27,9 @@ protocol nsl3-broken(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {R,ni}pk(R) ); + recv_1(I,R, {R,ni}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); @@ -52,7 +52,7 @@ protocol nsl3(I,R) var nr: Nonce; send_1(I,R, {I,ni}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); @@ -66,9 +66,9 @@ protocol nsl3(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}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/protocols/Demo/nsl3.spdl b/protocols/Demo/nsl3.spdl index 6d367cb..ebf9031 100644 --- a/protocols/Demo/nsl3.spdl +++ b/protocols/Demo/nsl3.spdl @@ -12,7 +12,7 @@ protocol nsl3(I,R) var nr: Nonce; send_1(I,R, {I,ni}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, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}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/protocols/misc/2r890-ex3-a.spdl b/protocols/misc/2r890-ex3-a.spdl index 32c55ab..d81b167 100644 --- a/protocols/misc/2r890-ex3-a.spdl +++ b/protocols/misc/2r890-ex3-a.spdl @@ -19,9 +19,9 @@ protocol course2r890year0405ex3(X,Y,I) fresh ny: Nonce; send_1(I,X, nx ); - read_2(X,I, { I,nx }sk(X) ); + recv_2(X,I, { I,nx }sk(X) ); send_3(I,Y, ny ); - read_4(Y,I, { ny,I }sk(Y) ); + recv_4(Y,I, { ny,I }sk(Y) ); claim_i1(I,Niagree); claim_i2(I,Nisynch); @@ -31,7 +31,7 @@ protocol course2r890year0405ex3(X,Y,I) { var nx: Nonce; - read_1(I,X, nx ); + recv_1(I,X, nx ); send_2(X,I, { I,nx }sk(X) ); } @@ -39,7 +39,7 @@ protocol course2r890year0405ex3(X,Y,I) { var ny: Nonce; - read_3(I,Y, ny ); + recv_3(I,Y, ny ); send_4(Y,I, { ny,I }sk(Y) ); } } diff --git a/protocols/misc/2r890-ex3-b.spdl b/protocols/misc/2r890-ex3-b.spdl index 4b9c8cd..9950b48 100644 --- a/protocols/misc/2r890-ex3-b.spdl +++ b/protocols/misc/2r890-ex3-b.spdl @@ -18,9 +18,9 @@ protocol course2r890year0405ex3(X,Y,I) fresh ni: Nonce; send_1(I,X, ni ); - read_2(X,I, { I,ni }sk(X) ); + recv_2(X,I, { I,ni }sk(X) ); send_3(I,Y, ni ); - read_4(Y,I, { ni,I }sk(Y) ); + recv_4(Y,I, { ni,I }sk(Y) ); claim_i1(I,Niagree); claim_i2(I,Nisynch); @@ -30,7 +30,7 @@ protocol course2r890year0405ex3(X,Y,I) { var nx: Nonce; - read_1(I,X, nx ); + recv_1(I,X, nx ); send_2(X,I, { I,nx }sk(X) ); } @@ -38,7 +38,7 @@ protocol course2r890year0405ex3(X,Y,I) { var ny: Nonce; - read_3(I,Y, ny ); + recv_3(I,Y, ny ); send_4(Y,I, { ny,I }sk(Y) ); } } diff --git a/protocols/misc/andrew-ban.spdl b/protocols/misc/andrew-ban.spdl index 580e108..d9a24ac 100644 --- a/protocols/misc/andrew-ban.spdl +++ b/protocols/misc/andrew-ban.spdl @@ -10,9 +10,9 @@ protocol andrewBan(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_5(I,Nisynch); claim_5b(I,Niagree); claim_6(I,Secret, kir); @@ -25,9 +25,9 @@ protocol andrewBan(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_8(R,Nisynch); claim_8b(R,Niagree); diff --git a/protocols/misc/andrew-lowe-ban.spdl b/protocols/misc/andrew-lowe-ban.spdl index 778fac1..8deb5f0 100644 --- a/protocols/misc/andrew-lowe-ban.spdl +++ b/protocols/misc/andrew-lowe-ban.spdl @@ -10,9 +10,9 @@ protocol andrewLoweBan(I,R) var kir: SessionKey; send_1(I,R, I,ni ); - read_2(R,I, {ni,kir,I}k(I,R) ); + recv_2(R,I, {ni,kir,I}k(I,R) ); send_3(I,R, {ni}kir ); - read_4(R,I, nr ); + recv_4(R,I, nr ); claim_5(I,Nisynch); claim_5b(I,Niagree); claim_6(I,Secret, kir); @@ -25,9 +25,9 @@ protocol andrewLoweBan(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,I}k(I,R) ); - read_3(I,R, {ni}kir ); + recv_3(I,R, {ni}kir ); send_4(R,I, nr ); claim_8(R,Nisynch); claim_8b(R,Niagree); diff --git a/protocols/misc/athena-breaker.spdl b/protocols/misc/athena-breaker.spdl index 75d15a0..717d926 100644 --- a/protocols/misc/athena-breaker.spdl +++ b/protocols/misc/athena-breaker.spdl @@ -25,7 +25,7 @@ protocol abreaker(I,R) { var T:Ticket; - read_!1(I,R, {T}pk(R) ); + recv_!1(I,R, {T}pk(R) ); send_!2(R,I, T ); } diff --git a/protocols/misc/bke-broken.spdl b/protocols/misc/bke-broken.spdl index e05e1bd..93700af 100644 --- a/protocols/misc/bke-broken.spdl +++ b/protocols/misc/bke-broken.spdl @@ -20,7 +20,7 @@ protocol bkebroken(I,R) var kir: Key; send_1 (I,R, { ni,I }pk(R) ); - read_2 (R,I, { h(ni),nr,kir }pk(I) ); + recv_2 (R,I, { h(ni),nr,kir }pk(I) ); send_3 (I,R, { h(nr),kir }pk(R) ); claim_4 (I, Secret, kir ); } @@ -31,9 +31,9 @@ protocol bkebroken(I,R) fresh nr: Nonce; fresh kir: Key; - read_1 (I,R, { ni,I }pk(R) ); + recv_1 (I,R, { ni,I }pk(R) ); send_2 (R,I, { h(ni),nr,kir }pk(I) ); - read_3 (I,R, { h(nr),kir }pk(R) ); + recv_3 (I,R, { h(nr),kir }pk(R) ); claim_5 (R, Secret, kir ); } } diff --git a/protocols/misc/bke-one.spdl b/protocols/misc/bke-one.spdl index f21b775..b6118cd 100644 --- a/protocols/misc/bke-one.spdl +++ b/protocols/misc/bke-one.spdl @@ -19,7 +19,7 @@ protocol bkeONE(I,R) var kir: Key; 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 ); } @@ -30,9 +30,9 @@ protocol bkeONE(I,R) fresh nr: Nonce; fresh kir: Key; - 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_5 (R, Secret, kir ); } } diff --git a/protocols/misc/bke-variation.spdl b/protocols/misc/bke-variation.spdl index f7e8b30..92cbe08 100644 --- a/protocols/misc/bke-variation.spdl +++ b/protocols/misc/bke-variation.spdl @@ -20,7 +20,7 @@ protocol bkevariation(I,R) var kir: Key; send_1 (I,R, { ni,I }pk(R) ); - read_2 (R,I, { hash(ni),nr,kir }pk(I) ); + recv_2 (R,I, { hash(ni),nr,kir }pk(I) ); send_3 (I,R, { hash(nr) }kir ); claim_4 (I, Secret, kir ); claim_5 (I, Niagree ); @@ -33,9 +33,9 @@ protocol bkevariation(I,R) fresh nr: Nonce; fresh kir: Key; - read_1 (I,R, { ni,I }pk(R) ); + recv_1 (I,R, { ni,I }pk(R) ); send_2 (R,I, { hash(ni),nr,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/protocols/misc/bke.spdl b/protocols/misc/bke.spdl index 3962db2..8c7e77a 100644 --- a/protocols/misc/bke.spdl +++ b/protocols/misc/bke.spdl @@ -15,7 +15,7 @@ protocol bke(I,R) var kir: Key; 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: Key; - 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/protocols/misc/bkepk-ce.spdl b/protocols/misc/bkepk-ce.spdl index 91bb7f9..71fbbe8 100644 --- a/protocols/misc/bkepk-ce.spdl +++ b/protocols/misc/bkepk-ce.spdl @@ -21,9 +21,9 @@ protocol bkeCE(A,B) fresh na: Nonce; fresh kab: Key; - read_1 (B,A, B,{ nb,B }pk(A) ); + recv_1 (B,A, B,{ nb,B }pk(A) ); send_2 (A,B, { hash(nb),na,A,kab }pk(B) ); - read_3 (B,A, { hash(na) }kab ); + recv_3 (B,A, { hash(na) }kab ); claim_A1 (A, Secret, na); claim_A2 (A, Secret, nb); @@ -36,7 +36,7 @@ protocol bkeCE(A,B) var kab: Key; send_1 (B,A, B,{ nb,B }pk(A) ); - read_2 (A,B, { hash(nb),na,A,kab }pk(B) ); + recv_2 (A,B, { hash(nb),na,A,kab }pk(B) ); send_3 (B,A, { hash(na) }kab ); claim_B1 (B, Secret, na); diff --git a/protocols/misc/bkepk-ce2.spdl b/protocols/misc/bkepk-ce2.spdl index f596453..14fe73d 100644 --- a/protocols/misc/bkepk-ce2.spdl +++ b/protocols/misc/bkepk-ce2.spdl @@ -21,7 +21,7 @@ protocol bkepkCE2(A,B,testnonce) var kab: Key; send_1 (B,A, B,{ nb,B }pk(A) ); - read_2 (A,B, { hash(nb),na,A,kab }pk(B) ); + recv_2 (A,B, { hash(nb),na,A,kab }pk(B) ); send_3 (B,A, { hash(na) }kab ); } @@ -31,16 +31,16 @@ protocol bkepkCE2(A,B,testnonce) fresh na: Nonce; fresh kab: Key; - read_1 (B,A, B,{ nb,B }pk(A) ); + recv_1 (B,A, B,{ nb,B }pk(A) ); send_2 (A,B, { hash(nb),na,A,kab }pk(B) ); - read_3 (B,A, { hash(na) }kab ); + recv_3 (B,A, { hash(na) }kab ); } role testnonce { var n: Nonce; - read_!4 (testnonce,testnonce, n); + recv_!4 (testnonce,testnonce, n); } } diff --git a/protocols/misc/boyd-nsl-fix.spdl b/protocols/misc/boyd-nsl-fix.spdl index 02adf67..6aed3c1 100644 --- a/protocols/misc/boyd-nsl-fix.spdl +++ b/protocols/misc/boyd-nsl-fix.spdl @@ -22,7 +22,7 @@ protocol boydNS(I,R) var nr: Nonce; send_1(I,R, {ni}pk(R),I ); - read_2(R,I, {nr}pk(I),hash(ni,R) ); + recv_2(R,I, {nr}pk(I),hash(ni,R) ); send_3(I,R, hash(nr, I,R) ); claim_i1(I,Secret,ni); claim_i2(I,Secret,nr); @@ -35,9 +35,9 @@ protocol boydNS(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {ni}pk(R),I ); + recv_1(I,R, {ni}pk(R),I ); send_2(R,I, {nr}pk(I),hash(ni,R) ); - read_3(I,R, hash(nr, I,R) ); + recv_3(I,R, hash(nr, I,R) ); claim_r1(R,Secret,ni); claim_r2(R,Secret,nr); claim_r3(R,Niagree); diff --git a/protocols/misc/boyd.spdl b/protocols/misc/boyd.spdl index 1ce9516..e112216 100644 --- a/protocols/misc/boyd.spdl +++ b/protocols/misc/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) ); @@ -39,9 +39,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)); claim_11 (R, Niagree); @@ -53,7 +53,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/protocols/misc/broken1.spdl b/protocols/misc/broken1.spdl index 800ca6a..983d598 100644 --- a/protocols/misc/broken1.spdl +++ b/protocols/misc/broken1.spdl @@ -20,13 +20,13 @@ protocol broken1(I,R,S) } role R { - read_3(S, R, {HelloWorld, S, I, R}k ); - read_1(I, R, PlainSight, {HelloWorld, I, R}k ); + recv_3(S, R, {HelloWorld, S, I, R}k ); + recv_1(I, R, PlainSight, {HelloWorld, I, R}k ); claim_4(R, Secret, PlainSight); } role S { - read_2(I, S, {HelloServer, I, S}k ); + recv_2(I, S, {HelloServer, I, S}k ); send_3(S, R, {HelloWorld, S, I, R}k ); } } diff --git a/protocols/misc/bunava-1-3.spdl b/protocols/misc/bunava-1-3.spdl index 5b5803a..711bf2b 100644 --- a/protocols/misc/bunava-1-3.spdl +++ b/protocols/misc/bunava-1-3.spdl @@ -20,7 +20,7 @@ protocol intruderhelp(Swap) var T: Ticket; var R0,R1: Agent; - read_!1(Swap,Swap, { T }k(R0,R1) ); + recv_!1(Swap,Swap, { T }k(R0,R1) ); send_!2(Swap,Swap, { T }k(R1,R0) ); } } @@ -33,7 +33,7 @@ protocol bunava13(R0,R1,R2) var n1,n2: Nonce; send_1(R0,R1, n0); - read_3(R2,R0, n2,{R2,n1,R1,n0}k(R0,R2) ); + recv_3(R2,R0, n2,{R2,n1,R1,n0}k(R0,R2) ); send_4(R0,R1, {R0,n2,R2,n1}k(R0,R1) ); claim_A1(R0, Niagree); @@ -45,9 +45,9 @@ protocol bunava13(R0,R1,R2) fresh n1: Nonce; var n0,n2: Nonce; - read_1(R0,R1, n0); + recv_1(R0,R1, n0); send_2(R1,R2, n1,{R1,n0}k(R1,R2) ); - read_4(R0,R1, {R0,n2,R2,n1}k(R0,R1) ); + recv_4(R0,R1, {R0,n2,R2,n1}k(R0,R1) ); send_5(R1,R2, {R1,R0,n2}k(R1,R2) ); claim_B1(R1, Niagree); @@ -59,9 +59,9 @@ protocol bunava13(R0,R1,R2) fresh n2: Nonce; var n0,n1: Nonce; - read_2(R1,R2, n1,{R1,n0}k(R1,R2) ); + recv_2(R1,R2, n1,{R1,n0}k(R1,R2) ); send_3(R2,R0, n2,{R2,n1,R1,n0}k(R0,R2) ); - read_5(R1,R2, {R1,R0,n2}k(R1,R2) ); + recv_5(R1,R2, {R1,R0,n2}k(R1,R2) ); claim_C1(R2, Niagree); claim_C2(R2, Nisynch); diff --git a/protocols/misc/bunava-1-4.spdl b/protocols/misc/bunava-1-4.spdl index a5be500..075e35d 100644 --- a/protocols/misc/bunava-1-4.spdl +++ b/protocols/misc/bunava-1-4.spdl @@ -21,7 +21,7 @@ protocol intruderhelp(Swap) var T: Ticket; var A,B: Agent; - read_!1(Swap,Swap, { T }k(A,B) ); + recv_!1(Swap,Swap, { T }k(A,B) ); send_!2(Swap,Swap, { T }k(B,A) ); } } @@ -34,7 +34,7 @@ protocol bunava14(A,B,C,D) var rb,rc,rd: Nonce; send_1(A,B, ra); - read_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) ); + recv_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) ); send_5(A,B, {A,rd,D,rc,C,rb}k(A,B) ); claim_A1(A, Niagree); @@ -46,9 +46,9 @@ protocol bunava14(A,B,C,D) fresh rb: Nonce; var ra,rc,rd: Nonce; - read_1(A,B, ra); + recv_1(A,B, ra); send_2(B,C, rb,{B,ra}k(B,C) ); - read_5(A,B, {A,rd,D,rc,C,rb}k(A,B) ); + recv_5(A,B, {A,rd,D,rc,C,rb}k(A,B) ); send_6(B,C, {B,A,rd,D,rc}k(B,C) ); claim_B1(B, Niagree); @@ -60,9 +60,9 @@ protocol bunava14(A,B,C,D) fresh rc: Nonce; var ra,rb,rd: Nonce; - read_2(B,C, rb,{B,ra}k(B,C) ); + recv_2(B,C, rb,{B,ra}k(B,C) ); send_3(C,D, rc,{C,rb,B,ra}k(C,D) ); - read_6(B,C, {B,A,rd,D,rc}k(B,C) ); + recv_6(B,C, {B,A,rd,D,rc}k(B,C) ); send_7(C,D, {C,B,A,rd}k(C,D) ); claim_C1(C, Niagree); @@ -74,9 +74,9 @@ protocol bunava14(A,B,C,D) fresh rd: Nonce; var ra,rb,rc: Nonce; - read_3(C,D, rc,{C,rb,B,ra}k(C,D) ); + recv_3(C,D, rc,{C,rb,B,ra}k(C,D) ); send_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) ); - read_7(C,D, {C,B,A,rd}k(C,D) ); + recv_7(C,D, {C,B,A,rd}k(C,D) ); claim_D1(D, Niagree); claim_D2(D, Nisynch); diff --git a/protocols/misc/bunava-2-3.spdl b/protocols/misc/bunava-2-3.spdl index af100ae..7c62732 100644 --- a/protocols/misc/bunava-2-3.spdl +++ b/protocols/misc/bunava-2-3.spdl @@ -16,7 +16,7 @@ protocol intruderhelp(Swap) var T: Ticket; var R0,R1: Agent; - read_!1(Swap,Swap, { T }k(R0,R1) ); + recv_!1(Swap,Swap, { T }k(R0,R1) ); send_!2(Swap,Swap, { T }k(R1,R0) ); } } @@ -30,7 +30,7 @@ protocol bunava23(R0,R1,R2) var T0: Ticket; send_1(R0,R1, n0); - read_3(R2,R0, n2, T0, { R2,{ R1,n0 }k(R0,R1) }k(R0,R2) ); + recv_3(R2,R0, n2, T0, { R2,{ R1,n0 }k(R0,R1) }k(R0,R2) ); send_4(R0,R1, { R0,n2 }k(R0,R2), { R0, T0 }k(R0,R1) ); claim_A1(R0, Niagree); @@ -43,9 +43,9 @@ protocol bunava23(R0,R1,R2) var n0,n2: Nonce; var T1: Ticket; - read_1(R0,R1, n0); + recv_1(R0,R1, n0); send_2(R1,R2, n1,{R1,n0}k(R1,R2) ); - read_4(R0,R1, T1, { R0, { R2,n1 }k(R1,R2) }k(R0,R1) ); + recv_4(R0,R1, T1, { R0, { R2,n1 }k(R1,R2) }k(R0,R1) ); send_5(R1,R2, { R1, T1 }k(R1,R2) ); claim_B1(R1, Niagree); @@ -58,9 +58,9 @@ protocol bunava23(R0,R1,R2) var n0,n1: Nonce; var T2: Ticket; - read_2(R1,R2, n1, T2 ); + recv_2(R1,R2, n1, T2 ); send_3(R2,R0, n2,{ R2,n1 }k(R1,R2), { R2, T2 }k(R0,R2) ); - read_5(R1,R2, { R1, { R0,n2 }k(R0,R2) }k(R1,R2) ); + recv_5(R1,R2, { R1, { R0,n2 }k(R0,R2) }k(R1,R2) ); claim_C1(R2, Niagree); claim_C2(R2, Nisynch); diff --git a/protocols/misc/bunava-2-4.spdl b/protocols/misc/bunava-2-4.spdl index 3311d62..999529a 100644 --- a/protocols/misc/bunava-2-4.spdl +++ b/protocols/misc/bunava-2-4.spdl @@ -18,7 +18,7 @@ secret k: Function; # var T: Ticket; # var A,B: Agent; # -# read_1(Swap,Swap, { T }k(A,B) ); +# recv_1(Swap,Swap, { T }k(A,B) ); # send_2(Swap,Swap, { T }k(B,A) ); # } # } @@ -32,7 +32,7 @@ protocol bunava24(A,B,C,D) var Tacd, Tabd: Ticket; send_1(A,B, ra); - read_4(D,A, rd, + recv_4(D,A, rd, Tacd, Tabd, { D, { C, { B,ra }k(A,B) }k(A,C) }k(A,D) @@ -53,11 +53,11 @@ protocol bunava24(A,B,C,D) var ra,rc,rd: Nonce; var Tbad, Tbac: Ticket; - read_1(A,B, ra); + recv_1(A,B, ra); send_2(B,C, rb, { B,ra }k(A,B) ); -# read_5(A,B, +# recv_5(A,B, # Tbad, # Tbac, # { A, { D, { C,rb }k(B,C) }k(B,D) }k(A,B) @@ -77,12 +77,12 @@ protocol bunava24(A,B,C,D) var ra,rb,rd: Nonce; var Tcab,Tcbd: Ticket; - read_2(B,C, rb, Tcab ); + recv_2(B,C, rb, Tcab ); send_3(C,D, rc, { C, rb }k(B,C), { C, Tcab }k(A,C) ); -# read_6(B,C, +# recv_6(B,C, # Tcbd, # { B, { A,{ D,rc }k(C,D) }k(A,C) }k(B,C) # ); @@ -100,13 +100,13 @@ protocol bunava24(A,B,C,D) var ra,rb,rc: Nonce; var Tdbc,Tdac: Ticket; - read_3(C,D, rc, Tdbc, Tdac ); + recv_3(C,D, rc, Tdbc, Tdac ); send_4(D,A, rd, { D, rc }k(C,D), { D, Tdbc }k(B,D), { D, Tdac }k(A,D) ); -# read_7(C,D, +# recv_7(C,D, # { C, { B,{ A,rd }k(A,D) }k(B,D) }k(C,D) # ); # diff --git a/protocols/misc/carkey-broken-limited.spdl b/protocols/misc/carkey-broken-limited.spdl index 91a75a4..c53509c 100644 --- a/protocols/misc/carkey-broken-limited.spdl +++ b/protocols/misc/carkey-broken-limited.spdl @@ -15,7 +15,7 @@ protocol carkeybrokenlim(I,R) { var ni: Nonce; - read_1(I,R, I,R ); + recv_1(I,R, I,R ); claim_2(R,Nisynch); } } diff --git a/protocols/misc/carkey-broken.spdl b/protocols/misc/carkey-broken.spdl index 8ad0198..4fdc927 100644 --- a/protocols/misc/carkey-broken.spdl +++ b/protocols/misc/carkey-broken.spdl @@ -15,7 +15,7 @@ protocol carkeybroken(I,R) { var ni: Nonce; - read_1(I,R, {ni}sk(I) ); + recv_1(I,R, {ni}sk(I) ); claim_2(R,Nisynch); } } diff --git a/protocols/misc/carkey-ni.spdl b/protocols/misc/carkey-ni.spdl index ec809fc..22d66fe 100644 --- a/protocols/misc/carkey-ni.spdl +++ b/protocols/misc/carkey-ni.spdl @@ -15,7 +15,7 @@ protocol carkeyni(I,R) { var ni: Nonce; - read_1(I,R, {R,ni}sk(I) ); + recv_1(I,R, {R,ni}sk(I) ); claim_2(R,Nisynch); } } diff --git a/protocols/misc/carkey-ni2.spdl b/protocols/misc/carkey-ni2.spdl index e6e5551..7b33b6c 100644 --- a/protocols/misc/carkey-ni2.spdl +++ b/protocols/misc/carkey-ni2.spdl @@ -16,8 +16,8 @@ protocol carkeyni2(I,R) { var ni: Nonce; - read_1(I,R, {R,ni}sk(I) ); - read_2(I,R, {R,ni}sk(I) ); + recv_1(I,R, {R,ni}sk(I) ); + recv_2(I,R, {R,ni}sk(I) ); claim_4(R,Nisynch); } } diff --git a/protocols/misc/ccitt509-ban.spdl b/protocols/misc/ccitt509-ban.spdl index 23e26b6..04e617d 100644 --- a/protocols/misc/ccitt509-ban.spdl +++ b/protocols/misc/ccitt509-ban.spdl @@ -13,7 +13,7 @@ protocol ccitt509(I,R) var yr,xr: Data; send_1(I,R, I,{ni, R, xi, {yi}pk(R) }sk(I) ); - read_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) ); + recv_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) ); send_3(I,R, I,{R,nr}sk(I) ); claim_4(I,Secret,yi); @@ -29,9 +29,9 @@ protocol ccitt509(I,R) fresh nr: Nonce; fresh yr,xr: Data; - read_1(I,R, I,{ni, R, xi, {yi}pk(R) }sk(I) ); + recv_1(I,R, I,{ni, R, xi, {yi}pk(R) }sk(I) ); send_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) ); - read_3(I,R, I,{R,nr}sk(I) ); + recv_3(I,R, I,{R,nr}sk(I) ); claim_8(R,Secret,yi); claim_9(R,Secret,yr); diff --git a/protocols/misc/compositionality-examples/th-1.spdl b/protocols/misc/compositionality-examples/th-1.spdl index a69cf2d..7701da0 100644 --- a/protocols/misc/compositionality-examples/th-1.spdl +++ b/protocols/misc/compositionality-examples/th-1.spdl @@ -11,8 +11,8 @@ protocol nsl3th1(I,R) var nr: Nonce; send_1(I,R, {P1,I,ni}pk(R) ); - read_1b(R,I, {nr}pk(I) ); - read_2(R,I, {P1,ni,nr,R}pk(I) ); + recv_1b(R,I, {nr}pk(I) ); + recv_2(R,I, {P1,ni,nr,R}pk(I) ); send_3(I,R, {P1,nr}pk(R) ); claim_i(I,Nisynch); @@ -23,10 +23,10 @@ protocol nsl3th1(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {P1,I,ni}pk(R) ); + recv_1(I,R, {P1,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); send_2(R,I, {P1,ni,nr,R}pk(I) ); - read_3(I,R, {P1,nr}pk(R) ); + recv_3(I,R, {P1,nr}pk(R) ); claim_r(R,Nisynch); } diff --git a/protocols/misc/compositionality-examples/th-1par2.spdl b/protocols/misc/compositionality-examples/th-1par2.spdl index 82451a1..9673ff9 100644 --- a/protocols/misc/compositionality-examples/th-1par2.spdl +++ b/protocols/misc/compositionality-examples/th-1par2.spdl @@ -13,8 +13,8 @@ protocol nsl3th1(I,R) var nr: Nonce; send_1(I,R, {P1,I,ni}pk(R) ); - read_1b(R,I, {nr}pk(I) ); - read_2(R,I, {P1,ni,nr,R}pk(I) ); + recv_1b(R,I, {nr}pk(I) ); + recv_2(R,I, {P1,ni,nr,R}pk(I) ); send_3(I,R, {P1,nr}pk(R) ); claim_i(I,Nisynch); @@ -25,10 +25,10 @@ protocol nsl3th1(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {P1,I,ni}pk(R) ); + recv_1(I,R, {P1,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); send_2(R,I, {P1,ni,nr,R}pk(I) ); - read_3(I,R, {P1,nr}pk(R) ); + recv_3(I,R, {P1,nr}pk(R) ); claim_r(R,Nisynch); } @@ -45,8 +45,8 @@ protocol nsl3th2(I,R) var nr: Nonce; send_1(I,R, {P2,I,ni}pk(R) ); - read_1b(R,I, {nr}pk(I) ); - read_2(R,I, {P2,ni,nr,R}pk(I) ); + recv_1b(R,I, {nr}pk(I) ); + recv_2(R,I, {P2,ni,nr,R}pk(I) ); send_3(I,R, {P2,nr}pk(R) ); claim_i(I,Nisynch); @@ -57,10 +57,10 @@ protocol nsl3th2(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {P2,I,ni}pk(R) ); + recv_1(I,R, {P2,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); send_2(R,I, {P2,ni,nr,R}pk(I) ); - read_3(I,R, {P2,nr}pk(R) ); + recv_3(I,R, {P2,nr}pk(R) ); claim_r(R,Nisynch); } diff --git a/protocols/misc/compositionality-examples/th-1seq2-rename-ni.spdl b/protocols/misc/compositionality-examples/th-1seq2-rename-ni.spdl index 082db56..afe0410 100644 --- a/protocols/misc/compositionality-examples/th-1seq2-rename-ni.spdl +++ b/protocols/misc/compositionality-examples/th-1seq2-rename-ni.spdl @@ -12,15 +12,15 @@ protocol nsl3th3ni(I,R) var nr,nr2: Nonce; send_1(I,R, {P1,I,ni}pk(R) ); - read_1b(R,I, {nr}pk(I) ); - read_2(R,I, {P1,ni,nr,R}pk(I) ); + recv_1b(R,I, {nr}pk(I) ); + recv_2(R,I, {P1,ni,nr,R}pk(I) ); send_3(I,R, {P1,nr}pk(R) ); //claim_i(I,Nisynch); send_21(I,R, {P2,I,ni}pk(R) ); - read_21b(R,I, {nr2}pk(I) ); - read_22(R,I, {P2,ni,nr2,R}pk(I) ); + recv_21b(R,I, {nr2}pk(I) ); + recv_22(R,I, {P2,ni,nr2,R}pk(I) ); send_23(I,R, {P2,nr2}pk(R) ); claim_i2(I,Nisynch); @@ -31,17 +31,17 @@ protocol nsl3th3ni(I,R) var ni,ni: Nonce; fresh nr,nr2: Nonce; - read_1(I,R, {P1,I,ni}pk(R) ); + recv_1(I,R, {P1,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); send_2(R,I, {P1,ni,nr,R}pk(I) ); - read_3(I,R, {P1,nr}pk(R) ); + recv_3(I,R, {P1,nr}pk(R) ); //claim_r(R,Nisynch); - read_21(I,R, {P2,I,ni}pk(R) ); + recv_21(I,R, {P2,I,ni}pk(R) ); send_21b(R,I, {nr2}pk(I) ); send_22(R,I, {P2,ni,nr2,R}pk(I) ); - read_23(I,R, {P2,nr2}pk(R) ); + recv_23(I,R, {P2,nr2}pk(R) ); claim_r2(R,Nisynch); } diff --git a/protocols/misc/compositionality-examples/th-1seq2-rename-nr.spdl b/protocols/misc/compositionality-examples/th-1seq2-rename-nr.spdl index 3e016f9..7d50d9a 100644 --- a/protocols/misc/compositionality-examples/th-1seq2-rename-nr.spdl +++ b/protocols/misc/compositionality-examples/th-1seq2-rename-nr.spdl @@ -12,15 +12,15 @@ protocol nsl3th3nr(I,R) var nr,nr: Nonce; send_1(I,R, {P1,I,ni}pk(R) ); - read_1b(R,I, {nr}pk(I) ); - read_2(R,I, {P1,ni,nr,R}pk(I) ); + recv_1b(R,I, {nr}pk(I) ); + recv_2(R,I, {P1,ni,nr,R}pk(I) ); send_3(I,R, {P1,nr}pk(R) ); //claim_i(I,Nisynch); send_21(I,R, {P2,I,ni2}pk(R) ); - read_21b(R,I, {nr}pk(I) ); - read_22(R,I, {P2,ni2,nr,R}pk(I) ); + recv_21b(R,I, {nr}pk(I) ); + recv_22(R,I, {P2,ni2,nr,R}pk(I) ); send_23(I,R, {P2,nr}pk(R) ); claim_i2(I,Nisynch); @@ -31,17 +31,17 @@ protocol nsl3th3nr(I,R) var ni,ni2: Nonce; fresh nr,nr: Nonce; - read_1(I,R, {P1,I,ni}pk(R) ); + recv_1(I,R, {P1,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); send_2(R,I, {P1,ni,nr,R}pk(I) ); - read_3(I,R, {P1,nr}pk(R) ); + recv_3(I,R, {P1,nr}pk(R) ); //claim_r(R,Nisynch); - read_21(I,R, {P2,I,ni2}pk(R) ); + recv_21(I,R, {P2,I,ni2}pk(R) ); send_21b(R,I, {nr}pk(I) ); send_22(R,I, {P2,ni2,nr,R}pk(I) ); - read_23(I,R, {P2,nr}pk(R) ); + recv_23(I,R, {P2,nr}pk(R) ); claim_r2(R,Nisynch); } diff --git a/protocols/misc/compositionality-examples/th-1seq2.spdl b/protocols/misc/compositionality-examples/th-1seq2.spdl index 6e50f3c..d3f689d 100644 --- a/protocols/misc/compositionality-examples/th-1seq2.spdl +++ b/protocols/misc/compositionality-examples/th-1seq2.spdl @@ -12,15 +12,15 @@ protocol nsl3th3(I,R) var nr,nr2: Nonce; send_1(I,R, {P1,I,ni}pk(R) ); - read_1b(R,I, {nr}pk(I) ); - read_2(R,I, {P1,ni,nr,R}pk(I) ); + recv_1b(R,I, {nr}pk(I) ); + recv_2(R,I, {P1,ni,nr,R}pk(I) ); send_3(I,R, {P1,nr}pk(R) ); //claim_i(I,Nisynch); send_21(I,R, {P2,I,ni2}pk(R) ); - read_21b(R,I, {nr2}pk(I) ); - read_22(R,I, {P2,ni2,nr2,R}pk(I) ); + recv_21b(R,I, {nr2}pk(I) ); + recv_22(R,I, {P2,ni2,nr2,R}pk(I) ); send_23(I,R, {P2,nr2}pk(R) ); claim_i2(I,Nisynch); @@ -31,17 +31,17 @@ protocol nsl3th3(I,R) var ni,ni2: Nonce; fresh nr,nr2: Nonce; - read_1(I,R, {P1,I,ni}pk(R) ); + recv_1(I,R, {P1,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); send_2(R,I, {P1,ni,nr,R}pk(I) ); - read_3(I,R, {P1,nr}pk(R) ); + recv_3(I,R, {P1,nr}pk(R) ); //claim_r(R,Nisynch); - read_21(I,R, {P2,I,ni2}pk(R) ); + recv_21(I,R, {P2,I,ni2}pk(R) ); send_21b(R,I, {nr2}pk(I) ); send_22(R,I, {P2,ni2,nr2,R}pk(I) ); - read_23(I,R, {P2,nr2}pk(R) ); + recv_23(I,R, {P2,nr2}pk(R) ); claim_r2(R,Nisynch); } diff --git a/protocols/misc/compositionality-examples/th-2.spdl b/protocols/misc/compositionality-examples/th-2.spdl index 3332085..74cd657 100644 --- a/protocols/misc/compositionality-examples/th-2.spdl +++ b/protocols/misc/compositionality-examples/th-2.spdl @@ -11,8 +11,8 @@ protocol nsl3th2(I,R) var nr: Nonce; send_1(I,R, {P2,I,ni}pk(R) ); - read_1b(R,I, {nr}pk(I) ); - read_2(R,I, {P2,ni,nr,R}pk(I) ); + recv_1b(R,I, {nr}pk(I) ); + recv_2(R,I, {P2,ni,nr,R}pk(I) ); send_3(I,R, {P2,nr}pk(R) ); claim_i(I,Nisynch); @@ -23,10 +23,10 @@ protocol nsl3th2(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {P2,I,ni}pk(R) ); + recv_1(I,R, {P2,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); send_2(R,I, {P2,ni,nr,R}pk(I) ); - read_3(I,R, {P2,nr}pk(R) ); + recv_3(I,R, {P2,nr}pk(R) ); claim_r(R,Nisynch); } diff --git a/protocols/misc/denning-sacco-shared.spdl b/protocols/misc/denning-sacco-shared.spdl index 0756c3b..d5e61ad 100644 --- a/protocols/misc/denning-sacco-shared.spdl +++ b/protocols/misc/denning-sacco-shared.spdl @@ -39,7 +39,7 @@ protocol denningsaccosh(A,S,B) var kab: SessionKey; send_1 (A,S, A,S ); - read_2 (S,A, {B, kab, t, T}k(A,S) ); + recv_2 (S,A, {B, kab, t, T}k(A,S) ); send_3 (A,B, T); claim_4 (A, Secret, kab); @@ -52,7 +52,7 @@ protocol denningsaccosh(A,S,B) fresh t: Time; fresh kab: SessionKey; - read_1 (A,S, A,S ); + recv_1 (A,S, A,S ); send_2 (S,A, {B, kab, t, { kab, A,t }k(B,S) }k(A,S) ); } @@ -61,7 +61,7 @@ protocol denningsaccosh(A,S,B) var t: Time; var kab: SessionKey; - read_3 (A,B, { kab, A,t }k(B,S) ); + recv_3 (A,B, { kab, A,t }k(B,S) ); claim_7 (B, Secret, kab); claim_8 (B, Nisynch); diff --git a/protocols/misc/f4.spdl b/protocols/misc/f4.spdl index 5b43bbb..f1a6987 100644 --- a/protocols/misc/f4.spdl +++ b/protocols/misc/f4.spdl @@ -19,9 +19,9 @@ protocol f4(I,R) { var nr: Nonce; - read_!1(R,I, nr ); + recv_!1(R,I, nr ); send_!2(I,R, { nr }sk(I) ); - read_!3(R,I, {{{{ nr }sk(R)}sk(R)}sk(R)}sk(R) ); + recv_!3(R,I, {{{{ nr }sk(R)}sk(R)}sk(R)}sk(R) ); claim_i1(I,Reachable); } diff --git a/protocols/misc/f5.spdl b/protocols/misc/f5.spdl index 860c165..c5eb3b7 100644 --- a/protocols/misc/f5.spdl +++ b/protocols/misc/f5.spdl @@ -19,9 +19,9 @@ protocol f5(I,R) { var nr: Nonce; - read_!1(R,I, nr ); + recv_!1(R,I, nr ); send_!2(I,R, { nr }sk(I) ); - read_!3(R,I, {{{{{ nr }sk(R)}sk(R)}sk(R)}sk(R)}sk(R) ); + recv_!3(R,I, {{{{{ nr }sk(R)}sk(R)}sk(R)}sk(R)}sk(R) ); claim_i1(I,Reachable); } diff --git a/protocols/misc/five-run-bound.spdl b/protocols/misc/five-run-bound.spdl index ee8d4c3..0e985ba 100644 --- a/protocols/misc/five-run-bound.spdl +++ b/protocols/misc/five-run-bound.spdl @@ -10,9 +10,9 @@ protocol r5bound(I,R) var ni: Nonce; fresh k2: Nonce; - read_!1 (I,R, ni ); + recv_!1 (I,R, ni ); send_!2 (R,I, { ni }sk(R) ); - read_!3 (I,R, {{{ {k1}pk(R) }sk(I)}sk(I)}sk(I) ); + recv_!3 (I,R, {{{ {k1}pk(R) }sk(I)}sk(I)}sk(I) ); send_!4 (R,I, {k2}k1 ); claim_6 (R, Secret, k2); diff --git a/protocols/misc/fourway-HSDDM05.cpp b/protocols/misc/fourway-HSDDM05.cpp index 5992e13..5602748 100644 --- a/protocols/misc/fourway-HSDDM05.cpp +++ b/protocols/misc/fourway-HSDDM05.cpp @@ -26,9 +26,9 @@ protocol fourway(X,Y) var y: Nonce; send_1( X,Y, x,msg1 ); - read_2( Y,X, y,msg2,hash( ptk,y,msg2 ) ); + recv_2( Y,X, y,msg2,hash( ptk,y,msg2 ) ); send_3( X,Y, x,msg3,hash( ptk,x,msg3 ) ); - read_4( Y,X, msg4,hash( ptk,msg4 ) ); + recv_4( Y,X, msg4,hash( ptk,msg4 ) ); claim_X1( X, Secret, ptk ); claim_X2( X, Niagree ); @@ -39,9 +39,9 @@ protocol fourway(X,Y) var x: Nonce; fresh y: Nonce; - read_1( X,Y, x,msg1 ); + recv_1( X,Y, x,msg1 ); send_2( Y,X, y,msg2,hash( ptk,y,msg2 ) ); - read_3( X,Y, x,msg3,hash( ptk,x,msg3 ) ); + recv_3( X,Y, x,msg3,hash( ptk,x,msg3 ) ); send_4( Y,X, msg4,hash( ptk,msg4 ) ); claim_Y1( Y, Secret, ptk ); diff --git a/protocols/misc/fourway-HSDDM05.spdl b/protocols/misc/fourway-HSDDM05.spdl index 4a91a9e..3f24ee8 100644 --- a/protocols/misc/fourway-HSDDM05.spdl +++ b/protocols/misc/fourway-HSDDM05.spdl @@ -22,9 +22,9 @@ protocol fourway(X,Y) var y: Nonce; send_1( X,Y, x,msg1 ); - read_2( Y,X, y,msg2,hash( hash( pmk(X,Y),x,y ),y,msg2 ) ); + recv_2( Y,X, y,msg2,hash( hash( pmk(X,Y),x,y ),y,msg2 ) ); send_3( X,Y, x,msg3,hash( hash( pmk(X,Y),x,y ),x,msg3 ) ); - read_4( Y,X, msg4,hash( hash( pmk(X,Y),x,y ),msg4 ) ); + recv_4( Y,X, msg4,hash( hash( pmk(X,Y),x,y ),msg4 ) ); claim_X1( X, Secret, hash( pmk(X,Y),x,y ) ); claim_X2( X, Niagree ); @@ -35,9 +35,9 @@ protocol fourway(X,Y) var x: Nonce; fresh y: Nonce; - read_1( X,Y, x,msg1 ); + recv_1( X,Y, x,msg1 ); send_2( Y,X, y,msg2,hash( hash( pmk(X,Y),x,y ),y,msg2 ) ); - read_3( X,Y, x,msg3,hash( hash( pmk(X,Y),x,y ),x,msg3 ) ); + recv_3( X,Y, x,msg3,hash( hash( pmk(X,Y),x,y ),x,msg3 ) ); send_4( Y,X, msg4,hash( hash( pmk(X,Y),x,y ),msg4 ) ); claim_Y1( Y, Secret, hash( pmk(X,Y),x,y ) ); diff --git a/protocols/misc/gong-nonce-b.spdl b/protocols/misc/gong-nonce-b.spdl index c9e85c0..58c2816 100644 --- a/protocols/misc/gong-nonce-b.spdl +++ b/protocols/misc/gong-nonce-b.spdl @@ -20,7 +20,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); @@ -36,9 +36,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); @@ -52,9 +52,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/protocols/misc/gong-nonce.spdl b/protocols/misc/gong-nonce.spdl index 6cfb50c..c7f3209 100644 --- a/protocols/misc/gong-nonce.spdl +++ b/protocols/misc/gong-nonce.spdl @@ -12,7 +12,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); @@ -28,9 +28,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); @@ -43,9 +43,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/protocols/misc/ibe-ns.spdl b/protocols/misc/ibe-ns.spdl index f96db64..4839341 100644 --- a/protocols/misc/ibe-ns.spdl +++ b/protocols/misc/ibe-ns.spdl @@ -18,9 +18,9 @@ protocol ibe(I,R,S) var nr: Nonce; //Note that we are not interested in the order of server messages. - read_!1(S,I, param(S) ); + recv_!1(S,I, param(S) ); send_3(I,R, {I,ni}ibepublic(param(S),R) ); - read_4(R,I, {ni,nr,R}ibepublic(param(S),I) ); + recv_4(R,I, {ni,nr,R}ibepublic(param(S),I) ); send_5(I,R, {nr}ibepublic(param(S),R) ); @@ -35,10 +35,10 @@ protocol ibe(I,R,S) var ni: Nonce; fresh nr: Nonce; - read_!2(S,R, {ibesecret(param(S),R)}pk(R) ); - read_3(I,R, {I,ni}ibepublic(param(S),R) ); + recv_!2(S,R, {ibesecret(param(S),R)}pk(R) ); + recv_3(I,R, {I,ni}ibepublic(param(S),R) ); send_4(R,I, {ni,nr,R}ibepublic(param(S),I) ); - read_5(I,R, {nr}ibepublic(param(S),R) ); + recv_5(I,R, {nr}ibepublic(param(S),R) ); claim_r1(R,Secret,ni); claim_r2(R,Secret,nr); @@ -48,7 +48,7 @@ protocol ibe(I,R,S) role S { - read_!0(S,S, R,S); // workaround for the fact that R & S are roles, so Scyther should not jump to conclusions (remove it and see what happens) + recv_!0(S,S, R,S); // workaround for the fact that R & S are roles, so Scyther should not jump to conclusions (remove it and see what happens) send_!1(S,I, param(S) ); send_!2(S,R, {ibesecret(param(S),R)}pk(R) ); diff --git a/protocols/misc/ibe.spdl b/protocols/misc/ibe.spdl index d1b23d6..f62d50d 100644 --- a/protocols/misc/ibe.spdl +++ b/protocols/misc/ibe.spdl @@ -16,7 +16,7 @@ protocol ibe(I,R,S) { fresh ni: Nonce; - read_1(S,I, param(S) ); + recv_1(S,I, param(S) ); send_3(I,R, {ni}ibepublic(param(S),R) ); claim_i1(I,Secret,ni); @@ -26,8 +26,8 @@ protocol ibe(I,R,S) { var ni: Nonce; - read_2(S,R, {ibesecret(param(S),R)}pk(R) ); - read_3(I,R, {ni}ibepublic(param(S),R) ); + recv_2(S,R, {ibesecret(param(S),R)}pk(R) ); + recv_3(I,R, {ni}ibepublic(param(S),R) ); claim_r1(R,Secret,ni); //of course this claim is invalid diff --git a/protocols/misc/isoiec11770-2-13.spdl b/protocols/misc/isoiec11770-2-13.spdl index 4790421..808b698 100644 --- a/protocols/misc/isoiec11770-2-13.spdl +++ b/protocols/misc/isoiec11770-2-13.spdl @@ -11,7 +11,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); } @@ -23,9 +23,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); @@ -36,7 +36,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/protocols/misc/kaochow-palm.spdl b/protocols/misc/kaochow-palm.spdl index 9401811..69e34d8 100644 --- a/protocols/misc/kaochow-palm.spdl +++ b/protocols/misc/kaochow-palm.spdl @@ -11,7 +11,7 @@ protocol kaochowPalm(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_5 (I, Nisynch); @@ -26,9 +26,9 @@ protocol kaochowPalm(I,R,S) var kir: Sessionkey; var T; - read_2 (S,R, { T, { I,R,ni,kir }k(R,S) }k(R,S) ); + recv_2 (S,R, { T, { I,R,ni,kir }k(R,S) }k(R,S) ); send_3 (R,I, T, {ni}kir, nr ); - read_4 (I,R, {nr}kir ); + recv_4 (I,R, {nr}kir ); claim_8 (R, Nisynch); claim_9 (R, Niagree); @@ -40,7 +40,7 @@ protocol kaochowPalm(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) }k(R,S) ); } } diff --git a/protocols/misc/kaochow-v2.spdl b/protocols/misc/kaochow-v2.spdl index 0265f3c..cbaee8e 100644 --- a/protocols/misc/kaochow-v2.spdl +++ b/protocols/misc/kaochow-v2.spdl @@ -11,7 +11,7 @@ protocol kaochow2(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_5 (I, Nisynch); @@ -26,9 +26,9 @@ protocol kaochow2(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_8 (R, Nisynch); claim_9 (R, Niagree); @@ -40,7 +40,7 @@ protocol kaochow2(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/protocols/misc/kaochow-v3.spdl b/protocols/misc/kaochow-v3.spdl index 61f6a7a..8a49ae6 100644 --- a/protocols/misc/kaochow-v3.spdl +++ b/protocols/misc/kaochow-v3.spdl @@ -13,7 +13,7 @@ protocol kaochow3(I,R,S) var T2: Ticket; send_1 (I,S, I,R,ni); - read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); + recv_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); send_4 (I,R, {nr,kir}kt, T2 ); claim_5 (I, Nisynch); @@ -29,9 +29,9 @@ protocol kaochow3(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, R, 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_8 (R, Nisynch); claim_9 (R, Niagree); @@ -43,7 +43,7 @@ protocol kaochow3(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/protocols/misc/kaochow.spdl b/protocols/misc/kaochow.spdl index 198d737..2c0de71 100644 --- a/protocols/misc/kaochow.spdl +++ b/protocols/misc/kaochow.spdl @@ -11,7 +11,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_5 (I, Nisynch); @@ -26,9 +26,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_8 (R, Nisynch); claim_9 (R, Niagree); @@ -40,7 +40,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/protocols/misc/kerberos-rddm.spdl b/protocols/misc/kerberos-rddm.spdl index 95c0598..2b4bdff 100644 --- a/protocols/misc/kerberos-rddm.spdl +++ b/protocols/misc/kerberos-rddm.spdl @@ -17,7 +17,7 @@ protocol @swapkey-ktk(I,R) var T:Ticket; - read_!X1(R,I,{T}ktk(I,R)); + recv_!X1(R,I,{T}ktk(I,R)); send_!X2(I,R,{T}ktk(R,I)); } role R @@ -32,7 +32,7 @@ protocol @swapkey-kck(I,R) var T:Ticket; - read_!X1(R,I,{T}kck(I,R)); + recv_!X1(R,I,{T}kck(I,R)); send_!X2(I,R,{T}kck(R,I)); } role R @@ -47,7 +47,7 @@ protocol @swapkey-kst(I,R) var T:Ticket; - read_!X1(R,I,{T}kst(I,R)); + recv_!X1(R,I,{T}kst(I,R)); send_!X2(I,R,{T}kst(R,I)); } role R @@ -67,17 +67,17 @@ protocol kerberos(C,K,T,S) { fresh t: Text; send_1(C,K, C,T,n1); - read_2(K,C, tgt, { AKey,n1,T }kck(C,K) ); + recv_2(K,C, tgt, { AKey,n1,T }kck(C,K) ); // Stage boundary send_3(C,T, tgt, { C }AKey,C,S,n2 ); - read_4(T,C, C, st, { SKey, n2, S }AKey ); + recv_4(T,C, C, st, { SKey, n2, S }AKey ); // Stage boundary send_5(C,S, st, { C,t }SKey ); - read_6(S,C, { t }SKey ); + recv_6(S,C, { t }SKey ); // Theorem 5 (a) // If C,K are honest @@ -96,7 +96,7 @@ protocol kerberos(C,K,T,S) { var n1: Nonce; fresh AKey: Sessionkey; - read_1(C,K, C,T,n1); + recv_1(C,K, C,T,n1); send_2(K,C, { AKey, C }ktk(T,K), { AKey,n1,T }kck(C,K) ); // Theorem 6 (a) // If C,K,T are all honest @@ -108,7 +108,7 @@ protocol kerberos(C,K,T,S) { var n2: Nonce; fresh SKey: Sessionkey; - read_3(C,T, { AKey, C }ktk(T,K), { C }AKey,C,S,n2 ); + recv_3(C,T, { AKey, C }ktk(T,K), { C }AKey,C,S,n2 ); send_4(T,C, C,{ SKey, C }kst(S,T), { SKey, n2, S }AKey ); // Theorem 5 (a) @@ -125,7 +125,7 @@ protocol kerberos(C,K,T,S) { var t: Text; var SKey: Sessionkey; - read_5(C,S, { SKey, C }kst(S,T), { C,t }SKey ); + recv_5(C,S, { SKey, C }kst(S,T), { C,t }SKey ); send_6(S,C, { t }SKey ); // Theorem 7 (b) // If C,K,S,T are honest diff --git a/protocols/misc/ksl.spdl b/protocols/misc/ksl.spdl index a0b2eda..eecce4d 100644 --- a/protocols/misc/ksl.spdl +++ b/protocols/misc/ksl.spdl @@ -29,11 +29,11 @@ protocol ksl(A,B,S) var Kab: SessionKey; send_1(A,B, Na, A); - read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab ); + recv_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab ); send_5(A,B, { Nc }Kab ); send_6(A,B, Ma,T ); - read_7(B,A, Mb,{Ma}Kab ); + recv_7(B,A, Mb,{Ma}Kab ); send_8(A,B, {Mb}Kab ); claim_A1(A,Secret, Kab); @@ -50,15 +50,15 @@ protocol ksl(A,B,S) fresh Tb: GeneralizedTimestamp; var T: Ticket; - read_1(A,B, Na, A); + recv_1(A,B, Na, A); send_2(B,S, Na, A, Nb, B ); - read_3(S,B, { Nb, A, Kab }k(B,S), T ); + recv_3(S,B, { Nb, A, Kab }k(B,S), T ); send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab ); - read_5(A,B, { Nc }Kab ); + recv_5(A,B, { Nc }Kab ); - read_6(A,B, Ma,{ Tb, A, Kab }Kbb ); + recv_6(A,B, Ma,{ Tb, A, Kab }Kbb ); send_7(B,A, Mb,{Ma}Kab ); - read_8(A,B, {Mb}Kab ); + recv_8(A,B, {Mb}Kab ); claim_B1(B,Secret, Kab); claim_B2(B,Niagree); @@ -70,7 +70,7 @@ protocol ksl(A,B,S) var Na, Nb: Nonce; fresh Kab: SessionKey; - read_2(B,S, Na, A, Nb, B ); + recv_2(B,S, Na, A, Nb, B ); send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) ); } } diff --git a/protocols/misc/localclaims-breaker.spdl b/protocols/misc/localclaims-breaker.spdl index 3abbb42..c1fb418 100644 --- a/protocols/misc/localclaims-breaker.spdl +++ b/protocols/misc/localclaims-breaker.spdl @@ -20,10 +20,10 @@ protocol lcbreaker(I,R) var x: Nonce; send_1(I,R, {I,ni}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,I}pk(R) ); - read_x1(R,I, { x }pk(I) ); + recv_x1(R,I, { x }pk(I) ); send_x2(I,R, { x }ni ); claim_i1(I,Secret,ni); @@ -36,12 +36,12 @@ protocol lcbreaker(I,R) fresh nr: Nonce; fresh x: Nonce; - read_1(I,R, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); - read_3(I,R, {nr,I}pk(R) ); + recv_3(I,R, {nr,I}pk(R) ); send_x1(R,I, { x }pk(I) ); - read_x2(I,R, { x }ni ); + recv_x2(I,R, { x }ni ); claim_r1(R,Secret,ni); claim_r2(R,Secret,nr); diff --git a/protocols/misc/localclaims-seq1.spdl b/protocols/misc/localclaims-seq1.spdl index 059159b..1bd7256 100644 --- a/protocols/misc/localclaims-seq1.spdl +++ b/protocols/misc/localclaims-seq1.spdl @@ -20,10 +20,10 @@ protocol lcbreakerS1(I,R) var x: Nonce; send_1(I,R, {I,ni}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,I}pk(R) ); - read_x1(R,I, { x }pk(I) ); + recv_x1(R,I, { x }pk(I) ); send_x2(I,R, { x }ni ); send_lc(I,R, {ni2}pk(R) ); @@ -39,14 +39,14 @@ protocol lcbreakerS1(I,R) fresh nr: Nonce; fresh x: Nonce; - read_1(I,R, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); - read_3(I,R, {nr,I}pk(R) ); + recv_3(I,R, {nr,I}pk(R) ); send_x1(R,I, { x }pk(I) ); - read_x2(I,R, { x }ni ); + recv_x2(I,R, { x }ni ); - read_lc(I,R, {ni2}pk(R) ); + recv_lc(I,R, {ni2}pk(R) ); claim_r0(R,Secret,ni2); claim_r1(R,Secret,ni); diff --git a/protocols/misc/localclaims.spdl b/protocols/misc/localclaims.spdl index 1623b5f..cc285bb 100644 --- a/protocols/misc/localclaims.spdl +++ b/protocols/misc/localclaims.spdl @@ -25,7 +25,7 @@ protocol localclaims(I,R) { var ni: Nonce; - read_1(I,R, {ni}pk(R) ); + recv_1(I,R, {ni}pk(R) ); claim_r1(R,Secret,ni); } diff --git a/protocols/misc/ns-symmetric-amended.spdl b/protocols/misc/ns-symmetric-amended.spdl index d000f1b..1b9a696 100644 --- a/protocols/misc/ns-symmetric-amended.spdl +++ b/protocols/misc/ns-symmetric-amended.spdl @@ -41,11 +41,11 @@ protocol nssymmetricamended(A,S,B) var nb: Nonce; send_1(A,B, A ); - read_2(B,A, T1 ); + recv_2(B,A, T1 ); send_3(A,S, A,B,na,T1 ); - read_4(S,A, { na,B,kab,T2 }k(A,S) ); + recv_4(S,A, { na,B,kab,T2 }k(A,S) ); send_5(A,B, T2 ); - read_6(B,A, { nb }kab ); + recv_6(B,A, { nb }kab ); send_7(A,B, { {nb}succ }kab ); claim_8(A, Secret, kab); @@ -59,7 +59,7 @@ protocol nssymmetricamended(A,S,B) var na: Nonce; var nb: Nonce; - read_3(A,S, A,B,na, { A,nb }k(B,S) ); + recv_3(A,S, A,B,na, { A,nb }k(B,S) ); send_4(S,A, { na,B,kab, { kab,A }k(B,S) }k(A,S) ); } @@ -68,11 +68,11 @@ protocol nssymmetricamended(A,S,B) var kab: SessionKey; fresh nb: Nonce; - read_1(A,B, A ); + recv_1(A,B, A ); send_2(B,A, { A,nb }k(B,S) ); - read_5(A,B, { kab,A }k(B,S) ); + recv_5(A,B, { kab,A }k(B,S) ); send_6(B,A, { nb }kab ); - read_7(A,B, { {nb}succ }kab ); + recv_7(A,B, { {nb}succ }kab ); claim_9(B, Secret, kab); claim_9a(B, Niagree); diff --git a/protocols/misc/ns-symmetric.spdl b/protocols/misc/ns-symmetric.spdl index 22c2366..1288288 100644 --- a/protocols/misc/ns-symmetric.spdl +++ b/protocols/misc/ns-symmetric.spdl @@ -39,9 +39,9 @@ protocol nssymmetric(A,S,B) var nb: Nonce; send_1(A,S, A,B,na ); - read_2(S,A, { na,B,kab,T }k(A,S) ); + recv_2(S,A, { na,B,kab,T }k(A,S) ); send_3(A,B, T ); - read_4(B,A, { nb }kab ); + recv_4(B,A, { nb }kab ); send_5(A,B, { {nb}succ }kab ); claim_6(A, Secret, kab); @@ -52,7 +52,7 @@ protocol nssymmetric(A,S,B) fresh kab: SessionKey; var na: Nonce; - read_1(A,S, A,B,na ); + recv_1(A,S, A,B,na ); send_2(S,A, { na,B,kab, { kab,A }k(B,S) }k(A,S) ); } @@ -61,9 +61,9 @@ protocol nssymmetric(A,S,B) var kab: SessionKey; fresh nb: Nonce; - read_3(A,B, { kab,A }k(B,S) ); + recv_3(A,B, { kab,A }k(B,S) ); send_4(B,A, { nb }kab ); - read_5(A,B, { {nb}succ }kab ); + recv_5(A,B, { {nb}succ }kab ); claim_7(B, Secret, kab); } diff --git a/protocols/misc/ns3-brutus.spdl b/protocols/misc/ns3-brutus.spdl index 1fd51b0..33e4015 100644 --- a/protocols/misc/ns3-brutus.spdl +++ b/protocols/misc/ns3-brutus.spdl @@ -10,7 +10,7 @@ protocol ns3brutus(I,R) var nr: Nonce; send_1(I,R, {I,ni}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_4(I,Secret,nr); } @@ -20,9 +20,9 @@ protocol ns3brutus(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}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_5(R,Secret,ni); } } diff --git a/protocols/misc/ns3.spdl b/protocols/misc/ns3.spdl index d0017c0..69f01ba 100644 --- a/protocols/misc/ns3.spdl +++ b/protocols/misc/ns3.spdl @@ -18,7 +18,7 @@ protocol ns3(I,R) var nr: Nonce; send_1(I,R, {I,ni}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); claim_i2(I,Secret,nr); @@ -31,9 +31,9 @@ protocol ns3(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}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); claim_r3(R,Niagree); diff --git a/protocols/misc/nsl3-nisynch-rep.spdl b/protocols/misc/nsl3-nisynch-rep.spdl index 991bf13..f990b21 100644 --- a/protocols/misc/nsl3-nisynch-rep.spdl +++ b/protocols/misc/nsl3-nisynch-rep.spdl @@ -11,7 +11,7 @@ protocol nsl3rep(I,R) send_1(I,R, {I,ni}pk(R) ); send_6(I,R, {I,ni}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_4(I,Niagree); claim_7(I,Nisynch); @@ -22,10 +22,10 @@ protocol nsl3rep(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {I,ni}pk(R) ); - read_6(I,R, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}pk(R) ); + recv_6(I,R, {I,ni}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_5(R,Niagree); claim_8(R,Nisynch); } diff --git a/protocols/misc/nsl3.spdl b/protocols/misc/nsl3.spdl index 1028bf5..f19a98b 100644 --- a/protocols/misc/nsl3.spdl +++ b/protocols/misc/nsl3.spdl @@ -10,7 +10,7 @@ protocol nsl3(I,R) var nr: Nonce; send_1(I,R, {I,ni}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); @@ -24,9 +24,9 @@ protocol nsl3(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}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/protocols/misc/nst1.spdl b/protocols/misc/nst1.spdl index 85c21fb..0348319 100644 --- a/protocols/misc/nst1.spdl +++ b/protocols/misc/nst1.spdl @@ -28,7 +28,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); send_!chain(I,R, { R,Tb,Kir }k(I,S), T); @@ -49,9 +49,9 @@ protocol neustub(I,R,S) fresh g: Ticket; - read_1(I,R, I, Ni); + recv_1(I,R, I, Ni); send_!2(R,S, R, {I, Ni, Tb, g}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_R5(R,Secret, g); @@ -68,7 +68,7 @@ protocol neustub(I,R,S) var g: Ticket; - read_!2(R,S, R, {I,Ni,Tb, g}k(R,S), Nr); + recv_!2(R,S, R, {I,Ni,Tb, g}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/protocols/misc/nst2.spdl b/protocols/misc/nst2.spdl index 85b6cab..ee43fad 100644 --- a/protocols/misc/nst2.spdl +++ b/protocols/misc/nst2.spdl @@ -32,10 +32,10 @@ protocol neustub^Repeat(I,R,S) fresh g: Ticket; var h: Ticket; - read_!chain(R,I, { R,Tr,Kir }k(I,S), Tb); + recv_!chain(R,I, { R,Tr,Kir }k(I,S), Tb); send_5(I,R,Mi,{I,Kir,Tr}k(R,S),g); - read_6(R,I,{Mi,Mr,g,h}Kir); + recv_6(R,I,{Mi,Mr,g,h}Kir); send_7(I,R,{I,Mr}Kir); claim_I0(I,Secret, g); @@ -56,9 +56,9 @@ protocol neustub^Repeat(I,R,S) var g: Ticket; fresh h: Ticket; - read_5(I,R,Mi,{I,Kir,Tr}k(R,S),g); + recv_5(I,R,Mi,{I,Kir,Tr}k(R,S),g); send_6(R,I,{Mi,Mr,g,h}Kir); - read_7(I,R,{I,Mr}Kir); + recv_7(I,R,{I,Mr}Kir); claim_R1(R,Secret, Kir); claim_R5(R,Secret, g); diff --git a/protocols/misc/onetrace.spdl b/protocols/misc/onetrace.spdl index 026115d..b81aa0a 100644 --- a/protocols/misc/onetrace.spdl +++ b/protocols/misc/onetrace.spdl @@ -9,9 +9,9 @@ protocol onetrace(I) { var input: String; - read_!1(I,I, input); + recv_!1(I,I, input); send_!2(I,I, Hallo); - read_!3(I,I, input); + recv_!3(I,I, input); claim_4(I, Secret, input); } } diff --git a/protocols/misc/otwayrees.spdl b/protocols/misc/otwayrees.spdl index fea9d6d..cd7f947 100644 --- a/protocols/misc/otwayrees.spdl +++ b/protocols/misc/otwayrees.spdl @@ -15,7 +15,7 @@ protocol otwayrees(A,B,S) var kab : SesKey; send_1(A,B, M,A,B, { na,M,A,B }k(A,S) ); - read_4(B,A, M, { na,kab }k(A,S) ); + recv_4(B,A, M, { na,kab }k(A,S) ); claim_5(A, Secret,kab); claim_5b(A, Niagree); @@ -29,9 +29,9 @@ protocol otwayrees(A,B,S) var kab : SesKey; var t1,t2; - read_1(A,B, M,A,B, t1 ); + recv_1(A,B, M,A,B, t1 ); send_2(B,S, M,A,B, t1, { nb,M,A,B }k(B,S) ); - read_3(S,B, M, t2, { nb,kab }k(B,S) ); + recv_3(S,B, M, t2, { nb,kab }k(B,S) ); send_4(B,A, M, t2 ); claim_6(B, Secret,kab); @@ -45,7 +45,7 @@ protocol otwayrees(A,B,S) var M : String; fresh kab : SesKey; - read_2(B,S, M,A,B, { na,M,A,B }k(A,S), { nb,M,A,B }k(B,S) ); + recv_2(B,S, M,A,B, { na,M,A,B }k(A,S), { nb,M,A,B }k(B,S) ); send_3(S,B, M, { na,kab }k(A,S) , { nb,kab }k(B,S) ); } } diff --git a/protocols/misc/samasc-broken.spdl b/protocols/misc/samasc-broken.spdl index 765d190..13a0cbe 100644 --- a/protocols/misc/samasc-broken.spdl +++ b/protocols/misc/samasc-broken.spdl @@ -16,14 +16,14 @@ protocol samascbroken(I,R) fresh nr: Nonce; var kir: Key; - read_!1a (I,R, { kir,I }pk(R) ); + recv_!1a (I,R, { kir,I }pk(R) ); send_!1b (R,I, {nr,R}pk(I) ); /* Commenting out these two lines yields an attack: */ - read_!2a (I,R, { nr }kir ); + recv_!2a (I,R, { nr }kir ); send_!2b (R,I, { I,R,nr }kir ); - read_!3 (I,R, { I,R }kir ); + recv_!3 (I,R, { I,R }kir ); claim_4 (R, Secret, kir ); } diff --git a/protocols/misc/simplest.spdl b/protocols/misc/simplest.spdl index c800620..3866d93 100644 --- a/protocols/misc/simplest.spdl +++ b/protocols/misc/simplest.spdl @@ -8,7 +8,7 @@ protocol simplest(I) var x: Nonce; fresh n: Nonce; - read_!1(I,I, x); + recv_!1(I,I, x); send_!2(I,I, n, {n, x}k ); claim_3(I, Secret, n); } diff --git a/protocols/misc/soph-keyexch.spdl b/protocols/misc/soph-keyexch.spdl index 75ccaa1..efe1366 100644 --- a/protocols/misc/soph-keyexch.spdl +++ b/protocols/misc/soph-keyexch.spdl @@ -12,7 +12,7 @@ protocol sophkx(I,R) var nr: Nonce; send_1(I,R, ni, {I,kir}pk(R) ); - read_2(R,I, {ni}kir ); + recv_2(R,I, {ni}kir ); claim_4(I,Secret,kir); } @@ -22,7 +22,7 @@ protocol sophkx(I,R) var kir: Sessionkey; fresh nr: Nonce; - read_1(I,R, ni, {I,kir}pk(R) ); + recv_1(I,R, ni, {I,kir}pk(R) ); send_2(R,I, {ni}kir ); } } diff --git a/protocols/misc/soph.spdl b/protocols/misc/soph.spdl index 13f5946..f285049 100644 --- a/protocols/misc/soph.spdl +++ b/protocols/misc/soph.spdl @@ -9,7 +9,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); } @@ -17,7 +17,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/protocols/misc/speedtest.spdl b/protocols/misc/speedtest.spdl index 4a311fe..7fd6d21 100644 --- a/protocols/misc/speedtest.spdl +++ b/protocols/misc/speedtest.spdl @@ -10,7 +10,7 @@ protocol ns3speedtest(I,R) var nr: Nonce; send_1(I,R, {I,ni}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_4(I,Secret,nr); } @@ -20,9 +20,9 @@ protocol ns3speedtest(I,R) var ni: Nonce; fresh nr: Nonce; - read_1(I,R, {I,ni}pk(R) ); + recv_1(I,R, {I,ni}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_5(R,Secret,ni); } } diff --git a/protocols/misc/splice-as-hc-cj.spdl b/protocols/misc/splice-as-hc-cj.spdl index 635c35f..7b741e2 100644 --- a/protocols/misc/splice-as-hc-cj.spdl +++ b/protocols/misc/splice-as-hc-cj.spdl @@ -13,9 +13,9 @@ protocol spliceAShcCJ(C,AS,S) fresh L: LifeTime; send_1(C,AS, C, S, N1 ); - read_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); + recv_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); send_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) ); - read_6(S,C, S, C, {N2}pk(C) ); + recv_6(S,C, S, C, {N2}pk(C) ); claim_7(C, Secret, N2); claim_9(C, Niagree); @@ -26,9 +26,9 @@ protocol spliceAShcCJ(C,AS,S) { var N1,N3: Nonce; - read_1(C,AS, C, S, N1 ); + recv_1(C,AS, C, S, N1 ); send_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); - read_4(S,AS, S, C, N3 ); + recv_4(S,AS, S, C, N3 ); send_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) ); } @@ -42,9 +42,9 @@ protocol spliceAShcCJ(C,AS,S) var ni: Nonce; fresh nr: Nonce; - read_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) ); + recv_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) ); send_4(S,AS, S, C, N3 ); - read_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) ); + recv_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) ); send_6(S,C, S, C, {N2}pk(C) ); claim_8(S, Secret, N2); diff --git a/protocols/misc/splice-as-hc.spdl b/protocols/misc/splice-as-hc.spdl index ff773dc..18d736f 100644 --- a/protocols/misc/splice-as-hc.spdl +++ b/protocols/misc/splice-as-hc.spdl @@ -13,9 +13,9 @@ protocol spliceAShc(C,AS,S) fresh L: LifeTime; send_1(C,AS, C, S, N1 ); - read_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); + recv_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); send_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); - read_6(S,C, S, C, {S, N2}pk(C) ); + recv_6(S,C, S, C, {S, N2}pk(C) ); claim_7(C, Secret, N2); claim_9(C, Niagree); @@ -26,9 +26,9 @@ protocol spliceAShc(C,AS,S) { var N1,N3: Nonce; - read_1(C,AS, C, S, N1 ); + recv_1(C,AS, C, S, N1 ); send_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); - read_4(S,AS, S, C, N3 ); + recv_4(S,AS, S, C, N3 ); send_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) ); } @@ -42,9 +42,9 @@ protocol spliceAShc(C,AS,S) var ni: Nonce; fresh nr: Nonce; - read_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); + recv_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); send_4(S,AS, S, C, N3 ); - read_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) ); + recv_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) ); send_6(S,C, S, C, {S, N2}pk(C) ); claim_8(S, Secret, N2); diff --git a/protocols/misc/splice-as.spdl b/protocols/misc/splice-as.spdl index abaca41..c205c3c 100644 --- a/protocols/misc/splice-as.spdl +++ b/protocols/misc/splice-as.spdl @@ -13,9 +13,9 @@ protocol spliceAS(C,AS,S) fresh L: LifeTime; send_1(C,AS, C, S, N1 ); - read_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) ); + recv_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) ); send_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); - read_6(S,C, S, C, {S, N2}pk(C) ); + recv_6(S,C, S, C, {S, N2}pk(C) ); claim_7(C, Secret, N2); claim_9(C, Niagree); @@ -26,9 +26,9 @@ protocol spliceAS(C,AS,S) { var N1,N3: Nonce; - read_1(C,AS, C, S, N1 ); + recv_1(C,AS, C, S, N1 ); send_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) ); - read_4(S,AS, S, C, N3 ); + recv_4(S,AS, S, C, N3 ); send_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) ); } @@ -42,9 +42,9 @@ protocol spliceAS(C,AS,S) var ni: Nonce; fresh nr: Nonce; - read_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); + recv_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); send_4(S,AS, S, C, N3 ); - read_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) ); + recv_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) ); send_6(S,C, S, C, {S, N2}pk(C) ); claim_8(S, Secret, N2); diff --git a/protocols/misc/tls/tls-BM-1.m4 b/protocols/misc/tls/tls-BM-1.m4 index bc48e10..a1102b7 100644 --- a/protocols/misc/tls/tls-BM-1.m4 +++ b/protocols/misc/tls/tls-BM-1.m4 @@ -35,9 +35,9 @@ protocol tls-bm-1(A,B) var nb: Nonce; send_1( A,B, msg1 ); - read_2( B,A, msg2 ); + recv_2( B,A, msg2 ); send_3( A,B, msg3 ); - read_4( B,A, msg4 ); + recv_4( B,A, msg4 ); claim_A1( A, Secret, kab ); claim_A2( A, Nisynch ); @@ -49,9 +49,9 @@ protocol tls-bm-1(A,B) var pmk: Nonce; fresh nb: Nonce; - read_1( A,B, msg1 ); + recv_1( A,B, msg1 ); send_2( B,A, msg2 ); - read_3( A,B, msg3 ); + recv_3( A,B, msg3 ); send_4( B,A, msg4 ); claim_B1( B, Secret, kab ); diff --git a/protocols/misc/tls/tls-BM-1.spdl b/protocols/misc/tls/tls-BM-1.spdl index 1adf816..66dfe88 100644 --- a/protocols/misc/tls/tls-BM-1.spdl +++ b/protocols/misc/tls/tls-BM-1.spdl @@ -35,9 +35,9 @@ protocol tls-bm-1(A,B) var nb: Nonce; send_1( A,B, na ); - read_2( B,A, nb ); + recv_2( B,A, nb ); send_3( A,B, { pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) ); - read_4( B,A, { na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) }hash(pmk,na,nb) ); + recv_4( B,A, { na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) }hash(pmk,na,nb) ); claim_A1( A, Secret, hash(pmk,na,nb) ); claim_A2( A, Nisynch ); @@ -49,9 +49,9 @@ protocol tls-bm-1(A,B) var pmk: Nonce; fresh nb: Nonce; - read_1( A,B, na ); + recv_1( A,B, na ); send_2( B,A, nb ); - read_3( A,B, { pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) ); + recv_3( A,B, { pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) ); send_4( B,A, { na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) }hash(pmk,na,nb) ); claim_B1( B, Secret, hash(pmk,na,nb) ); diff --git a/protocols/misc/tls/tls-HSDDM05-2.cpp b/protocols/misc/tls/tls-HSDDM05-2.cpp index fa40d5f..d4ee124 100644 --- a/protocols/misc/tls/tls-HSDDM05-2.cpp +++ b/protocols/misc/tls/tls-HSDDM05-2.cpp @@ -54,9 +54,9 @@ protocol tls-HSDDM05(X,Y) var pb: Params; send_1( X,Y, msg1 ); - read_2( Y,X, msg2 ); + recv_2( Y,X, msg2 ); send_3( X,Y, msg3 ); - read_4( Y,X, msg4 ); + recv_4( Y,X, msg4 ); claim_X1( X, Secret, msecret ); } @@ -69,9 +69,9 @@ protocol tls-HSDDM05(X,Y) fresh Ny: Nonce; fresh pb: Params; - read_1( X,Y, msg1 ); + recv_1( X,Y, msg1 ); send_2( Y,X, msg2 ); - read_3( X,Y, msg3 ); + recv_3( X,Y, msg3 ); send_4( Y,X, msg4 ); claim_Y1( Y, Secret, msecret ); diff --git a/protocols/misc/tls/tls-HSDDM05-2.spdl b/protocols/misc/tls/tls-HSDDM05-2.spdl index 8ed52cc..95de3b8 100644 --- a/protocols/misc/tls/tls-HSDDM05-2.spdl +++ b/protocols/misc/tls/tls-HSDDM05-2.spdl @@ -26,9 +26,9 @@ protocol tls-HSDDM05(X,Y) var pb: Params; send_1( X,Y, X,Nx,pa ); - read_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); + recv_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); send_3( X,Y, { X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) ); - read_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring)),serverstring) ); + recv_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring)),serverstring) ); claim_X1( X, Secret, msecret ); } @@ -41,9 +41,9 @@ protocol tls-HSDDM05(X,Y) fresh Ny: Nonce; fresh pb: Params; - read_1( X,Y, X,Nx,pa ); + recv_1( X,Y, X,Nx,pa ); send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); - read_3( X,Y, { X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) ); + recv_3( X,Y, { X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring) ); send_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret)}sk(X),{msecret}pk(Y),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),msecret),clientstring)),serverstring) ); claim_Y1( Y, Secret, msecret ); diff --git a/protocols/misc/tls/tls-HSDDM05-fix.cpp b/protocols/misc/tls/tls-HSDDM05-fix.cpp index 82cbc0a..5ce8e79 100644 --- a/protocols/misc/tls/tls-HSDDM05-fix.cpp +++ b/protocols/misc/tls/tls-HSDDM05-fix.cpp @@ -44,9 +44,9 @@ protocol tls-HSDDM05(X,Y) var pb: Params; send_1( X,Y, msg1 ); - read_2( Y,X, msg2 ); + recv_2( Y,X, msg2 ); send_3( X,Y, msg3 ); - read_4( Y,X, msg4 ); + recv_4( Y,X, msg4 ); claim_X1( X, Secret, msecret ); } @@ -59,9 +59,9 @@ protocol tls-HSDDM05(X,Y) fresh Ny: Nonce; fresh pb: Params; - read_1( X,Y, msg1 ); + recv_1( X,Y, msg1 ); send_2( Y,X, msg2 ); - read_3( X,Y, msg3 ); + recv_3( X,Y, msg3 ); send_4( Y,X, msg4 ); claim_Y1( Y, Secret, msecret ); diff --git a/protocols/misc/tls/tls-HSDDM05-fix.m4 b/protocols/misc/tls/tls-HSDDM05-fix.m4 index 9abe9c7..4710815 100644 --- a/protocols/misc/tls/tls-HSDDM05-fix.m4 +++ b/protocols/misc/tls/tls-HSDDM05-fix.m4 @@ -45,9 +45,9 @@ protocol tls-HSDDM05(X,Y) var pb: Params; send_1( X,Y, msg1 ); - read_2( Y,X, msg2 ); + recv_2( Y,X, msg2 ); send_3( X,Y, msg3 ); - read_4( Y,X, msg4 ); + recv_4( Y,X, msg4 ); claim_X1( X, Secret, msecret ); } @@ -60,9 +60,9 @@ protocol tls-HSDDM05(X,Y) fresh Ny: Nonce; fresh pb: Params; - read_1( X,Y, msg1 ); + recv_1( X,Y, msg1 ); send_2( Y,X, msg2 ); - read_3( X,Y, msg3 ); + recv_3( X,Y, msg3 ); send_4( Y,X, msg4 ); claim_Y1( Y, Secret, msecret ); diff --git a/protocols/misc/tls/tls-HSDDM05-fix.spdl b/protocols/misc/tls/tls-HSDDM05-fix.spdl index c3820fc..5ac52da 100644 --- a/protocols/misc/tls/tls-HSDDM05-fix.spdl +++ b/protocols/misc/tls/tls-HSDDM05-fix.spdl @@ -45,9 +45,9 @@ protocol tls-HSDDM05(X,Y) var pb: Params; send_1( X,Y, X,Nx,pa ); - read_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); + recv_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); send_3( X,Y, { X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring) ); - read_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring)),serverstring) ); + recv_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring)),serverstring) ); claim_X1( X, Secret, msecret ); } @@ -60,9 +60,9 @@ protocol tls-HSDDM05(X,Y) fresh Ny: Nonce; fresh pb: Params; - read_1( X,Y, X,Nx,pa ); + recv_1( X,Y, X,Nx,pa ); send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); - read_3( X,Y, { X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring) ); + recv_3( X,Y, { X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring) ); send_4( Y,X, hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{msecret}pk(Y),{hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y))}sk(X),hash(msecret,hash(X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{msecret}pk(Y)),clientstring)),serverstring) ); claim_Y1( Y, Secret, msecret ); diff --git a/protocols/misc/tls/tls-HSDDM05.cpp b/protocols/misc/tls/tls-HSDDM05.cpp index 182f171..4f3274a 100644 --- a/protocols/misc/tls/tls-HSDDM05.cpp +++ b/protocols/misc/tls/tls-HSDDM05.cpp @@ -48,9 +48,9 @@ protocol tls-HSDDM05(X,Y) var pb: Params; send_1( X,Y, msg1 ); - read_2( Y,X, msg2 ); + recv_2( Y,X, msg2 ); send_3( X,Y, msg3 ); - read_4( Y,X, msg4 ); + recv_4( Y,X, msg4 ); claim_X1( X, Secret, msecret ); } @@ -63,9 +63,9 @@ protocol tls-HSDDM05(X,Y) fresh Ny: Nonce; fresh pb: Params; - read_1( X,Y, msg1 ); + recv_1( X,Y, msg1 ); send_2( Y,X, msg2 ); - read_3( X,Y, msg3 ); + recv_3( X,Y, msg3 ); send_4( Y,X, msg4 ); claim_Y1( Y, Secret, msecret ); diff --git a/protocols/misc/tls/tls-HSDDM05.spdl b/protocols/misc/tls/tls-HSDDM05.spdl index cb9b1e9..1abe0f5 100644 --- a/protocols/misc/tls/tls-HSDDM05.spdl +++ b/protocols/misc/tls/tls-HSDDM05.spdl @@ -26,9 +26,9 @@ protocol tls-HSDDM05(X,Y) var pb: Params; send_1( X,Y, X,Nx,pa ); - read_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); + recv_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); send_3( X,Y, { X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring) ); - read_4( Y,X, hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring),serverstring) ); + recv_4( Y,X, hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring),serverstring) ); claim_X1( X, Secret, msecret ); } @@ -41,9 +41,9 @@ protocol tls-HSDDM05(X,Y) fresh Ny: Nonce; fresh pb: Params; - read_1( X,Y, X,Nx,pa ); + recv_1( X,Y, X,Nx,pa ); send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); - read_3( X,Y, { X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring) ); + recv_3( X,Y, { X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring) ); send_4( Y,X, hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence)}sk(X),{msecret}pk(Y),hash(msecret,X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),clientstring),serverstring) ); claim_Y1( Y, Secret, msecret ); diff --git a/protocols/misc/tls/tls-paulson-avispa.cpp b/protocols/misc/tls/tls-paulson-avispa.cpp index aef2211..2c1a42c 100644 --- a/protocols/misc/tls/tls-paulson-avispa.cpp +++ b/protocols/misc/tls/tls-paulson-avispa.cpp @@ -48,13 +48,13 @@ protocol tlspaulson-avispa(a,b) var pb: Params; send_1( a,b, a,na,sid,pa ); - read_2( b,a, nb,sid,pb ); - read_3( b,a, CERT(b) ); + recv_2( b,a, nb,sid,pb ); + recv_3( b,a, CERT(b) ); send_4( a,b, CERT(a) ); send_5( a,b, { pms }pk(b) ); send_6( a,b, { hash(nb,b,pms) }sk(a) ); send_7( a,b, { F }CLIENTK ); - read_8( b,a, { F }SERVERK ); + recv_8( b,a, { F }SERVERK ); claim_9a(a, Secret, SERVERK); claim_9b(a, Secret, CLIENTK); @@ -70,13 +70,13 @@ protocol tlspaulson-avispa(a,b) fresh nb: Nonce; fresh pb: Params; - read_1( a,b, a,na,sid,pa ); + recv_1( a,b, a,na,sid,pa ); send_2( b,a, nb,sid,pb ); send_3( b,a, CERT(b) ); - read_4( a,b, CERT(a) ); - read_5( a,b, { pms }pk(b) ); - read_6( a,b, { hash(nb,b,pms) }sk(a) ); - read_7( a,b, { F }CLIENTK ); + recv_4( a,b, CERT(a) ); + recv_5( a,b, { pms }pk(b) ); + recv_6( a,b, { hash(nb,b,pms) }sk(a) ); + recv_7( a,b, { F }CLIENTK ); send_8( b,a, { F }SERVERK ); claim_10a(b, Secret, SERVERK); diff --git a/protocols/misc/tls/tls-paulson-avispa.spdl b/protocols/misc/tls/tls-paulson-avispa.spdl index 9f67636..21c297e 100644 --- a/protocols/misc/tls/tls-paulson-avispa.spdl +++ b/protocols/misc/tls/tls-paulson-avispa.spdl @@ -29,13 +29,13 @@ protocol tlspaulson-avispa(a,b) var pb: Params; send_1( a,b, a,na,sid,pa ); - read_2( b,a, nb,sid,pb ); - read_3( b,a, { b,pk(b) }sk(Terence) ); + recv_2( b,a, nb,sid,pb ); + recv_3( b,a, { b,pk(b) }sk(Terence) ); send_4( a,b, { a,pk(a) }sk(Terence) ); send_5( a,b, { pms }pk(b) ); send_6( a,b, { hash(nb,b,pms) }sk(a) ); send_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(a,na,nb,hash(pms,na,nb)) ); - read_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(b,na,nb,hash(pms,na,nb)) ); + recv_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(b,na,nb,hash(pms,na,nb)) ); claim_9a(a, Secret, keygen(b,na,nb,hash(pms,na,nb))); claim_9b(a, Secret, keygen(a,na,nb,hash(pms,na,nb))); @@ -51,13 +51,13 @@ protocol tlspaulson-avispa(a,b) fresh nb: Nonce; fresh pb: Params; - read_1( a,b, a,na,sid,pa ); + recv_1( a,b, a,na,sid,pa ); send_2( b,a, nb,sid,pb ); send_3( b,a, { b,pk(b) }sk(Terence) ); - read_4( a,b, { a,pk(a) }sk(Terence) ); - read_5( a,b, { pms }pk(b) ); - read_6( a,b, { hash(nb,b,pms) }sk(a) ); - read_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(a,na,nb,hash(pms,na,nb)) ); + recv_4( a,b, { a,pk(a) }sk(Terence) ); + recv_5( a,b, { pms }pk(b) ); + recv_6( a,b, { hash(nb,b,pms) }sk(a) ); + recv_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(a,na,nb,hash(pms,na,nb)) ); send_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(b,na,nb,hash(pms,na,nb)) ); claim_10a(b, Secret, keygen(b,na,nb,hash(pms,na,nb))); diff --git a/protocols/misc/tls/tls-paulson.cpp b/protocols/misc/tls/tls-paulson.cpp index 7147024..880e269 100644 --- a/protocols/misc/tls/tls-paulson.cpp +++ b/protocols/misc/tls/tls-paulson.cpp @@ -40,13 +40,13 @@ protocol tlspaulson(a,b) var pb: Params; send_1( a,b, a,na,sid,pa ); - read_2( b,a, nb,sid,pb ); - read_3( b,a, CERT(b) ); + recv_2( b,a, nb,sid,pb ); + recv_3( b,a, CERT(b) ); send_4( a,b, CERT(a) ); send_5( a,b, { pms }pk(b) ); send_6( a,b, { hash(nb,b,pms) }sk(a) ); send_7( a,b, { F }CLIENTK ); - read_8( b,a, { F }SERVERK ); + recv_8( b,a, { F }SERVERK ); claim_9a(a, Secret, SERVERK); claim_9b(a, Secret, CLIENTK); @@ -61,13 +61,13 @@ protocol tlspaulson(a,b) fresh nb: Nonce; fresh pb: Params; - read_1( a,b, a,na,sid,pa ); + recv_1( a,b, a,na,sid,pa ); send_2( b,a, nb,sid,pb ); send_3( b,a, CERT(b) ); - read_4( a,b, CERT(a) ); - read_5( a,b, { pms }pk(b) ); - read_6( a,b, { hash(nb,b,pms) }sk(a) ); - read_7( a,b, { F }CLIENTK ); + recv_4( a,b, CERT(a) ); + recv_5( a,b, { pms }pk(b) ); + recv_6( a,b, { hash(nb,b,pms) }sk(a) ); + recv_7( a,b, { F }CLIENTK ); send_8( b,a, { F }SERVERK ); claim_10a(b, Secret, SERVERK); diff --git a/protocols/misc/tls/tls-paulson.spdl b/protocols/misc/tls/tls-paulson.spdl index c385cd3..3b0523a 100644 --- a/protocols/misc/tls/tls-paulson.spdl +++ b/protocols/misc/tls/tls-paulson.spdl @@ -25,13 +25,13 @@ protocol tlspaulson(a,b) var pb: Params; send_1( a,b, a,na,sid,pa ); - read_2( b,a, nb,sid,pb ); - read_3( b,a, { b,pk(b) }sk(Terence) ); + recv_2( b,a, nb,sid,pb ); + recv_3( b,a, { b,pk(b) }sk(Terence) ); send_4( a,b, { a,pk(a) }sk(Terence) ); send_5( a,b, { pms }pk(b) ); send_6( a,b, { hash(nb,b,pms) }sk(a) ); send_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) ); - read_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) ); + recv_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) ); claim_9a(a, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true)); claim_9b(a, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false)); @@ -46,13 +46,13 @@ protocol tlspaulson(a,b) fresh nb: Nonce; fresh pb: Params; - read_1( a,b, a,na,sid,pa ); + recv_1( a,b, a,na,sid,pa ); send_2( b,a, nb,sid,pb ); send_3( b,a, { b,pk(b) }sk(Terence) ); - read_4( a,b, { a,pk(a) }sk(Terence) ); - read_5( a,b, { pms }pk(b) ); - read_6( a,b, { hash(nb,b,pms) }sk(a) ); - read_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) ); + recv_4( a,b, { a,pk(a) }sk(Terence) ); + recv_5( a,b, { pms }pk(b) ); + recv_6( a,b, { hash(nb,b,pms) }sk(a) ); + recv_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) ); send_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) ); claim_10a(b, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true)); diff --git a/protocols/misc/tmn-Gijs.spdl b/protocols/misc/tmn-Gijs.spdl index 55893cf..9ee2b75 100644 --- a/protocols/misc/tmn-Gijs.spdl +++ b/protocols/misc/tmn-Gijs.spdl @@ -13,7 +13,7 @@ protocol tmn(A,B,S) var Kb: Key; send_1(A,S, B,{Ka}pk(S) ); - read_4(S,A, B,{Kb}Ka ); + recv_4(S,A, B,{Kb}Ka ); #claim_5(A,Secret,Ka); #claim_8(A,Secret,Kb); @@ -23,7 +23,7 @@ protocol tmn(A,B,S) { fresh Kb: Key; - read_2(S,B, A ); + recv_2(S,B, A ); send_3(B,S, A, { Kb }pk(S) ); claim_6(B,Secret,Kb); @@ -33,9 +33,9 @@ protocol tmn(A,B,S) { var Ka,Kb: Key; - read_1(A,S, B,{Ka}pk(S) ); + recv_1(A,S, B,{Ka}pk(S) ); send_2(S,B, A ); - read_3(B,S, A, { Kb }pk(S) ); + recv_3(B,S, A, { Kb }pk(S) ); send_4(S,A, B,{Kb}Ka ); #claim_7(S,Secret,Ka); diff --git a/protocols/misc/tmn.spdl b/protocols/misc/tmn.spdl index d1baab3..e52723a 100644 --- a/protocols/misc/tmn.spdl +++ b/protocols/misc/tmn.spdl @@ -12,7 +12,7 @@ protocol tmn(A,B,S) var Kb: Key; send_1(A,S, B,{Ka}pk(S) ); - read_4(S,A, B,{Kb}Ka ); + recv_4(S,A, B,{Kb}Ka ); claim_5(A,Secret,Ka); claim_8(A,Secret,Kb); @@ -22,7 +22,7 @@ protocol tmn(A,B,S) { fresh Kb: Key; - read_2(S,B, A ); + recv_2(S,B, A ); send_3(B,S, A, { Kb }pk(S) ); claim_6(B,Secret,Kb); @@ -32,9 +32,9 @@ protocol tmn(A,B,S) { var Ka,Kb: Key; - read_1(A,S, B,{Ka}pk(S) ); + recv_1(A,S, B,{Ka}pk(S) ); send_2(S,B, A ); - read_3(B,S, A, { Kb }pk(S) ); + recv_3(B,S, A, { Kb }pk(S) ); send_4(S,A, B,{Kb}Ka ); claim_7(S,Secret,Ka); diff --git a/protocols/misc/unknown2.spdl b/protocols/misc/unknown2.spdl index 1ce13fb..39de355 100644 --- a/protocols/misc/unknown2.spdl +++ b/protocols/misc/unknown2.spdl @@ -11,7 +11,7 @@ protocol unknown2(I,R,S) var T; send_1(I,R, ni ); - read_3(S,I, { I,R,kir,ni,nr }k(I,S), T ); + recv_3(S,I, { I,R,kir,ni,nr }k(I,S), T ); send_4(I,R, T, {nr}kir ); claim_i1(I,Nisynch); @@ -25,9 +25,9 @@ protocol unknown2(I,R,S) var ni: Nonce; var kir: SessionKey; - read_1(I,R, ni ); + recv_1(I,R, ni ); send_2(R,S, { I,R,ni,nr }k(R,S) ); - read_4(I,R, { I,R,kir,ni,nr }k(R,S), {nr}kir ); + recv_4(I,R, { I,R,kir,ni,nr }k(R,S), {nr}kir ); claim_r1(R,Nisynch); claim_r2(R,Niagree); @@ -39,7 +39,7 @@ protocol unknown2(I,R,S) fresh kir: SessionKey; var ni,nr: Nonce; - read_2(R,S, { I,R,ni,nr }k(R,S) ); + recv_2(R,S, { I,R,ni,nr }k(R,S) ); send_3(S,I, { I,R,kir,ni,nr }k(I,S), { I,R,kir,ni,nr }k(R,S) ); /* diff --git a/protocols/misc/wmf-brutus.spdl b/protocols/misc/wmf-brutus.spdl index 08335db..b70086f 100644 --- a/protocols/misc/wmf-brutus.spdl +++ b/protocols/misc/wmf-brutus.spdl @@ -17,7 +17,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); } @@ -26,7 +26,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/protocols/misc/woolam-cmv.spdl b/protocols/misc/woolam-cmv.spdl index f101e8d..2beb420 100644 --- a/protocols/misc/woolam-cmv.spdl +++ b/protocols/misc/woolam-cmv.spdl @@ -24,9 +24,9 @@ protocol woolamcmv(A,B,S) var t1,t2; send_1(A,B, A,Na); - read_2(B,A, B,Nb); + recv_2(B,A, B,Nb); send_3(A,B, { A,B, Na,Nb }k(A,S) ); - read_6(B,A, { B,Na,Nb,Kab }k(A,S), { Na,Nb }Kab ); + recv_6(B,A, { B,Na,Nb,Kab }k(A,S), { Na,Nb }Kab ); send_7(A,B, { Nb }Kab ); claim_8(A,Secret, Kab); @@ -41,13 +41,13 @@ protocol woolamcmv(A,B,S) var Kab: SessionKey; var t1,t2; - read_1(A,B, A,Na); + recv_1(A,B, A,Na); send_2(B,A, B,Nb); - read_3(A,B, t1 ); + recv_3(A,B, t1 ); send_4(B,S, t1, { A,B,Na,Nb }k(B,S) ); - read_5(S,B, t2, { A,Na,Nb,Kab }k(B,S) ); + recv_5(S,B, t2, { A,Na,Nb,Kab }k(B,S) ); send_6(B,A, t2, { Na,Nb }Kab ); - read_7(A,B, { Nb }Kab ); + recv_7(A,B, { Nb }Kab ); claim_11(B,Secret, Kab); claim_12(B,Niagree); @@ -59,7 +59,7 @@ protocol woolamcmv(A,B,S) var Na, Nb: Nonce; fresh Kab: SessionKey; - read_4(B,S, { A,B, Na,Nb }k(A,S), { A,B,Na,Nb }k(B,S) ); + recv_4(B,S, { A,B, Na,Nb }k(A,S), { A,B,Na,Nb }k(B,S) ); send_5(S,B, { B,Na,Nb,Kab }k(A,S), { A,Na,Nb,Kab }k(B,S) ); claim_14(S,Secret, Kab); diff --git a/protocols/misc/woolam-pi-f.spdl b/protocols/misc/woolam-pi-f.spdl index ab2d8fb..b11ddee 100644 --- a/protocols/misc/woolam-pi-f.spdl +++ b/protocols/misc/woolam-pi-f.spdl @@ -18,7 +18,7 @@ protocol woolampif(A,B,S) var Nb: Nonce; send_1(A,B, A); - read_2(B,A, Nb); + recv_2(B,A, Nb); send_3(A,B, { A,B,Nb }k(A,S) ); } @@ -27,11 +27,11 @@ protocol woolampif(A,B,S) fresh Nb: Nonce; var T: Ticket; - read_1(A,B, A); + recv_1(A,B, A); send_2(B,A, Nb); - read_3(A,B, T); + recv_3(A,B, T); send_4(B,S, { A,B,Nb, T }k(B,S) ); - read_5(S,B, { A,B,Nb }k(B,S) ); + recv_5(S,B, { A,B,Nb }k(B,S) ); claim_6(B,Niagree); claim_7(B,Nisynch); @@ -41,7 +41,7 @@ protocol woolampif(A,B,S) { var Nb: Nonce; - read_4(B,S, { A,B,Nb, { A,B,Nb }k(A,S) }k(B,S) ); + recv_4(B,S, { A,B,Nb, { A,B,Nb }k(A,S) }k(B,S) ); send_5(S,B, { A,B,Nb }k(B,S) ); } } diff --git a/protocols/misc/yahalom-ban.spdl b/protocols/misc/yahalom-ban.spdl index 90bf4fd..9f88aa7 100644 --- a/protocols/misc/yahalom-ban.spdl +++ b/protocols/misc/yahalom-ban.spdl @@ -21,7 +21,7 @@ protocol yahalomBan(A,B,S) var kab; 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); } @@ -33,9 +33,9 @@ protocol yahalomBan(A,B,S) var ticket; var kab; - 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,kab,nb}k(B,S) , {nb}kab ); + recv_4(A,B, {A,kab,nb}k(B,S) , {nb}kab ); claim_6(B, Secret,kab); } @@ -44,7 +44,7 @@ protocol yahalomBan(A,B,S) fresh kab; var na,nb; - 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,kab,nb}k(B,S) ); } } diff --git a/protocols/misc/yahalom-lowe.spdl b/protocols/misc/yahalom-lowe.spdl index d4660a5..d7bf5c1 100644 --- a/protocols/misc/yahalom-lowe.spdl +++ b/protocols/misc/yahalom-lowe.spdl @@ -18,7 +18,7 @@ protocol yahalomlowe(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_8(I, Secret,kir); @@ -32,10 +32,10 @@ protocol yahalomlowe(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_11(R, Secret,kir); claim_12(R, Nisynch); claim_13(R, Niagree); @@ -46,7 +46,7 @@ protocol yahalomlowe(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/protocols/misc/yahalom-paulson.spdl b/protocols/misc/yahalom-paulson.spdl index f10fcc6..a73558d 100644 --- a/protocols/misc/yahalom-paulson.spdl +++ b/protocols/misc/yahalom-paulson.spdl @@ -19,7 +19,7 @@ protocol yahalompaulson(I,R,S) var T: Ticket; 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_8(I, Secret,kir); @@ -33,9 +33,9 @@ protocol yahalompaulson(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, 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_11(R, Secret,kir); claim_12(R, Nisynch); @@ -47,7 +47,7 @@ protocol yahalompaulson(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) ); } }