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

- Unfolded secrecy claims.

Browse Source
This commit is contained in:
ccremers 2005-02-19 14:25:30 +00:00
parent e36392b1d2
commit 49d314d0f5
8 changed files with 40 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
spdl/bkepk.spdl
View File

@ -23,7 +23,8 @@ protocol bkepk(A,B)
send_1 (B,A, B,{ nb,B }pk(A) ); send_1 (B,A, B,{ nb,B }pk(A) );
read_2 (A,B, { hash(nb),na,A,kab }pk(B) ); read_2 (A,B, { hash(nb),na,A,kab }pk(B) );
send_3 (B,A, { hash(na) }kab ); send_3 (B,A, { hash(na) }kab );
claim_4 (B, Secret, na,nb ); claim_4 (B, Secret, na );
claim_5 (B, Secret, nb );
} }
role A role A
@ -35,7 +36,8 @@ protocol bkepk(A,B)
read_1 (B,A, B,{ nb,B }pk(A) ); read_1 (B,A, B,{ nb,B }pk(A) );
send_2 (A,B, { hash(nb),na,A,kab }pk(B) ); send_2 (A,B, { hash(nb),na,A,kab }pk(B) );
read_3 (B,A, { hash(na) }kab ); read_3 (B,A, { hash(na) }kab );
claim_5 (A, Secret, na,nb ); claim_6 (A, Secret, na );
claim_7 (A, Secret, nb );
} }
} }

10
spdl/ccitt509-ban.spdl
View File

@ -16,8 +16,9 @@ protocol ccitt509(I,R)
read_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) ); read_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) );
send_3(I,R, I,{R,nr}sk(I) ); send_3(I,R, I,{R,nr}sk(I) );
claim_4(I,Secret,yi,yr); claim_4(I,Secret,yi);
claim_5(I,Nisynch); claim_5(I,Secret,yr);
claim_6(I,Nisynch);
} }
role R role R
@ -31,8 +32,9 @@ protocol ccitt509(I,R)
send_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) ); send_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) );
read_3(I,R, I,{R,nr}sk(I) ); read_3(I,R, I,{R,nr}sk(I) );
claim_7(R,Secret,yi,yr); claim_7(R,Secret,yi);
claim_8(R,Nisynch); claim_8(R,Secret,yr);
claim_9(R,Nisynch);
} }
} }

8
spdl/gong-nonce-b.spdl
View File

@ -23,7 +23,8 @@ protocol gongnonceb(I,R,S)
read_4 (S,I, { S,I,R,kr,I }k(I,S), { R,I,ni }f(ki,kr), nr ); read_4 (S,I, { S,I,R,kr,I }k(I,S), { R,I,ni }f(ki,kr), nr );
send_5 (I,R, { I,R,nr }f(ki,kr) ); send_5 (I,R, { I,R,nr }f(ki,kr) );
claim_6 (I, Secret, ki,kr); claim_6 (I, Secret, ki);
claim_7 (I, Secret, kr);
claim_8 (I, Nisynch); claim_8 (I, Nisynch);
} }
@ -38,8 +39,9 @@ protocol gongnonceb(I,R,S)
send_3 (R,S, { R,S,R,kr,I }k(R,S), { R,I, ni }f(ki,kr), nr ); send_3 (R,S, { R,S,R,kr,I }k(R,S), { R,I, ni }f(ki,kr), nr );
read_5 (I,R, { I,R,nr }f(ki,kr) ); read_5 (I,R, { I,R,nr }f(ki,kr) );
claim_7 (R, Secret, ki,kr); claim_9 (R, Secret, ki);
claim_9 (R, Nisynch); claim_10 (R, Secret, kr);
claim_11 (R, Nisynch);
} }
role S role S

8
spdl/gong-nonce.spdl
View File

