Fixing remaining 'read's to 'recv'.
This commit is contained in:
parent
727e813c77
commit
b81db8e9b7
@ -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);
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
|
@ -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 );
|
||||
|
||||
}
|
||||
|
@ -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 );
|
||||
}
|
||||
}
|
||||
|
@ -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 );
|
||||
}
|
||||
}
|
||||
|
@ -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 );
|
||||
|
@ -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 );
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -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);
|
||||
|
@ -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 );
|
||||
}
|
||||
}
|
||||
|
@ -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 );
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
|
@ -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)
|
||||
# );
|
||||
#
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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 );
|
||||
|
@ -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 ) );
|
||||
|
@ -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 );
|
||||
}
|
||||
}
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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) );
|
||||
|
||||
|
@ -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
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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 );
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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 );
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
|
@ -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 );
|
||||
}
|
||||
}
|
||||
|
@ -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 );
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
|
@ -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 );
|
||||
|
@ -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) );
|
||||
|
@ -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 );
|
||||
|
@ -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 );
|
||||
|
@ -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 );
|
||||
|
@ -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 );
|
||||
|
@ -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 );
|
||||
|
@ -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 );
|
||||
|
@ -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 );
|
||||
|
@ -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);
|
||||
|
@ -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)));
|
||||
|
@ -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);
|
||||
|
@ -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));
|
||||
|
@ -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);
|
||||
|
@ -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);
|
||||
|
@ -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) );
|
||||
|
||||
/*
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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);
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
@ -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) );
|
||||
}
|
||||
|
@ -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) );
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user