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

- Improvements in the scenarios.

Browse Source
This commit is contained in:
ccremers 2004-08-27 19:08:31 +00:00
parent 4f534410bd
commit 939ece7500
4 changed files with 10 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spdl/ns3.spdl
View File

@ -13,6 +13,7 @@ protocol ns3(I,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_4(I,Secret,ni,nr); claim_4(I,Secret,ni,nr);
claim_6(I,Nisynch);
} }
role R role R
@ -24,6 +25,7 @@ protocol ns3(I,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_5(R,Secret,ni,nr); claim_5(R,Secret,ni,nr);
claim_7(R,Nisynch);
} }
} }

10
spdl/nsl3-nisynch-rep.spdl
View File

@ -10,10 +10,11 @@ protocol nsl3(I,R)
var nr: Nonce; var nr: Nonce;
send_1(I,R, {I,ni}pk(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) ); read_2(R,I, {ni,nr,R}pk(I) );
read_6(R,I, {ni,nr,R}pk(I) );
send_3(I,R, {nr}pk(R) ); send_3(I,R, {nr}pk(R) );
claim_4(I,Nisynch); claim_4(I,Niagree);
claim_7(I,Nisynch);
} }
role R role R
@ -22,10 +23,11 @@ protocol nsl3(I,R)
const nr: Nonce; const nr: Nonce;
read_1(I,R, {I,ni}pk(R) ); read_1(I,R, {I,ni}pk(R) );
read_6(I,R, {I,ni}pk(R) );
send_2(R,I, {ni,nr,R}pk(I) ); send_2(R,I, {ni,nr,R}pk(I) );
send_6(R,I, {ni,nr,R}pk(I) );
read_3(I,R, {nr}pk(R) ); read_3(I,R, {nr}pk(R) );
claim_5(I,Nisynch); claim_5(R,Niagree);
claim_8(R,Nisynch);
} }
} }

2
spdl/nsl3-nisynch.spdl
View File

@ -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_5(I,Nisynch); claim_5(R,Nisynch);
} }
} }

2
spdl/nsl3.spdl
View File

@ -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_5(I,Secret,ni,nr); claim_5(R,Secret,ni,nr);
} }
} }