diff --git a/spdl/nsl-generalized-4.spdl b/spdl/nsl-generalized-4.spdl new file mode 100644 index 0000000..e03a3e5 --- /dev/null +++ b/spdl/nsl-generalized-4.spdl @@ -0,0 +1,99 @@ +/* + * Generalized Needham-Schroeder-Lowe protocol. + * Four-party version. + * + * Cas Cremers + * Mon May 23 11:49:29 CEST 2005 + */ + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol nslgen4(R1,R2,R3,R4) +{ + role R1 + { + const n1: Nonce; + var n2,n3,n4: Nonce; + + send_1(R1,R2, {R1,R3,R4,n1}pk(R2) ); + read_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) ); + send_5(R1,R2, {n2,n3,n4,R3,R4}pk(R2) ); + + claim_r1a(R1,Secret,n1); + claim_r1b(R1,Secret,n2); + claim_r1c(R1,Secret,n3); + claim_r1d(R1,Secret,n4); + + claim_r1A(R1,Niagree); + claim_r1S(R1,Nisynch); + } + + role R2 + { + 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_5(R1,R2, {n2,n3,n4,R3,R4}pk(R2) ); + send_6(R2,R3, {n3,n4,R4}pk(R3) ); + + claim_r2a(R2,Secret,n1); + claim_r2b(R2,Secret,n2); + claim_r2c(R2,Secret,n3); + claim_r2d(R2,Secret,n4); + + claim_r2A(R2,Niagree); + claim_r2S(R2,Nisynch); + } + + role R3 + { + 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_6(R2,R3, {n3,n4,R4}pk(R3) ); + send_7(R3,R4, {n4}pk(R4) ); + + claim_r3a(R3,Secret,n1); + claim_r3b(R3,Secret,n2); + claim_r3c(R3,Secret,n3); + claim_r3d(R3,Secret,n4); + + claim_r3A(R3,Niagree); + claim_r3S(R3,Nisynch); + } + + role R4 + { + const n4: Nonce; + var n1,n2,n3: Nonce; + + read_3(R3,R4, {n1,n2,n3,R1,R2,R3}pk(R4) ); + send_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) ); + read_7(R3,R4, {n4}pk(R4) ); + + claim_r4a(R4,Secret,n1); + claim_r4b(R4,Secret,n2); + claim_r4c(R4,Secret,n3); + claim_r4d(R4,Secret,n4); + + claim_r4A(R4,Niagree); + claim_r4S(R4,Nisynch); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + +run nslgen4.R1(Agent,Agent,Agent,Agent); +run nslgen4.R2(Agent,Agent,Agent,Agent); +run nslgen4.R3(Agent,Agent,Agent,Agent); +run nslgen4.R4(Agent,Agent,Agent,Agent);