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

- Updates for the new claims stuff.

Browse Source
This commit is contained in:
ccremers 2004-02-22 13:16:53 +00:00
parent 59f61abb9f
commit 95f8558514
16 changed files with 29 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
spdl/ns3-brutus.spdl
View File

@ -12,7 +12,7 @@ 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(I,nr); claim(I,Secret,nr);
} }
role R role R
@ -23,7 +23,7 @@ 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(I,ni); claim(I,Secret,ni);
} }
} }

4
spdl/ns3-extreme.spdl
View File

@ -12,7 +12,7 @@ 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(I,nr); claim(I,Secret,nr);
} }
role R role R
@ -23,7 +23,7 @@ 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(I,ni); claim(I,Secret,ni);
} }
} }

4
spdl/ns3-var.spdl
View File

@ -12,7 +12,7 @@ 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(I,ni,nr); claim(I,Secret,ni,nr);
} }
role R role R
@ -23,7 +23,7 @@ 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(R,ni,nr); claim(R,Secret,ni,nr);
} }
} }

4
spdl/ns3.spdl
View File

@ -12,7 +12,7 @@ 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(I,ni,nr); claim(I,Secret,ni,nr);
} }
role R role R
@ -23,7 +23,7 @@ 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(R,ni,nr); claim(R,Secret,ni,nr);
} }
} }

4
spdl/nsl3-var.spdl
View File

@ -12,7 +12,7 @@ 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(I,ni,nr); claim(I,Secret,ni,nr);
} }
role R role R
@ -23,7 +23,7 @@ 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(I,ni,nr); claim(I,Secret,ni,nr);
} }
} }

4
spdl/nsl3.spdl
View File

@ -12,7 +12,7 @@ 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(I,ni,nr); claim(I,Secret,ni,nr);
} }
role R role R
@ -23,7 +23,7 @@ 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(I,ni,nr); claim(I,Secret,ni,nr);
} }
} }

2
spdl/nsl7.spdl
View File

@ -12,7 +12,7 @@ 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(I,nr,ni); claim(I,Secret,nr,ni);
} }
} }

4
spdl/otwayrees.spdl
View File

@ -16,7 +16,7 @@ protocol otwayrees(A,B,S)
send_1(A,B, M,A,B, { na,M,A,B }k(A,S) ); send_1(A,B, M,A,B, { na,M,A,B }k(A,S) );
read_4(B,A, M, { na,kab }k(A,S) ); read_4(B,A, M, { na,kab }k(A,S) );
claim(A, kab); claim(A, Secret,kab);
} }
role B role B
@ -32,7 +32,7 @@ protocol otwayrees(A,B,S)
read_3(S,B, M, t2, { nb,kab }k(B,S) ); read_3(S,B, M, t2, { nb,kab }k(B,S) );
send_4(B,A, M, t2 ); send_4(B,A, M, t2 );
claim(B, kab); claim(B, Secret,kab);
} }
role S role S

4
spdl/tls-paulson.spdl
View File

@ -34,7 +34,7 @@ protocol tlspaulson(a,b)
send_7( a,b, { F }CLIENTK ); send_7( a,b, { F }CLIENTK );
read_8( b,a, { F }SERVERK ); read_8( b,a, { F }SERVERK );
claim(a, CLIENTK, SERVERK); claim(a, Secret,CLIENTK, SERVERK);
} }
@ -55,7 +55,7 @@ protocol tlspaulson(a,b)
read_7( a,b, { F }CLIENTK ); read_7( a,b, { F }CLIENTK );
send_8( b,a, { F }SERVERK ); send_8( b,a, { F }SERVERK );
claim(a, CLIENTK, SERVERK); claim(a, Secret,CLIENTK, SERVERK);
} }
} }

6
spdl/tmn.spdl
View File

@ -12,7 +12,7 @@ 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(A,Ka,Kb); claim(A,Secret,Ka,Kb);
} }
role B role B
@ -22,7 +22,7 @@ protocol tmn(A,B,S)
read_2(S,B, A ); read_2(S,B, A );
send_3(B,S, A, { Kb }pk(S) ); send_3(B,S, A, { Kb }pk(S) );
claim(B,Kb); claim(B,Secret,Kb);
} }
role S role S
@ -34,7 +34,7 @@ protocol tmn(A,B,S)
read_3(B,S, A, { Kb }pk(S) ); read_3(B,S, A, { Kb }pk(S) );
send_4(S,A, B,{Kb}Ka ); send_4(S,A, B,{Kb}Ka );
//claim(S,Ka); //claim(S,Secret,Ka);
} }
} }