@ -15,7 +15,8 @@ protocol gongnonce(I,R,S)
read_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr); read_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr);
send_4 (I,S, { I,S,I, ki, R, nr }k(I,S) ); send_4 (I,S, { I,S,I, ki, R, nr }k(I,S) );
claim_6 (I, Secret, ki,kr); claim_6 (I, Secret, ki);
claim_7 (I, Secret, kr);
claim_8 (I, Nisynch); claim_8 (I, Nisynch);
} }
@ -30,8 +31,9 @@ protocol gongnonce(I,R,S)
send_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S)); send_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S));
read_5 (S,R, { S,R,I, ki, R, nr }k(R,S) ); read_5 (S,R, { S,R,I, ki, R, nr }k(R,S) );
claim_7 (R, Secret, ki,kr); claim_9 (R, Secret, ki);
claim_9 (R, Nisynch); claim_10 (R, Secret, kr);
claim_11 (R, Nisynch);
} }
role S role S

14
spdl/ns3.spdl
View File

@ -12,9 +12,10 @@ protocol ns3(I,R)
send_1(I,R, {I,ni}pk(R) ); send_1(I,R, {I,ni}pk(R) );
read_2(R,I, {ni,nr}pk(I) ); read_2(R,I, {ni,nr}pk(I) );
send_3(I,R, {nr}pk(R) ); send_3(I,R, {nr}pk(R) );
claim_i1(I,Secret,ni,nr); claim_i1(I,Secret,ni);
claim_i2(I,Niagree); claim_i2(I,Secret,nr);
claim_i3(I,Nisynch); claim_i3(I,Niagree);
claim_i4(I,Nisynch);
} }
role R role R
@ -25,9 +26,10 @@ protocol ns3(I,R)
read_1(I,R, {I,ni}pk(R) ); read_1(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr}pk(I) ); send_2(R,I, {ni,nr}pk(I) );
read_3(I,R, {nr}pk(R) ); read_3(I,R, {nr}pk(R) );
claim_r1(R,Secret,ni,nr); claim_r1(R,Secret,ni);
claim_r2(R,Niagree); claim_r2(R,Secret,nr);
claim_r3(R,Nisynch); claim_r3(R,Niagree);
claim_r4(R,Nisynch);
} }
} }

14
spdl/nsl3.spdl
View File

@ -12,9 +12,10 @@ protocol nsl3(I,R)
send_1(I,R, {I,ni}pk(R) ); send_1(I,R, {I,ni}pk(R) );
read_2(R,I, {ni,nr,R}pk(I) ); read_2(R,I, {ni,nr,R}pk(I) );
send_3(I,R, {nr}pk(R) ); send_3(I,R, {nr}pk(R) );
claim_i1(I,Secret,ni,nr); claim_i1(I,Secret,ni);
claim_i2(I,Niagree); claim_i2(I,Secret,nr);
claim_i3(I,Nisynch); claim_i3(I,Niagree);
claim_i4(I,Nisynch);
} }
role R role R
@ -25,9 +26,10 @@ protocol nsl3(I,R)
read_1(I,R, {I,ni}pk(R) ); read_1(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) ); send_2(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) ); read_3(I,R, {nr}pk(R) );
claim_r1(R,Secret,ni,nr); claim_r1(R,Secret,ni);
claim_r2(R,Niagree); claim_r2(R,Secret,nr);
claim_r3(R,Nisynch); claim_r3(R,Niagree);
claim_r4(R,Nisynch);
} }
} }

3
spdl/nsl7.spdl
View File

@ -12,7 +12,8 @@ protocol nsl7(I,R)
read_1(I,R, {I,ni}pk(R) ); read_1(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) ); send_2(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) ); read_3(I,R, {nr}pk(R) );
claim_4(I,Secret,nr,ni); claim_4(I,Secret,ni);
claim_5(I,Secret,nr);
} }
} }

3
spdl/tmn.spdl
View File

@ -14,7 +14,8 @@ protocol tmn(A,B,S)
send_1(A,S, B,{Ka}pk(S) ); send_1(A,S, B,{Ka}pk(S) );
read_4(S,A, B,{Kb}Ka ); read_4(S,A, B,{Kb}Ka );
claim_5(A,Secret,Ka,Kb); claim_5(A,Secret,Ka);
claim_8(A,Secret,Kb);
} }
role B role B