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

- Fixed type flaw problem.

Browse Source
This commit is contained in:
ccremers 2005-05-24 14:31:55 +00:00
parent 907243281d
commit f8bafdcd60
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/bke-generalized-4.spdl
View File

@ -2,7 +2,9 @@
* Generalized Bilateral Key Exchange 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 BKE structure for the simple
* case.
*
* Cas Cremers
* Mon May 23 15:15:37 CEST 2005
@ -20,7 +22,7 @@ protocol bkegen4(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 );
@ -38,8 +40,8 @@ protocol bkegen4(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 );
send_6(R2,R3, {n3}n4 );
@ -57,8 +59,8 @@ protocol bkegen4(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 );
send_7(R3,R4, {zero}n4 );
@ -76,7 +78,7 @@ protocol bkegen4(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, {zero}n4 );