2
spdl/wmf-brutus.spdl
View File

@ -18,7 +18,7 @@ protocol wmfbrutus(A,B,S)
read_2(S,B, { A, kab }k(B,S) ); read_2(S,B, { A, kab }k(B,S) );
claim(B, kab); claim(B, Secret,kab);
} }
role S role S

2
spdl/woolam-ce.spdl
View File

@ -28,7 +28,7 @@ protocol woolamce(A,B,S)
send_6(B,A, { B,(Na,(Nb,Kab)) }Kas, { Na,Nb }Kab ); send_6(B,A, { B,(Na,(Nb,Kab)) }Kas, { Na,Nb }Kab );
read_7(A,B, { Nb }Kab ); read_7(A,B, { Nb }Kab );
claim(B,authToken); claim(B,Secret,authToken);
} }
} }

2
spdl/woolam-cmv.spdl
View File

@ -28,7 +28,7 @@ protocol woolamcmv(A,B,S)
send_6(B,A, t2, { Na,Nb }Kab ); send_6(B,A, t2, { Na,Nb }Kab );
read_7(A,B, { Nb }Kab ); read_7(A,B, { Nb }Kab );
claim(B,Kab,Nb,authToken); claim(B,Secret,Kab,Nb,authToken);
} }
} }

4
spdl/yahalom-ban.spdl
View File

@ -19,7 +19,7 @@ protocol yahalomBan(A,B,S)
send_1(A,B, A,na); send_1(A,B, A,na);
read_3(S,A, nb, {B,kab,na}k(A,S), ticket ); read_3(S,A, nb, {B,kab,na}k(A,S), ticket );
send_4(A,B, ticket, {nb}kab ); send_4(A,B, ticket, {nb}kab );
claim(A, kab); claim(A, Secret,kab);
} }
role B role B
@ -32,7 +32,7 @@ protocol yahalomBan(A,B,S)
read_1(A,B, A,na); read_1(A,B, A,na);
send_2(B,S, B,nb, {A,na}k(B,S) ); send_2(B,S, B,nb, {A,na}k(B,S) );
read_4(A,B, {A,kab,nb}k(B,S) , {nb}kab ); read_4(A,B, {A,kab,nb}k(B,S) , {nb}kab );
claim(B, kab); claim(B, Secret,kab);
} }
role S role S

4
spdl/yahalom-lowe.spdl
View File

@ -17,7 +17,7 @@ protocol yahalomlowe(A,B,S)
send_1(A,B, A,na); send_1(A,B, A,na);
read_3(S,A, {B,kab,na,nb}k(A,S) ); read_3(S,A, {B,kab,na,nb}k(A,S) );
send_5(A,B, {A,B,S,nb}kab ); send_5(A,B, {A,B,S,nb}kab );
claim(A, kab); claim(A, Secret,kab);
} }
role B role B
@ -30,7 +30,7 @@ protocol yahalomlowe(A,B,S)
send_2(B,S, {A,na,nb}k(B,S) ); send_2(B,S, {A,na,nb}k(B,S) );
read_4(S,B, {A,kab}k(B,S) ); read_4(S,B, {A,kab}k(B,S) );
read_5(A,B, {A,B,S,nb}kab ); read_5(A,B, {A,B,S,nb}kab );
claim(B, kab); claim(B, Secret,kab);
} }
role S role S

4
spdl/yahalom.spdl
View File

@ -16,7 +16,7 @@ protocol yahalom(A,B,S)
send_1(A,B, A,na); send_1(A,B, A,na);
read_3(S,A, nb, {B,kab,na,nb}k(A,S), ticket ); read_3(S,A, nb, {B,kab,na,nb}k(A,S), ticket );
send_4(A,B, ticket, {nb}kab ); send_4(A,B, ticket, {nb}kab );
claim(A, kab); claim(A, Secret,kab);
} }
role B role B
@ -29,7 +29,7 @@ protocol yahalom(A,B,S)
read_1(A,B, A,na); read_1(A,B, A,na);
send_2(B,S, B,nb, {A,na,nb}k(B,S) ); send_2(B,S, B,nb, {A,na,nb}k(B,S) );
read_4(A,B, {A,kab}k(B,S) , {nb}kab ); read_4(A,B, {A,kab}k(B,S) , {nb}kab );
claim(B, kab); claim(B, Secret,kab);
} }
role S role S