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

- Fixes.

Browse Source
This commit is contained in:
ccremers 2005-04-21 12:13:04 +00:00
parent 8e1041b567
commit 5b3e177e2d
4 changed files with 20 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
spdl/2r890-ex3-a.spdl
View File

@ -19,9 +19,9 @@ protocol course2r890year0405ex3(X,Y,I)
const ny: Nonce; const ny: Nonce;
send_1(I,X, nx ); send_1(I,X, nx );
read_2(X,I, { nx,I }sk(X) ); read_2(X,I, { I,nx }sk(X) );
send_3(I,Y, ny ); send_3(I,Y, ny );
read_4(Y,I, { I,ny }sk(Y) ); read_4(Y,I, { ny,I }sk(Y) );
claim_i1(I,Niagree); claim_i1(I,Niagree);
claim_i2(I,Nisynch); claim_i2(I,Nisynch);
@ -32,7 +32,7 @@ protocol course2r890year0405ex3(X,Y,I)
var nx: Nonce; var nx: Nonce;
read_1(I,X, nx ); read_1(I,X, nx );
send_2(X,I, { nx,I }sk(X) ); send_2(X,I, { I,nx }sk(X) );
} }
role Y role Y
@ -40,7 +40,7 @@ protocol course2r890year0405ex3(X,Y,I)
var ny: Nonce; var ny: Nonce;
read_3(I,Y, ny ); read_3(I,Y, ny );
send_4(Y,I, { I,ny }sk(Y) ); send_4(Y,I, { ny,I }sk(Y) );
} }
} }

8
spdl/2r890-ex3-b.spdl
View File

@ -18,9 +18,9 @@ protocol course2r890year0405ex3(X,Y,I)
const ni: Nonce; const ni: Nonce;
send_1(I,X, ni ); send_1(I,X, ni );
read_2(X,I, { ni,I }sk(X) ); read_2(X,I, { I,ni }sk(X) );
send_3(I,Y, ni ); send_3(I,Y, ni );
read_4(Y,I, { I,ni }sk(Y) ); read_4(Y,I, { ni,I }sk(Y) );
claim_i1(I,Niagree); claim_i1(I,Niagree);
claim_i2(I,Nisynch); claim_i2(I,Nisynch);
@ -31,7 +31,7 @@ protocol course2r890year0405ex3(X,Y,I)
var nx: Nonce; var nx: Nonce;
read_1(I,X, nx ); read_1(I,X, nx );
send_2(X,I, { nx,I }sk(X) ); send_2(X,I, { I,nx }sk(X) );
} }
role Y role Y
@ -39,7 +39,7 @@ protocol course2r890year0405ex3(X,Y,I)
var ny: Nonce; var ny: Nonce;
read_3(I,Y, ny ); read_3(I,Y, ny );
send_4(Y,I, { I,ny }sk(Y) ); send_4(Y,I, { ny,I }sk(Y) );
} }
} }

8
spdl/ns3.spdl
View File

@ -56,4 +56,12 @@ compromised sk(Eve);
run ns3.I(Agent,Agent); run ns3.I(Agent,Agent);
run ns3.R(Agent,Agent); run ns3.R(Agent,Agent);
run ns3.I(Agent,Agent);
run ns3.R(Agent,Agent);
run ns3.I(Agent,Agent);
run ns3.R(Agent,Agent);
run ns3.I(Agent,Agent);
run ns3.R(Agent,Agent);
run ns3.I(Agent,Agent);
run ns3.R(Agent,Agent);

6
spdl/tls-paulson.cpp
View File

@ -36,7 +36,8 @@ 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_9(a, Secret,CLIENTK, SERVERK); claim_9a(a, Secret, SERVERK);
claim_9b(a, Secret, CLIENTK);
} }
@ -57,7 +58,8 @@ 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_10(b, Secret,CLIENTK, SERVERK); claim_10a(b, Secret, SERVERK);
claim_10b(b, Secret, CLIENTK);
} }
} }