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

- Anti-typeflaw reordering.

Browse Source
This commit is contained in:
ccremers 2005-05-23 13:51:39 +00:00
parent 76aa940e1d
commit 907243281d
1 changed files with 9 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
spdl/nsl-generalized-4.spdl
View File

@ -2,7 +2,9 @@
* Generalized Needham-Schroeder-Lowe protocol.
* Four-party version.
*
* Vulnerable to a typeflaw attack but otherwise okay.
* Specific order of interleaving in message 1-4 is required to (a)
* avoid type flaws whilst (b) retaining NSL structure for the simple
* case.
*
* Mon May 23 11:49:29 CEST 2005
*/
@ -18,7 +20,7 @@ protocol nslgen4(R1,R2,R3,R4)
const n1: Nonce;
var n2,n3,n4: Nonce;
send_1(R1,R2, {R1,R3,R4,n1}pk(R2) );
send_1(R1,R2, {n1,R1,R3,R4}pk(R2) );
read_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
send_5(R1,R2, {n2,n3,n4}pk(R2) );
@ -36,8 +38,8 @@ protocol nslgen4(R1,R2,R3,R4)
const n2: Nonce;
var n1,n3,n4: Nonce;
read_1(R1,R2, {R1,R3,R4,n1}pk(R2) );
send_2(R2,R3, {n1,n2,R1,R2,R4}pk(R3) );
read_1(R1,R2, {n1,R1,R3,R4}pk(R2) );
send_2(R2,R3, {n1,R1,n2,R2,R4}pk(R3) );
read_5(R1,R2, {n2,n3,n4}pk(R2) );
send_6(R2,R3, {n3,n4}pk(R3) );
@ -55,8 +57,8 @@ protocol nslgen4(R1,R2,R3,R4)
const n3: Nonce;
var n1,n2,n4: Nonce;
read_2(R2,R3, {n1,n2,R1,R2,R4}pk(R3) );
send_3(R3,R4, {n1,n2,n3,R1,R2,R3}pk(R4) );
read_2(R2,R3, {n1,R1,n2,R2,R4}pk(R3) );
send_3(R3,R4, {n1,R1,n2,R2,n3,R3}pk(R4) );
read_6(R2,R3, {n3,n4}pk(R3) );
send_7(R3,R4, {n4}pk(R4) );
@ -74,7 +76,7 @@ protocol nslgen4(R1,R2,R3,R4)
const n4: Nonce;
var n1,n2,n3: Nonce;
read_3(R3,R4, {n1,n2,n3,R1,R2,R3}pk(R4) );
read_3(R3,R4, {n1,R1,n2,R2,n3,R3}pk(R4) );
send_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
read_7(R3,R4, {n4}pk(R4) );