diff --git a/spdl/bke-generalized-4.spdl b/spdl/bke-generalized-4.spdl index afda1b9..3c78dc0 100644 --- a/spdl/bke-generalized-4.spdl +++ b/spdl/bke-generalized-4.spdl @@ -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 );