diff --git a/spdl/misc/andrew-ban.spdl b/spdl/misc/andrew-ban.spdl new file mode 100644 index 0000000..3524f75 --- /dev/null +++ b/spdl/misc/andrew-ban.spdl @@ -0,0 +1,53 @@ +usertype SessionKey; +secret k: Function; + +protocol andrewBan(I,R) +{ + role I + { + const ni: Nonce; + var nr,nr2: Nonce; + var kir: SessionKey; + + send_1(I,R, I,{ni}k(I,R) ); + read_2(R,I, {ni,nr}k(I,R) ); + send_3(I,R, {nr}k(I,R) ); + read_4(R,I, {kir,nr2,ni}k(I,R) ); + claim_5(I,Nisynch); + claim_5b(I,Niagree); + claim_6(I,Secret, kir); + claim_7(I,Secret, k(I,R)); + } + + role R + { + var ni: Nonce; + const nr,nr2: Nonce; + const kir: SessionKey; + + read_1(I,R, I,{ni}k(I,R) ); + send_2(R,I, {ni,nr}k(I,R) ); + read_3(I,R, {nr}k(I,R) ); + send_4(R,I, {kir,nr2,ni}k(I,R) ); + claim_8(R,Nisynch); + claim_8b(R,Niagree); + claim_9(R,Secret, kir); + claim_10(R,Secret, k(I,R)); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const kee: SessionKey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Alice,Eve); +compromised k(Bob,Eve); + +run andrewBan.I(Agent,Agent); +run andrewBan.R(Agent,Agent); +run andrewBan.I(Agent,Agent); +run andrewBan.R(Agent,Agent); diff --git a/spdl/misc/andrew-lowe-ban.spdl b/spdl/misc/andrew-lowe-ban.spdl new file mode 100644 index 0000000..8c292bd --- /dev/null +++ b/spdl/misc/andrew-lowe-ban.spdl @@ -0,0 +1,53 @@ +usertype SessionKey; +secret k: Function; + +protocol andrewLoweBan(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: SessionKey; + + send_1(I,R, I,ni ); + read_2(R,I, {ni,kir,I}k(I,R) ); + send_3(I,R, {ni}kir ); + read_4(R,I, nr ); + claim_5(I,Nisynch); + claim_5b(I,Niagree); + claim_6(I,Secret, kir); + claim_7(I,Secret, k(I,R)); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + const kir: SessionKey; + + read_1(I,R, I,ni ); + send_2(R,I, {ni,kir,I}k(I,R) ); + read_3(I,R, {ni}kir ); + send_4(R,I, nr ); + claim_8(R,Nisynch); + claim_8b(R,Niagree); + claim_9(R,Secret, kir); + claim_10(R,Secret, k(I,R)); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const kee: SessionKey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Alice,Eve); +compromised k(Bob,Eve); + +run andrewLoweBan.I(Agent,Agent); +run andrewLoweBan.R(Agent,Agent); +run andrewLoweBan.I(Agent,Agent); +run andrewLoweBan.R(Agent,Agent); diff --git a/spdl/misc/bke-broken.spdl b/spdl/misc/bke-broken.spdl new file mode 100644 index 0000000..4d2321e --- /dev/null +++ b/spdl/misc/bke-broken.spdl @@ -0,0 +1,48 @@ +/* + Bilateral Key Exchange with Public Key protocol (bkebroken) + Broken version with man in the middle attack. +*/ + +usertype Key; + +const pk,h: Function; +secret sk,hinv: Function; + +inversekeys (pk,sk); +inversekeys (h,hinv); + +protocol bkebroken(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Key; + + send_1 (I,R, { ni,I }pk(R) ); + read_2 (R,I, { h(ni),nr,kir }pk(I) ); + send_3 (I,R, { h(nr),kir }pk(R) ); + claim_4 (I, Secret, kir ); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + const kir: Key; + + read_1 (I,R, { ni,I }pk(R) ); + send_2 (R,I, { h(ni),nr,kir }pk(I) ); + read_3 (I,R, { h(nr),kir }pk(R) ); + claim_5 (R, Secret, kir ); + } +} + +const a,b,e: Agent; + +untrusted e; +compromised sk(e); +const ne: Nonce; + +run bkebroken.I(a,Agent); +run bkebroken.R(Agent,b); diff --git a/spdl/misc/bke-one.spdl b/spdl/misc/bke-one.spdl new file mode 100644 index 0000000..a5e8325 --- /dev/null +++ b/spdl/misc/bke-one.spdl @@ -0,0 +1,58 @@ +/* + Bilateral Key Exchange with Public Key protocol (bkeONE) +*/ + +usertype Key; + +const pk,hash: Function; +secret sk,unhash: Function; + +inversekeys (pk,sk); +inversekeys (hash,unhash); + +protocol bkeONE(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Key; + + send_1 (I,R, { ni,I }pk(R) ); + read_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); + send_3 (I,R, { hash(nr) }kir ); + claim_4 (I, Secret, kir ); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + const kir: Key; + + read_1 (I,R, { ni,I }pk(R) ); + send_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); + read_3 (I,R, { hash(nr) }kir ); + claim_5 (R, Secret, kir ); + } +} + +const a,e: Agent; + +untrusted e; +compromised sk(e); +const ne: Nonce; + +run bkeONE.I(a,Agent); +run bkeONE.R(Agent,a); +run bkeONE.I(a,Agent); +run bkeONE.R(Agent,a); + +run bkeONE.I(a,Agent); +run bkeONE.R(Agent,a); +run bkeONE.I(a,Agent); +run bkeONE.R(Agent,a); + +run bkeONE.I(a,Agent); +run bkeONE.R(Agent,a); + diff --git a/spdl/misc/bke-variation.spdl b/spdl/misc/bke-variation.spdl new file mode 100644 index 0000000..6f7e91f --- /dev/null +++ b/spdl/misc/bke-variation.spdl @@ -0,0 +1,55 @@ +/* + Bilateral Key Exchange with Public Key protocol (BKEPK) + Variation for exercise 2r890 +*/ + +usertype Key; + +const pk,hash: Function; +secret sk,unhash: Function; + +inversekeys (pk,sk); +inversekeys (hash,unhash); + +protocol bkevariation(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Key; + + send_1 (I,R, { ni,I }pk(R) ); + read_2 (R,I, { hash(ni),nr,kir }pk(I) ); + send_3 (I,R, { hash(nr) }kir ); + claim_4 (I, Secret, kir ); + claim_5 (I, Niagree ); + claim_6 (I, Nisynch ); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + const kir: Key; + + read_1 (I,R, { ni,I }pk(R) ); + send_2 (R,I, { hash(ni),nr,kir }pk(I) ); + read_3 (I,R, { hash(nr) }kir ); + claim_7 (R, Secret, kir ); + claim_8 (R, Niagree ); + claim_9 (R, Nisynch ); + } +} + +const a,b,e: Agent; + +untrusted e; +compromised sk(e); +const ne: Nonce; + +run bkevariation.I(a,Agent); +run bkevariation.R(Agent,b); +run bkevariation.I(a,Agent); +run bkevariation.R(Agent,b); + diff --git a/spdl/misc/bke.spdl b/spdl/misc/bke.spdl new file mode 100644 index 0000000..73d9ac5 --- /dev/null +++ b/spdl/misc/bke.spdl @@ -0,0 +1,62 @@ +/* + Bilateral Key Exchange with Public Key protocol (BKEPK) +*/ + +usertype Key; + +const pk,hash: Function; +secret sk,unhash: Function; + +inversekeys (pk,sk); +inversekeys (hash,unhash); + +protocol bke(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Key; + + send_1 (I,R, { ni,I }pk(R) ); + read_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); + send_3 (I,R, { hash(nr) }kir ); + claim_4 (I, Secret, kir ); + claim_5 (I, Niagree ); + claim_6 (I, Nisynch ); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + const kir: Key; + + read_1 (I,R, { ni,I }pk(R) ); + send_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); + read_3 (I,R, { hash(nr) }kir ); + claim_7 (R, Secret, kir ); + claim_8 (R, Niagree ); + claim_9 (R, Nisynch ); + } +} + +const a,b,e: Agent; + +untrusted e; +compromised sk(e); +const ne: Nonce; + +run bke.I(a,Agent); +run bke.R(Agent,b); +run bke.I(a,Agent); +run bke.R(Agent,b); + +run bke.I(a,Agent); +run bke.R(Agent,b); +run bke.I(a,Agent); +run bke.R(Agent,b); + +run bke.I(a,Agent); +run bke.R(Agent,b); + diff --git a/spdl/misc/bkepk-ce.spdl b/spdl/misc/bkepk-ce.spdl new file mode 100644 index 0000000..d74a1f2 --- /dev/null +++ b/spdl/misc/bkepk-ce.spdl @@ -0,0 +1,61 @@ +/* + Bilateral Key Exchange with Public Key protocol (bkeCE) + + Version from Corin/Etalle: An Improved Constraint-Based System for the Verification of Security Protocols. + Tried to stay as close as possible to compare timing results. +*/ + +usertype Key; + +const pk,hash: Function; +secret sk: Function; + +inversekeys (pk,sk); + +protocol bkeCE(A,B,testnonce) +{ + role B + { + const nb: Nonce; + var na: Nonce; + var kab: Key; + + send_1 (B,A, B,{ nb,B }pk(A) ); + read_2 (A,B, { hash(nb),na,A,kab }pk(B) ); + send_3 (B,A, { hash(na) }kab ); + } + + role A + { + var nb: Nonce; + const na: Nonce; + const kab: Key; + + read_1 (B,A, B,{ nb,B }pk(A) ); + send_2 (A,B, { hash(nb),na,A,kab }pk(B) ); + read_3 (B,A, { hash(na) }kab ); + } + + role testnonce + { + var n: Nonce; + + read_4 (testnonce,testnonce, n); + } +} + +const Alice,Bob,Eve; + +compromised sk(Eve); +untrusted Eve; + + +run bkeCE.A(Alice,Bob,Alice); +run bkeCE.A(Alice,Bob,Alice); +run bkeCE.B(Alice,Bob,Alice); +run bkeCE.B(Alice,Bob,Alice); +run bkeCE.testnonce(Alice,Bob,Alice); +run bkeCE.testnonce(Alice,Bob,Alice); + +run bkeCE.A(Alice,Bob,Alice); +run bkeCE.testnonce(Alice,Bob,Alice); diff --git a/spdl/misc/bkepk-ce2.spdl b/spdl/misc/bkepk-ce2.spdl new file mode 100644 index 0000000..0e50a55 --- /dev/null +++ b/spdl/misc/bkepk-ce2.spdl @@ -0,0 +1,62 @@ +/* + Bilateral Key Exchange with Public Key protocol (bkepkCE2) + + Version from Corin/Etalle: An Improved Constraint-Based System for the Verification of Security Protocols. + Tried to stay as close as possible to compare timing results. +*/ + +usertype Key; + +const pk,hash: Function; +secret sk: Function; + +inversekeys (pk,sk); + +protocol bkepkCE2(A,B,testnonce) +{ + role B + { + const nb: Nonce; + var na: Nonce; + var kab: Key; + + send_1 (B,A, B,{ nb,B }pk(A) ); + read_2 (A,B, { hash(nb),na,A,kab }pk(B) ); + send_3 (B,A, { hash(na) }kab ); + } + + role A + { + var nb: Nonce; + const na: Nonce; + const kab: Key; + + read_1 (B,A, B,{ nb,B }pk(A) ); + send_2 (A,B, { hash(nb),na,A,kab }pk(B) ); + read_3 (B,A, { hash(na) }kab ); + } + + role testnonce + { + var n: Nonce; + + read_4 (testnonce,testnonce, n); + } +} + +const Alice,Bob,Eve; + +compromised sk(Eve); +untrusted Eve; + + +run bkepkCE2.A(Alice,Bob,Alice); +run bkepkCE2.A(Alice,Bob,Alice); +run bkepkCE2.A(Alice,Bob,Alice); +run bkepkCE2.B(Alice,Bob,Alice); +run bkepkCE2.B(Alice,Bob,Alice); +run bkepkCE2.B(Alice,Bob,Alice); + +run bkepkCE2.testnonce(Alice,Bob,Alice); +run bkepkCE2.testnonce(Alice,Bob,Alice); +run bkepkCE2.testnonce(Alice,Bob,Alice); diff --git a/spdl/misc/boyd-nsl-fix.spdl b/spdl/misc/boyd-nsl-fix.spdl new file mode 100644 index 0000000..3413026 --- /dev/null +++ b/spdl/misc/boyd-nsl-fix.spdl @@ -0,0 +1,55 @@ +/* + * Boyd fix for NS(L) + * + * From the paper "Towards Extensional Goals in Authentication + * Protocols" + * + * Broken. Best shown by attack id 4. + */ + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); +const hash: Function; +secret unhash: Function; +inversekeys (hash,unhash); + +protocol boydNS(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + + send_1(I,R, {ni}pk(R),I ); + read_2(R,I, {nr}pk(I),hash(ni,R) ); + send_3(I,R, hash(nr, I,R) ); + claim_i1(I,Secret,ni); + claim_i2(I,Secret,nr); + claim_i3(I,Niagree); + claim_i4(I,Nisynch); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + read_1(I,R, {ni}pk(R),I ); + send_2(R,I, {nr}pk(I),hash(ni,R) ); + read_3(I,R, hash(nr, I,R) ); + claim_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + claim_r3(R,Niagree); + claim_r4(R,Nisynch); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + +run boydNS.I(Agent,Agent); +run boydNS.R(Agent,Agent); diff --git a/spdl/misc/boyd.spdl b/spdl/misc/boyd.spdl new file mode 100644 index 0000000..adcf26e --- /dev/null +++ b/spdl/misc/boyd.spdl @@ -0,0 +1,81 @@ +usertype Sessionkey; +usertype Macseed; +secret k: Function; +const m: Function; +secret unm: Function; +const f: Function; + +inversekeys (m, unm); + +/* + * Boyd key agreement + * + * Boyd & Mathuria: Protocols for authentication and key establishment + * (2003) p. 101 + * + * Note that MAC_ks(x) has been interpreted as MAC(x,ks); this + * assumption causes some possible false attacks. + */ + +protocol boyd(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var ks: Macseed; + + send_1 (I,S, I,R, ni ); + read_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr ); + send_4 (I,R, m(nr, m(ks,ni,nr)) ); + + claim_6 (I, Secret, m(ks,ni,nr) ); + claim_7 (I, Niagree); + claim_8 (I, Nisynch); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + var ks: Macseed; + + read_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni ); + send_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr ); + read_4 (I,R, m(nr, m(ks,ni,nr)) ); + + claim_10 (R, Secret, m(ks,ni,nr)); + claim_11 (R, Niagree); + claim_12 (R, Nisynch); + } + + role S + { + var ni,nr: Nonce; + const ks: Macseed; + + read_1 (I,S, I,R, ni ); + send_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni ); + } +} + +const Alice,Bob,Simon,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const mcsde: Macseed; +const ke: Sessionkey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Simon); +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Simon,Eve); + +run boyd.I(Agent,Agent,Simon); +run boyd.R(Agent,Agent,Simon); +run boyd.S(Agent,Agent,Simon); +run boyd.I(Agent,Agent,Simon); +run boyd.R(Agent,Agent,Simon); +run boyd.S(Agent,Agent,Simon); diff --git a/spdl/misc/broken1.spdl b/spdl/misc/broken1.spdl new file mode 100644 index 0000000..800ca6a --- /dev/null +++ b/spdl/misc/broken1.spdl @@ -0,0 +1,39 @@ +/* + * A broken protocol + * + * Cas Cremers + * Visualization challenge of the week. + * Can be checked withouth CL, please do so. + */ + +usertype String, Key; +const PlainSight: String; +secret HelloWorld, HelloServer: String; +secret k: Key; + +protocol broken1(I,R,S) +{ + role I + { + send_1(I, R, PlainSight, {HelloWorld, I, R}k ); + send_2(I, S, {HelloServer, I, S}k ); + } + role R + { + read_3(S, R, {HelloWorld, S, I, R}k ); + read_1(I, R, PlainSight, {HelloWorld, I, R}k ); + claim_4(R, Secret, PlainSight); + } + role S + { + read_2(I, S, {HelloServer, I, S}k ); + send_3(S, R, {HelloWorld, S, I, R}k ); + } +} + +const a, b, S: Agent; + +run broken1.I(a, b, S); +run broken1.R(a, b, S); +run broken1.S(a, b, S); + diff --git a/spdl/misc/bunava-1-3.spdl b/spdl/misc/bunava-1-3.spdl new file mode 100644 index 0000000..0bae140 --- /dev/null +++ b/spdl/misc/bunava-1-3.spdl @@ -0,0 +1,89 @@ +# Buttyan Nagy Vajda protocol 1 (3-party) +# +# Modelled after the description in the paper +# "Efficient multi-party challenge-response protocols for entity +# authentication" +# +# Attacks: +# Does not satisfy ni-agree, because when Alice in the R0 role terminates +# it cannot be sure that the agent in role R1 is aware of having sent a +# reply for Alice. +# R0 type flaw attack exists in which there are only two agents active. +# + +secret k: Function; + +protocol intruderhelp(Swap) +{ + role Swap + { + var T: Ticket; + var R0,R1: Agent; + + read_1(Swap,Swap, { T }k(R0,R1) ); + send_2(Swap,Swap, { T }k(R1,R0) ); + } +} + +protocol bunava13(R0,R1,R2) +{ + role R0 + { + const n0: Nonce; + var n1,n2: Nonce; + + send_1(R0,R1, n0); + read_3(R2,R0, n2,{R2,n1,R1,n0}k(R0,R2) ); + send_4(R0,R1, {R0,n2,R2,n1}k(R0,R1) ); + + claim_A1(R0, Niagree); + claim_A2(R0, Nisynch); + } + + role R1 + { + const n1: Nonce; + var n0,n2: Nonce; + + read_1(R0,R1, n0); + send_2(R1,R2, n1,{R1,n0}k(R1,R2) ); + read_4(R0,R1, {R0,n2,R2,n1}k(R0,R1) ); + send_5(R1,R2, {R1,R0,n2}k(R1,R2) ); + + claim_B1(R1, Niagree); + claim_B2(R1, Nisynch); + } + + role R2 + { + const n2: Nonce; + var n0,n1: Nonce; + + read_2(R1,R2, n1,{R1,n0}k(R1,R2) ); + send_3(R2,R0, n2,{R2,n1,R1,n0}k(R0,R2) ); + read_5(R1,R2, {R1,R0,n2}k(R1,R2) ); + + claim_C1(R2, Niagree); + claim_C2(R2, Nisynch); + } +} + +const Alice,Bob,Charlie,David,Frodo,Gerard,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Charlie,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Charlie); + +# General scenario, 2 parallel runs of the protocol + +run bunava13.R0(Agent,Agent,Agent); +run bunava13.R1(Agent,Agent,Agent); +run bunava13.R2(Agent,Agent,Agent); +run bunava13.R0(Agent,Agent,Agent); +run bunava13.R1(Agent,Agent,Agent); +run bunava13.R2(Agent,Agent,Agent); diff --git a/spdl/misc/bunava-1-4.spdl b/spdl/misc/bunava-1-4.spdl new file mode 100644 index 0000000..8e69760 --- /dev/null +++ b/spdl/misc/bunava-1-4.spdl @@ -0,0 +1,106 @@ +# Buttyan Nagy Vajda protocol 1 (4-party) +# +# Modelled after the description in the paper +# "Efficient multi-party challenge-response protocols for entity +# authentication" +# +# Attacks: +# Does not satisfy ni-agree, because when Alice in the A role terminates +# it cannot be sure that the agent in role B is aware of having sent a +# reply for Alice. +# A type flaw attack exists in which there are only three agents active. +# Especially -m2 attack 17 is nice, I think. +# + +secret k: Function; + +protocol intruderhelp(Swap) +{ + role Swap + { + var T: Ticket; + var A,B: Agent; + + read_1(Swap,Swap, { T }k(A,B) ); + send_2(Swap,Swap, { T }k(B,A) ); + } +} + +protocol bunava14(A,B,C,D) +{ + role A + { + const ra: Nonce; + var rb,rc,rd: Nonce; + + send_1(A,B, ra); + read_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) ); + send_5(A,B, {A,rd,D,rc,C,rb}k(A,B) ); + + claim_A1(A, Niagree); + claim_A2(A, Nisynch); + } + + role B + { + const rb: Nonce; + var ra,rc,rd: Nonce; + + read_1(A,B, ra); + send_2(B,C, rb,{B,ra}k(B,C) ); + read_5(A,B, {A,rd,D,rc,C,rb}k(A,B) ); + send_6(B,C, {B,A,rd,D,rc}k(B,C) ); + + claim_B1(B, Niagree); + claim_B2(B, Nisynch); + } + + role C + { + const rc: Nonce; + var ra,rb,rd: Nonce; + + read_2(B,C, rb,{B,ra}k(B,C) ); + send_3(C,D, rc,{C,rb,B,ra}k(C,D) ); + read_6(B,C, {B,A,rd,D,rc}k(B,C) ); + send_7(C,D, {C,B,A,rd}k(C,D) ); + + claim_C1(C, Niagree); + claim_C2(C, Nisynch); + } + + role D + { + const rd: Nonce; + var ra,rb,rc: Nonce; + + read_3(C,D, rc,{C,rb,B,ra}k(C,D) ); + send_4(D,A, rd,{D,rc,C,rb,B,ra}k(A,D) ); + read_7(C,D, {C,B,A,rd}k(C,D) ); + + claim_D1(D, Niagree); + claim_D2(D, Nisynch); + } +} + +const Alice,Bob,Charlie,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Charlie,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Charlie); + +# General scenario, 2 parallel runs of the protocol + +run bunava14.A(Agent,Agent,Agent,Agent); +run bunava14.B(Agent,Agent,Agent,Agent); +run bunava14.C(Agent,Agent,Agent,Agent); +run bunava14.D(Agent,Agent,Agent,Agent); +run bunava14.A(Agent,Agent,Agent,Agent); +run bunava14.B(Agent,Agent,Agent,Agent); +run bunava14.C(Agent,Agent,Agent,Agent); +run bunava14.D(Agent,Agent,Agent,Agent); diff --git a/spdl/misc/bunava-2-3.spdl b/spdl/misc/bunava-2-3.spdl new file mode 100644 index 0000000..76224e1 --- /dev/null +++ b/spdl/misc/bunava-2-3.spdl @@ -0,0 +1,88 @@ +# Buttyan Nagy Vajda protocol 2 (3-party) +# +# Modelled after the description in the paper +# "Efficient multi-party challenge-response protocols for entity +# authentication" +# +# Attacks: +# + +secret k: Function; + +protocol intruderhelp(Swap) +{ + role Swap + { + var T: Ticket; + var R0,R1: Agent; + + read_1(Swap,Swap, { T }k(R0,R1) ); + send_2(Swap,Swap, { T }k(R1,R0) ); + } +} + +protocol bunava23(R0,R1,R2) +{ + role R0 + { + const n0: Nonce; + var n1,n2: Nonce; + var T0: Ticket; + + send_1(R0,R1, n0); + read_3(R2,R0, n2, T0, { R2,{ R1,n0 }k(R0,R1) }k(R0,R2) ); + send_4(R0,R1, { R0,n2 }k(R0,R2), { R0, T0 }k(R0,R1) ); + + claim_A1(R0, Niagree); + claim_A2(R0, Nisynch); + } + + role R1 + { + const n1: Nonce; + var n0,n2: Nonce; + var T1: Ticket; + + read_1(R0,R1, n0); + send_2(R1,R2, n1,{R1,n0}k(R1,R2) ); + read_4(R0,R1, T1, { R0, { R2,n1 }k(R1,R2) }k(R0,R1) ); + send_5(R1,R2, { R1, T1 }k(R1,R2) ); + + claim_B1(R1, Niagree); + claim_B2(R1, Nisynch); + } + + role R2 + { + const n2: Nonce; + var n0,n1: Nonce; + var T2: Ticket; + + read_2(R1,R2, n1, T2 ); + send_3(R2,R0, n2,{ R2,n1 }k(R1,R2), { R2, T2 }k(R0,R2) ); + read_5(R1,R2, { R1, { R0,n2 }k(R0,R2) }k(R1,R2) ); + + claim_C1(R2, Niagree); + claim_C2(R2, Nisynch); + } +} + +const Alice,Bob,Charlie,David,Frodo,Gerard,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Charlie,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Charlie); + +# General scenario + +run bunava23.R0(Agent,Agent,Agent); +run bunava23.R1(Agent,Agent,Agent); +run bunava23.R2(Agent,Agent,Agent); +run bunava23.R0(Agent,Agent,Agent); +run bunava23.R1(Agent,Agent,Agent); +run bunava23.R2(Agent,Agent,Agent); diff --git a/spdl/misc/bunava-2-4.spdl b/spdl/misc/bunava-2-4.spdl new file mode 100644 index 0000000..68e5fe4 --- /dev/null +++ b/spdl/misc/bunava-2-4.spdl @@ -0,0 +1,138 @@ +# Buttyan Nagy Vajda protocol 2 (4-party) +# +# Modelled after the description in the paper +# "Efficient multi-party challenge-response protocols for entity +# authentication" +# +# Note: +# Does not seem to reach the claim. I don't know why yet. TODO +# investigate. +# + +secret k: Function; + +# protocol intruderhelp(Swap) +# { +# role Swap +# { +# var T: Ticket; +# var A,B: Agent; +# +# read_1(Swap,Swap, { T }k(A,B) ); +# send_2(Swap,Swap, { T }k(B,A) ); +# } +# } + +protocol bunava24(A,B,C,D) +{ + role A + { + const ra: Nonce; + var rb,rc,rd: Nonce; + var Tacd, Tabd: Ticket; + + send_1(A,B, ra); + read_4(D,A, rd, + Tacd, + Tabd, + { D, { C, { B,ra }k(A,B) }k(A,C) }k(A,D) + ); +# send_5(A,B, +# { A, rd }k(A,D), +# { A, Tacd }k(A,C), +# { A, Tabd }k(A,B) +# ); + + claim_A1(A, Niagree); + claim_A2(A, Nisynch); + } + + role B + { + const rb: Nonce; + var ra,rc,rd: Nonce; + var Tbad, Tbac: Ticket; + + read_1(A,B, ra); + send_2(B,C, rb, + { B,ra }k(A,B) + ); +# read_5(A,B, +# Tbad, +# Tbac, +# { A, { D, { C,rb }k(B,C) }k(B,D) }k(A,B) +# ); +# send_6(B,C, +# { B, Tbad }k(B,D), +# { B, Tbac }k(B,C) +# ); +# +# claim_B1(B, Niagree); +# claim_B2(B, Nisynch); + } + + role C + { + const rc: Nonce; + var ra,rb,rd: Nonce; + var Tcab,Tcbd: Ticket; + + read_2(B,C, rb, Tcab ); + send_3(C,D, rc, + { C, rb }k(B,C), + { C, Tcab }k(A,C) + ); +# read_6(B,C, +# Tcbd, +# { B, { A,{ D,rc }k(C,D) }k(A,C) }k(B,C) +# ); +# send_7(C,D, +# { C, Tcbd }k(C,D) +# ); +# +# claim_C1(C, Niagree); +# claim_C2(C, Nisynch); + } + + role D + { + const rd: Nonce; + var ra,rb,rc: Nonce; + var Tdbc,Tdac: Ticket; + + read_3(C,D, rc, Tdbc, Tdac ); + send_4(D,A, rd, + { D, rc }k(C,D), + { D, Tdbc }k(B,D), + { D, Tdac }k(A,D) + ); +# read_7(C,D, +# { C, { B,{ A,rd }k(A,D) }k(B,D) }k(C,D) +# ); +# +# claim_D1(D, Niagree); +# claim_D2(D, Nisynch); + } +} + +const Alice,Bob,Charlie,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Charlie,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Charlie); + +# General scenario + +run bunava24.A(Agent,Agent,Agent,Agent); +run bunava24.B(Agent,Agent,Agent,Agent); +run bunava24.C(Agent,Agent,Agent,Agent); +run bunava24.D(Agent,Agent,Agent,Agent); +run bunava24.A(Agent,Agent,Agent,Agent); +run bunava24.B(Agent,Agent,Agent,Agent); +run bunava24.C(Agent,Agent,Agent,Agent); +run bunava24.D(Agent,Agent,Agent,Agent); diff --git a/spdl/misc/carkey-broken-limited.spdl b/spdl/misc/carkey-broken-limited.spdl new file mode 100644 index 0000000..346beaa --- /dev/null +++ b/spdl/misc/carkey-broken-limited.spdl @@ -0,0 +1,32 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol carkeybrokenlim(I,R) +{ + role I + { + const ni: Nonce; + + send_1(I,R, I,R ); + } + + role R + { + var ni: Nonce; + + read_1(I,R, I,R ); + claim_2(R,Nisynch); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const nc: Nonce; +compromised sk(Eve); + +run carkeybrokenlim.I(Alice,Bob); +run carkeybrokenlim.R(Alice,Bob); +run carkeybrokenlim.I(Alice,Bob); +run carkeybrokenlim.R(Alice,Bob); diff --git a/spdl/misc/carkey-broken.spdl b/spdl/misc/carkey-broken.spdl new file mode 100644 index 0000000..a0e0ba5 --- /dev/null +++ b/spdl/misc/carkey-broken.spdl @@ -0,0 +1,32 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol carkeybroken(I,R) +{ + role I + { + const ni: Nonce; + + send_1(I,R, {ni}sk(I) ); + } + + role R + { + var ni: Nonce; + + read_1(I,R, {ni}sk(I) ); + claim_2(R,Nisynch); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const nc: Nonce; +compromised sk(Eve); + +run carkeybroken.I(Agent,Agent); +run carkeybroken.R(Agent,Agent); +run carkeybroken.I(Agent,Agent); +run carkeybroken.R(Agent,Agent); diff --git a/spdl/misc/carkey-ni.spdl b/spdl/misc/carkey-ni.spdl new file mode 100644 index 0000000..ed189b4 --- /dev/null +++ b/spdl/misc/carkey-ni.spdl @@ -0,0 +1,32 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol carkeyni(I,R) +{ + role I + { + const ni: Nonce; + + send_1(I,R, {R,ni}sk(I) ); + } + + role R + { + var ni: Nonce; + + read_1(I,R, {R,ni}sk(I) ); + claim_2(R,Nisynch); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const nc: Nonce; +compromised sk(Eve); + +run carkeyni.I(Agent,Agent); +run carkeyni.R(Agent,Agent); +run carkeyni.I(Agent,Agent); +run carkeyni.R(Agent,Agent); diff --git a/spdl/misc/carkey-ni2.spdl b/spdl/misc/carkey-ni2.spdl new file mode 100644 index 0000000..49bbe95 --- /dev/null +++ b/spdl/misc/carkey-ni2.spdl @@ -0,0 +1,34 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol carkeyni2(I,R) +{ + role I + { + const ni: Nonce; + + send_1(I,R, {R,ni}sk(I) ); + send_2(I,R, {R,ni}sk(I) ); + } + + role R + { + var ni: Nonce; + + read_1(I,R, {R,ni}sk(I) ); + read_2(I,R, {R,ni}sk(I) ); + claim_4(R,Nisynch); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const nc: Nonce; +compromised sk(Eve); + +run carkeyni2.I(Agent,Agent); +run carkeyni2.R(Agent,Agent); +run carkeyni2.I(Agent,Agent); +run carkeyni2.R(Agent,Agent); diff --git a/spdl/misc/ccitt509-ban.spdl b/spdl/misc/ccitt509-ban.spdl new file mode 100644 index 0000000..c4c15d5 --- /dev/null +++ b/spdl/misc/ccitt509-ban.spdl @@ -0,0 +1,53 @@ +usertype Data; +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol ccitt509(I,R) +{ + role I + { + const xi,yi: Data; + const ni: Nonce; + var nr: Nonce; + var yr,xr: Data; + + send_1(I,R, I,{ni, R, xi, {yi}pk(R) }sk(I) ); + read_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) ); + send_3(I,R, I,{R,nr}sk(I) ); + + claim_4(I,Secret,yi); + claim_5(I,Secret,yr); + claim_6(I,Nisynch); + claim_7(I,Niagree); + } + + role R + { + var xi,yi: Data; + var ni: Nonce; + const nr: Nonce; + const yr,xr: Data; + + read_1(I,R, I,{ni, R, xi, {yi}pk(R) }sk(I) ); + send_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) ); + read_3(I,R, I,{R,nr}sk(I) ); + + claim_8(R,Secret,yi); + claim_9(R,Secret,yr); + claim_10(R,Nisynch); + claim_11(R,Niagree); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const de: Data; +compromised sk(Eve); + +run ccitt509.I(Agent,Agent); +run ccitt509.R(Agent,Agent); +run ccitt509.I(Agent,Agent); +run ccitt509.R(Agent,Agent); diff --git a/spdl/misc/denning-sacco-shared.spdl b/spdl/misc/denning-sacco-shared.spdl new file mode 100644 index 0000000..4ace1c8 --- /dev/null +++ b/spdl/misc/denning-sacco-shared.spdl @@ -0,0 +1,74 @@ +/* +* Denning-Sacco shared key +* CJ, but modeled after Sjouke's protocol list +*/ + +/* default includes */ + +/* asymmetric */ + +const pk,hash: Function; +secret sk,unhash: Function; + +/* symmetric */ + +usertype SessionKey, Time, Ticket; +secret k: Function; + +/* agents */ + +const a,b,e: Agent; + + +/* untrusted e */ + +untrusted e; +const ne: Nonce; +const kee: SessionKey; + +compromised k(e,e); +compromised k(e,a); +compromised k(e,b); +compromised k(a,e); +compromised k(b,e); + +protocol denningsaccosh(A,S,B) +{ + role A + { + var t: Time; + var T: Ticket; + var kab: SessionKey; + + send_1 (A,S, A,S ); + read_2 (S,A, {B, kab, t, T}k(A,S) ); + send_3 (A,B, T); + + claim_4 (A, Secret, kab); + claim_5 (A, Nisynch); + claim_6 (A, Niagree); + } + + role S + { + const t: Time; + const kab: SessionKey; + + read_1 (A,S, A,S ); + send_2 (S,A, {B, kab, t, { kab, A,t }k(B,S) }k(A,S) ); + } + + role B + { + var t: Time; + var kab: SessionKey; + + read_3 (A,B, { kab, A,t }k(B,S) ); + + claim_7 (B, Secret, kab); + claim_8 (B, Nisynch); + claim_9 (B, Niagree); + } +} + + diff --git a/spdl/misc/f4.spdl b/spdl/misc/f4.spdl new file mode 100644 index 0000000..b34a06f --- /dev/null +++ b/spdl/misc/f4.spdl @@ -0,0 +1,48 @@ +/* + * f4.spdl + * + * Tailored protocol to show that any number of runs can be required to + * find an attack. + * + * For this version, -m2 and -r4 are needed. + * + * April 2005, Cas Cremers + */ + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol f4(I,R) +{ + role I + { + var nr: Nonce; + + read_1(R,I, nr ); + send_2(I,R, { nr }sk(I) ); + read_3(R,I, {{{{ nr }sk(R)}sk(R)}sk(R)}sk(R) ); + + claim_i1(I,Niagree); + } + + role R + { + const nr: Nonce; + send_1(R,I, nr ); + } + +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + +run f4.I(Agent,Agent); +run f4.I(Agent,Agent); +run f4.I(Agent,Agent); +run f4.I(Agent,Agent); +run f4.I(Agent,Agent); +run f4.I(Agent,Agent); diff --git a/spdl/misc/f5.spdl b/spdl/misc/f5.spdl new file mode 100644 index 0000000..8ed74f2 --- /dev/null +++ b/spdl/misc/f5.spdl @@ -0,0 +1,48 @@ +/* + * f5.spdl + * + * Tailored protocol to show that any number of runs can be required to + * find an attack. + * + * For this version, -m2 and -r5 are needed. + * + * April 2005, Cas Cremers + */ + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol f4(I,R) +{ + role I + { + var nr: Nonce; + + read_1(R,I, nr ); + send_2(I,R, { nr }sk(I) ); + read_3(R,I, {{{{{ nr }sk(R)}sk(R)}sk(R)}sk(R)}sk(R) ); + + claim_i1(I,Niagree); + } + + role R + { + const nr: Nonce; + send_1(R,I, nr ); + } + +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + +run f4.I(Agent,Agent); +run f4.I(Agent,Agent); +run f4.I(Agent,Agent); +run f4.I(Agent,Agent); +run f4.I(Agent,Agent); +run f4.I(Agent,Agent); diff --git a/spdl/misc/five-run-bound.spdl b/spdl/misc/five-run-bound.spdl new file mode 100644 index 0000000..f3cd1e9 --- /dev/null +++ b/spdl/misc/five-run-bound.spdl @@ -0,0 +1,32 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol r5bound(I,R) +{ + role R + { + var k1: Nonce; + var ni: Nonce; + const k2: Nonce; + + read_1 (I,R, ni ); + send_2 (R,I, { ni }sk(R) ); + read_3 (I,R, {{{ {k1}pk(R) }sk(I)}sk(I)}sk(I) ); + send_4 (R,I, {k2}k1 ); + + claim_6 (R, Secret, k2); + } +} + +const Alice, Bob: Agent; +const ne: Nonce; + +run r5bound.R(Agent); +run r5bound.R(Agent); + +run r5bound.R(Agent); +run r5bound.R(Agent); + +run r5bound.R(Agent); +run r5bound.R(Agent); diff --git a/spdl/misc/gong-nonce-b.spdl b/spdl/misc/gong-nonce-b.spdl new file mode 100644 index 0000000..e9bb6d2 --- /dev/null +++ b/spdl/misc/gong-nonce-b.spdl @@ -0,0 +1,81 @@ +usertype Sessionkey; +usertype Keypart; +secret k: Function; +const f: Function; + +/* + * Gong nonce based alternative + * + * Boyd & Mathuria: Protocols for authentication and key establishment + * (2003) p. 101 + */ + +protocol gongnonceb(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + const ki: Keypart; + var kr: Keypart; + + send_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni ); + read_4 (S,I, { S,I,R,kr,I }k(I,S), { R,I,ni }f(ki,kr), nr ); + send_5 (I,R, { I,R,nr }f(ki,kr) ); + + claim_6 (I, Secret, ki); + claim_7 (I, Secret, kr); + claim_8 (I, Nisynch); + claim_9 (I, Niagree); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + const kr: Keypart; + var ki: Keypart; + + read_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni ); + send_3 (R,S, { R,S,R,kr,I }k(R,S), { R,I, ni }f(ki,kr), nr ); + read_5 (I,R, { I,R,nr }f(ki,kr) ); + + claim_10 (R, Secret, ki); + claim_11 (R, Secret, kr); + claim_12 (R, Nisynch); + claim_13 (R, Niagree); + } + + role S + { + var ni,nr: Nonce; + var ki,kr: Keypart; + var T; + + read_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni ); + send_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni ); + read_3 (R,S, { R,S,R,kr,I }k(R,S), T, nr ); + send_4 (S,I, { S,I,R,kr,I }k(I,S), T, nr ); + } +} + +const Alice,Bob,Simon,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const kpe: Keypart; +const ke: Sessionkey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Simon); +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Simon,Eve); + +run gongnonceb.I(Agent,Agent,Simon); +run gongnonceb.R(Agent,Agent,Simon); +run gongnonceb.S(Agent,Agent,Simon); +run gongnonceb.I(Agent,Agent,Simon); +run gongnonceb.R(Agent,Agent,Simon); +run gongnonceb.S(Agent,Agent,Simon); diff --git a/spdl/misc/gong-nonce.spdl b/spdl/misc/gong-nonce.spdl new file mode 100644 index 0000000..3670288 --- /dev/null +++ b/spdl/misc/gong-nonce.spdl @@ -0,0 +1,72 @@ +usertype Sessionkey; +usertype Keypart; +secret k: Function; + +protocol gongnonce(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + const ki: Keypart; + var kr: Keypart; + + send_1 (I,R, I,R,ni ); + read_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr); + send_4 (I,S, { I,S,I, ki, R, nr }k(I,S) ); + + claim_6 (I, Secret, ki); + claim_7 (I, Secret, kr); + claim_8 (I, Nisynch); + claim_9 (I, Niagree); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + const kr: Keypart; + var ki: Keypart; + + read_1 (I,R, I,R,ni ); + send_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S)); + read_5 (S,R, { S,R,I, ki, R, nr }k(R,S) ); + + claim_10 (R, Secret, ki); + claim_11 (R, Secret, kr); + claim_12 (R, Nisynch); + claim_13 (R, Niagree); + } + + role S + { + var ni,nr: Nonce; + var ki,kr: Keypart; + + read_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S)); + send_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr); + read_4 (I,S, { I,S,I, ki, R, nr }k(I,S) ); + send_5 (S,R, { S,R,I, ki, R, nr }k(R,S) ); + } +} + +const Alice,Bob,Simon,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const kpe: Keypart; +const ke: Sessionkey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Simon); +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Simon,Eve); + +run gongnonce.I(Agent,Agent,Simon); +run gongnonce.R(Agent,Agent,Simon); +run gongnonce.S(Agent,Agent,Simon); +run gongnonce.I(Agent,Agent,Simon); +run gongnonce.R(Agent,Agent,Simon); +run gongnonce.S(Agent,Agent,Simon); diff --git a/spdl/misc/helloworld.spdl b/spdl/misc/helloworld.spdl new file mode 100644 index 0000000..597a308 --- /dev/null +++ b/spdl/misc/helloworld.spdl @@ -0,0 +1,17 @@ +usertype String, World; +secret HelloWorld, k: String; + +protocol hw(initiator,world) +{ + role initiator + { + send_1(initiator, world, HelloWorld); + /* claim_2(initiator, Secret, HelloWorld); */ + } +} + +const Alice, Bob: Agent; +const Earth, Mars: World; + +run hw.initiator(Agent,World); + diff --git a/spdl/misc/ibe-ns.spdl b/spdl/misc/ibe-ns.spdl new file mode 100644 index 0000000..5874e2e --- /dev/null +++ b/spdl/misc/ibe-ns.spdl @@ -0,0 +1,69 @@ +// 12/05/06 +// S. Mauw +// Using Identity Based Encryption primitive to make NSL authentication. +// The only requirement on the server communications is that the +// sending of the private key is secret. + +const pk: Function; //public-private keys are used to model a secure channel +secret sk: Function; //from the keyserver to the parties +const ibepublic: Function; //publicly known key construction from server + //parameters and recipient name +secret ibesecret: Function;//secret key determined by server for recipient +const param: Function; //public security parameter of server +inversekeys (pk,sk); +inversekeys (ibepublic,ibesecret); + +protocol ibe(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + +//Note that we are not interested in the order of server messages. + read_!1(S,I, param(S) ); + send_3(I,R, {I,ni}ibepublic(param(S),R) ); + read_4(R,I, {ni,nr,R}ibepublic(param(S),I) ); + send_5(I,R, {nr}ibepublic(param(S),R) ); + + + claim_i1(I,Secret,ni); + claim_i2(I,Secret,nr); + claim_i3(I,Niagree); + claim_i4(I,Nisynch); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + read_!2(S,R, {ibesecret(param(S),R)}pk(R) ); + read_3(I,R, {I,ni}ibepublic(param(S),R) ); + send_4(R,I, {ni,nr,R}ibepublic(param(S),I) ); + read_5(I,R, {nr}ibepublic(param(S),R) ); + + claim_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + claim_r3(R,Niagree); + claim_r4(R,Nisynch); + } + + role S + { + read_!0(S,S, R,S); // workaround for the fact that R & S are roles, so Scyther should not jump to conclusions (remove it and see what happens) + send_!1(S,I, param(S) ); + send_!2(S,R, {ibesecret(param(S),R)}pk(R) ); + + claim_s1(S,Secret,ibesecret(param(S),R)); + } +} + +const Alice, Bob, Carol, Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); +compromised ibesecret(param(Eve),Alice); +compromised ibesecret(param(Eve),Bob); +compromised ibesecret(param(Eve),Carol); diff --git a/spdl/misc/ibe.spdl b/spdl/misc/ibe.spdl new file mode 100644 index 0000000..dc33589 --- /dev/null +++ b/spdl/misc/ibe.spdl @@ -0,0 +1,50 @@ +// 12/05/06 +// S. Mauw +// Modeling of Identity Based Encryption primitive. + +const pk: Function; +secret sk: Function; +const ibepublic: Function; +secret ibesecret: Function; +const param: Function; +inversekeys (pk,sk); +inversekeys (ibepublic,ibesecret); + +protocol ibe(I,R,S) +{ + role I + { + const ni: Nonce; + + read_1(S,I, param(S) ); + send_3(I,R, {ni}ibepublic(param(S),R) ); + + claim_i1(I,Secret,ni); + } + + role R + { + var ni: Nonce; + + read_2(S,R, {ibesecret(param(S),R)}pk(R) ); + read_3(I,R, {ni}ibepublic(param(S),R) ); + + claim_r1(R,Secret,ni); + //of course this claim is invalid + } + + role S + { + send_1(S,I, param(S) ); + send_2(S,R, {ibesecret(param(S),R)}pk(R) ); + } +} + +const Alice, Bob, Carol, Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); +compromised ibesecret(param(Eve),Alice); +compromised ibesecret(param(Eve),Bob); +compromised ibesecret(param(Eve),Carol); diff --git a/spdl/misc/isoiec11770-2-13.spdl b/spdl/misc/isoiec11770-2-13.spdl new file mode 100644 index 0000000..2be4d3d --- /dev/null +++ b/spdl/misc/isoiec11770-2-13.spdl @@ -0,0 +1,63 @@ +usertype Sessionkey; +usertype Ticket; +secret k: Function; + +protocol isoiec11770213(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Sessionkey; + + send_1 (I,R, ni); + read_4 (R,I, { ni,kir,R }k(I,S) ); + + claim_5 (I, Secret, kir); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + const kir: Sessionkey; + var T; + + read_1 (I,R, ni); + send_2 (R,S, { nr,ni,I,kir }k(R,S) ); + read_3 (S,R, { nr, I }k(R,S), T ); + send_4 (R,I, T ); + + claim_6 (R, Secret, kir); + } + + role S + { + var ni,nr: Nonce; + var kir: Sessionkey; + + read_2 (R,S, { nr,ni,I,kir }k(R,S) ); + send_3 (S,R, { nr, I }k(R,S), { ni,kir,R }k(I,S) ); + } +} + +const Alice,Bob,Simon,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const te: Ticket; +const ke: Sessionkey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Simon); +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Simon,Eve); + +run isoiec11770213.I(Agent,Agent,Simon); +run isoiec11770213.R(Agent,Agent,Simon); +run isoiec11770213.S(Agent,Agent,Simon); +run isoiec11770213.I(Agent,Agent,Simon); +run isoiec11770213.R(Agent,Agent,Simon); +run isoiec11770213.S(Agent,Agent,Simon); diff --git a/spdl/misc/kaochow-palm.spdl b/spdl/misc/kaochow-palm.spdl new file mode 100644 index 0000000..559a5e1 --- /dev/null +++ b/spdl/misc/kaochow-palm.spdl @@ -0,0 +1,67 @@ +usertype Sessionkey; +usertype Ticket; +secret k: Function; + +protocol kaochowPalm(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Sessionkey; + + send_1 (I,S, I,R,ni); + read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr ); + send_4 (I,R, {nr}kir ); + + claim_5 (I, Nisynch); + claim_6 (I, Niagree); + claim_7 (I, Secret, kir); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + var kir: Sessionkey; + var T; + + read_2 (S,R, { T, { I,R,ni,kir }k(R,S) }k(R,S) ); + send_3 (R,I, T, {ni}kir, nr ); + read_4 (I,R, {nr}kir ); + + claim_8 (R, Nisynch); + claim_9 (R, Niagree); + claim_10 (R, Secret, kir); + } + + role S + { + var ni: Nonce; + const kir: Sessionkey; + + read_1 (I,S, I,R,ni); + send_2 (S,R, { {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) }k(R,S) ); + } +} + +const Alice,Bob,Simon,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const te: Ticket; +const ke: Sessionkey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Simon); +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Simon,Eve); + +run kaochowPalm.I(Agent,Agent,Simon); +run kaochowPalm.R(Agent,Agent,Simon); +run kaochowPalm.S(Agent,Agent,Simon); +run kaochowPalm.I(Agent,Agent,Simon); +run kaochowPalm.R(Agent,Agent,Simon); +run kaochowPalm.S(Agent,Agent,Simon); diff --git a/spdl/misc/kaochow-v2.spdl b/spdl/misc/kaochow-v2.spdl new file mode 100644 index 0000000..edd8eb4 --- /dev/null +++ b/spdl/misc/kaochow-v2.spdl @@ -0,0 +1,67 @@ +usertype Sessionkey; +usertype Ticket; +secret k: Function; + +protocol kaochow2(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir,kt: Sessionkey; + + send_1 (I,S, I,R,ni); + read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr ); + send_4 (I,R, {nr,kir}kt ); + + claim_5 (I, Nisynch); + claim_6 (I, Niagree); + claim_7 (I, Secret, kir); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + var kir,kt: Sessionkey; + var T: Ticket; + + read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); + send_3 (R,I, R, T, {ni, kir}kt, nr ); + read_4 (I,R, {nr,kir}kt ); + + claim_8 (R, Nisynch); + claim_9 (R, Niagree); + claim_10 (R, Secret, kir); + } + + role S + { + var ni: Nonce; + const kir, kt: Sessionkey; + + read_1 (I,S, I,R,ni); + send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); + } +} + +const Alice,Bob,Simon,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const te: Ticket; +const ke: Sessionkey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Simon); +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Simon,Eve); + +run kaochow2.I(Agent,Agent,Simon); +run kaochow2.R(Agent,Agent,Simon); +run kaochow2.S(Agent,Agent,Simon); +run kaochow2.I(Agent,Agent,Simon); +run kaochow2.R(Agent,Agent,Simon); +run kaochow2.S(Agent,Agent,Simon); diff --git a/spdl/misc/kaochow-v3.spdl b/spdl/misc/kaochow-v3.spdl new file mode 100644 index 0000000..93669fd --- /dev/null +++ b/spdl/misc/kaochow-v3.spdl @@ -0,0 +1,70 @@ +usertype Sessionkey; +usertype Ticket; +usertype Timestamp; +secret k: Function; + +protocol kaochow3(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir,kt: Sessionkey; + var T2: Ticket; + + send_1 (I,S, I,R,ni); + read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); + send_4 (I,R, {nr,kir}kt, T2 ); + + claim_5 (I, Nisynch); + claim_6 (I, Niagree); + claim_7 (I, Secret, kir); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + var kir,kt: Sessionkey; + var T: Ticket; + const tr: Timestamp; + + read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); + send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); + read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) ); + + claim_8 (R, Nisynch); + claim_9 (R, Niagree); + claim_10 (R, Secret, kir); + } + + role S + { + var ni: Nonce; + const kir, kt: Sessionkey; + + read_1 (I,S, I,R,ni); + send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); + } +} + +const Alice,Bob,Simon,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const te: Ticket; +const ke: Sessionkey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Simon); +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Simon,Eve); + +run kaochow3.I(Agent,Agent,Simon); +run kaochow3.R(Agent,Agent,Simon); +run kaochow3.S(Agent,Agent,Simon); +run kaochow3.I(Agent,Agent,Simon); +run kaochow3.R(Agent,Agent,Simon); +run kaochow3.S(Agent,Agent,Simon); diff --git a/spdl/misc/kaochow.spdl b/spdl/misc/kaochow.spdl new file mode 100644 index 0000000..5b17ef5 --- /dev/null +++ b/spdl/misc/kaochow.spdl @@ -0,0 +1,67 @@ +usertype Sessionkey; +usertype Ticket; +secret k: Function; + +protocol kaochow(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Sessionkey; + + send_1 (I,S, I,R,ni); + read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr ); + send_4 (I,R, {nr}kir ); + + claim_5 (I, Nisynch); + claim_6 (I, Niagree); + claim_7 (I, Secret, kir); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + var kir: Sessionkey; + var T; + + read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); + send_3 (R,I, T, {ni}kir, nr ); + read_4 (I,R, {nr}kir ); + + claim_8 (R, Nisynch); + claim_9 (R, Niagree); + claim_10 (R, Secret, kir); + } + + role S + { + var ni: Nonce; + const kir: Sessionkey; + + read_1 (I,S, I,R,ni); + send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) ); + } +} + +const Alice,Bob,Simon,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const te: Ticket; +const ke: Sessionkey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Eve,Simon); +compromised k(Alice,Eve); +compromised k(Bob,Eve); +compromised k(Simon,Eve); + +run kaochow.I(Agent,Agent,Simon); +run kaochow.R(Agent,Agent,Simon); +run kaochow.S(Agent,Agent,Simon); +run kaochow.I(Agent,Agent,Simon); +run kaochow.R(Agent,Agent,Simon); +run kaochow.S(Agent,Agent,Simon); diff --git a/spdl/misc/ksl.spdl b/spdl/misc/ksl.spdl new file mode 100644 index 0000000..635b311 --- /dev/null +++ b/spdl/misc/ksl.spdl @@ -0,0 +1,83 @@ +/* + * KSL from SPORE + * + * Messages 6-8 are intended for repeated authentication, and there are + * known attacks on this. However, we don't model that yet. + * + * Furthermore, it is interesting to experiment here with key + * compromise (of kab), when this is implemented in Scyther. + */ + +usertype Server, SessionKey, GeneralizedTimestamp, Ticket, TicketKey; +secret k: Function; + +const a, b, e: Agent; +const s: Server; + +/* give the intruder something to work with */ + +const ne: Nonce; +const kee: SessionKey; +untrusted e; +compromised k(e,s); + +protocol ksl(A,B,S) +{ + role A + { + const Na, Ma: Nonce; + var Nc, Mb: Nonce; + var T: Ticket; + var Kab: SessionKey; + + send_1(A,B, Na, A); + read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab ); + send_5(A,B, { Nc }Kab ); + + send_6(A,B, Ma,T ); + read_7(B,A, Mb,{Ma}Kab ); + send_8(A,B, {Mb}Kab ); + + claim_A1(A,Secret, Kab); + claim_A2(A,Niagree); + claim_A3(A,Nisynch); + } + + role B + { + var Na,Ma: Nonce; + const Nb,Nc,Mb: Nonce; + var Kab: SessionKey; + const Kbb: TicketKey; + const Tb: GeneralizedTimestamp; + var T: Ticket; + + read_1(A,B, Na, A); + send_2(B,S, Na, A, Nb, B ); + read_3(S,B, { Nb, A, Kab }k(B,S), T ); + send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab ); + read_5(A,B, { Nc }Kab ); + + read_6(A,B, Ma,{ Tb, A, Kab }Kbb ); + send_7(B,A, Mb,{Ma}Kab ); + read_8(A,B, {Mb}Kab ); + + claim_B1(B,Secret, Kab); + claim_B2(B,Niagree); + claim_B3(B,Nisynch); + } + + role S + { + var Na, Nb: Nonce; + const Kab: SessionKey; + + read_2(B,S, Na, A, Nb, B ); + send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) ); + } +} + +run ksl.A(a,b,s); +run ksl.B(a,b,s); +run ksl.S(a,b,s); + diff --git a/spdl/misc/localclaims-breaker.spdl b/spdl/misc/localclaims-breaker.spdl new file mode 100644 index 0000000..b54b315 --- /dev/null +++ b/spdl/misc/localclaims-breaker.spdl @@ -0,0 +1,56 @@ +/* + * Breaker for localclaims protocol + * + * Starts out as NSL3; last message (label3) has added name to avoid + * confusion with the later messages. + * + * Added messages labeled with x1 and x2 to allow for breaking the other + * protocol. + */ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol lcbreaker(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var x: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, {ni,nr,R}pk(I) ); + send_3(I,R, {nr,I}pk(R) ); + + read_x1(R,I, { x }pk(I) ); + send_x2(I,R, { x }ni ); + + claim_i1(I,Secret,ni); + claim_i2(I,Secret,nr); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + const x: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, {ni,nr,R}pk(I) ); + read_3(I,R, {nr,I}pk(R) ); + + send_x1(R,I, { x }pk(I) ); + read_x2(I,R, { x }ni ); + + claim_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + } +} + +const Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + diff --git a/spdl/misc/localclaims-seq1.spdl b/spdl/misc/localclaims-seq1.spdl new file mode 100644 index 0000000..16e5892 --- /dev/null +++ b/spdl/misc/localclaims-seq1.spdl @@ -0,0 +1,63 @@ +/* + * Breaker for localclaims protocol; sequential composition variant 1 + * + * Starts out as NSL3; last message (label3) has added name to avoid + * confusion with the later messages. + * + * Added messages labeled with x1 and x2 to allow for breaking the other + * protocol. + */ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol lcbreakerS1(I,R) +{ + role I + { + const ni,ni2: Nonce; + var nr: Nonce; + var x: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, {ni,nr,R}pk(I) ); + send_3(I,R, {nr,I}pk(R) ); + + read_x1(R,I, { x }pk(I) ); + send_x2(I,R, { x }ni ); + + send_lc(I,R, {ni2}pk(R) ); + + claim_i0(I,Secret,ni2); + claim_i1(I,Secret,ni); + claim_i2(I,Secret,nr); + } + + role R + { + var ni,ni2: Nonce; + const nr: Nonce; + const x: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, {ni,nr,R}pk(I) ); + read_3(I,R, {nr,I}pk(R) ); + + send_x1(R,I, { x }pk(I) ); + read_x2(I,R, { x }ni ); + + read_lc(I,R, {ni2}pk(R) ); + + claim_r0(R,Secret,ni2); + claim_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + } +} + +const Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + + diff --git a/spdl/misc/localclaims.spdl b/spdl/misc/localclaims.spdl new file mode 100644 index 0000000..8a27b30 --- /dev/null +++ b/spdl/misc/localclaims.spdl @@ -0,0 +1,45 @@ +/* + * Local claims + */ + +// PKI infrastructure + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +// The protocol description + +protocol localclaims(I,R) +{ + role I + { + const ni: Nonce; + + send_1(I,R, {ni}pk(R) ); + + claim_i1(I,Secret,ni); + } + + role R + { + var ni: Nonce; + + read_1(I,R, {ni}pk(R) ); + + claim_r1(R,Secret,ni); + } +} + +// The agents in the system + +const Alice,Bob: Agent; + +// An untrusted agent, with leaked information + +const Eve: Agent; +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + + diff --git a/spdl/misc/ns-symmetric-amended.spdl b/spdl/misc/ns-symmetric-amended.spdl new file mode 100644 index 0000000..9231c85 --- /dev/null +++ b/spdl/misc/ns-symmetric-amended.spdl @@ -0,0 +1,83 @@ +/* + * Needham-Schroeder symmetric + * Amended version (from Sjouke's interpret.) + */ + +/* symmetric */ + +usertype SessionKey; +secret k: Function; + +/* agents */ + +const a,b,e: Agent; + + +/* untrusted e */ + +untrusted e; +const ne: Nonce; +const kee: SessionKey; + +compromised k(e,e); +compromised k(e,a); +compromised k(e,b); +compromised k(a,e); +compromised k(b,e); + +/* {}x used for public (invertible) function modeling */ + +usertype PseudoFunction; +const succ: PseudoFunction; + +usertype Ticket; + +protocol nssymmetricamended(A,S,B) +{ + role A + { + const na: Nonce; + var T1: Ticket; + var T2: Ticket; + var kab: SessionKey; + var nb: Nonce; + + send_1(A,B, A ); + read_2(B,A, T1 ); + send_3(A,S, A,B,na,T1 ); + read_4(S,A, { na,B,kab,T2 }k(A,S) ); + send_5(A,B, T2 ); + read_6(B,A, { nb }kab ); + send_7(A,B, { {nb}succ }kab ); + + claim_8(A, Secret, kab); + claim_8a(A, Niagree); + claim_8b(A, Nisynch); + } + + role S + { + const kab: SessionKey; + var na: Nonce; + var nb: Nonce; + + read_3(A,S, A,B,na, { A,nb }k(B,S) ); + send_4(S,A, { na,B,kab, { kab,A }k(B,S) }k(A,S) ); + } + + role B + { + var kab: SessionKey; + const nb: Nonce; + + read_1(A,B, A ); + send_2(B,A, { A,nb }k(B,S) ); + read_5(A,B, { kab,A }k(B,S) ); + send_6(B,A, { nb }kab ); + read_7(A,B, { {nb}succ }kab ); + + claim_9(B, Secret, kab); + claim_9a(B, Niagree); + claim_9b(B, Nisynch); + } +} diff --git a/spdl/misc/ns-symmetric.spdl b/spdl/misc/ns-symmetric.spdl new file mode 100644 index 0000000..0eb0793 --- /dev/null +++ b/spdl/misc/ns-symmetric.spdl @@ -0,0 +1,72 @@ +/* + * Needham-Schroeder symmetric + */ + +/* symmetric */ + +usertype SessionKey; +secret k: Function; + +/* agents */ + +const a,b,e: Agent; + + +/* untrusted e */ + +untrusted e; +const ne: Nonce; +const kee: SessionKey; + +compromised k(e,e); +compromised k(e,a); +compromised k(e,b); +compromised k(a,e); +compromised k(b,e); + +/* {}x used for public (invertible) function modeling */ + +usertype PseudoFunction; +const succ: PseudoFunction; + +usertype Ticket; + +protocol nssymmetric(A,S,B) +{ + role A + { + const na: Nonce; + var T: Ticket; + var kab: SessionKey; + var nb: Nonce; + + send_1(A,S, A,B,na ); + read_2(S,A, { na,B,kab,T }k(A,S) ); + send_3(A,B, T ); + read_4(B,A, { nb }kab ); + send_5(A,B, { {nb}succ }kab ); + + claim_6(A, Secret, kab); + } + + role S + { + const kab: SessionKey; + var na: Nonce; + + read_1(A,S, A,B,na ); + send_2(S,A, { na,B,kab, { kab,A }k(B,S) }k(A,S) ); + } + + role B + { + var kab: SessionKey; + const nb: Nonce; + + read_3(A,B, { kab,A }k(B,S) ); + send_4(B,A, { nb }kab ); + read_5(A,B, { {nb}succ }kab ); + + claim_7(B, Secret, kab); + } +} diff --git a/spdl/misc/ns3-brutus.spdl b/spdl/misc/ns3-brutus.spdl new file mode 100644 index 0000000..b915956 --- /dev/null +++ b/spdl/misc/ns3-brutus.spdl @@ -0,0 +1,50 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol ns3brutus(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, {ni,nr}pk(I) ); + send_3(I,R, {nr}pk(R) ); + claim_4(I,Secret,nr); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, {ni,nr}pk(I) ); + read_3(I,R, {nr}pk(R) ); + claim_5(R,Secret,ni); + } +} + +const Alice,Bob,Eve : Agent; + +/* something like this will later on all be implied by 'untrusted Eve' */ + +untrusted Eve; +/* const nc: Nonce; */ +compromised sk(Eve); + +/* pre-defined 10 runs, limit using --max-runs parameters */ +/* to be nice to brutus, stupid scenario :( */ + +run ns3brutus.R(Agent,Bob); + run ns3brutus.I(Alice,Agent); +run ns3brutus.R(Agent,Bob); + run ns3brutus.I(Alice,Agent); +run ns3brutus.R(Agent,Bob); + run ns3brutus.I(Alice,Agent); +run ns3brutus.R(Agent,Bob); + run ns3brutus.I(Alice,Agent); +run ns3brutus.R(Agent,Bob); + run ns3brutus.I(Alice,Agent); diff --git a/spdl/misc/ns3.spdl b/spdl/misc/ns3.spdl new file mode 100644 index 0000000..44cb490 --- /dev/null +++ b/spdl/misc/ns3.spdl @@ -0,0 +1,67 @@ +/* + * Needham-Schroeder protocol + */ + +// PKI infrastructure + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +// The protocol description + +protocol ns3(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, {ni,nr}pk(I) ); + send_3(I,R, {nr}pk(R) ); + claim_i1(I,Secret,ni); + claim_i2(I,Secret,nr); + claim_i3(I,Niagree); + claim_i4(I,Nisynch); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, {ni,nr}pk(I) ); + read_3(I,R, {nr}pk(R) ); + claim_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + claim_r3(R,Niagree); + claim_r4(R,Nisynch); + } +} + +// The agents in the system + +const Alice,Bob: Agent; + +// An untrusted agent, with leaked information + +const Eve: Agent; +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + +// The runs (only needed for the modelchecker algorithm) + +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); +run ns3.I(Agent,Agent); +run ns3.R(Agent,Agent); + diff --git a/spdl/misc/nsl3-nisynch-rep.spdl b/spdl/misc/nsl3-nisynch-rep.spdl new file mode 100644 index 0000000..104c8b8 --- /dev/null +++ b/spdl/misc/nsl3-nisynch-rep.spdl @@ -0,0 +1,43 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol nsl3rep(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + send_6(I,R, {I,ni}pk(R) ); + read_2(R,I, {ni,nr,R}pk(I) ); + send_3(I,R, {nr}pk(R) ); + claim_4(I,Niagree); + claim_7(I,Nisynch); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + read_6(I,R, {I,ni}pk(R) ); + send_2(R,I, {ni,nr,R}pk(I) ); + read_3(I,R, {nr}pk(R) ); + claim_5(R,Niagree); + claim_8(R,Nisynch); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const nc: Nonce; +compromised sk(Eve); + +run nsl3rep.I(Agent,Agent); +run nsl3rep.R(Agent,Agent); +run nsl3rep.I(Agent,Agent); +run nsl3rep.R(Agent,Agent); diff --git a/spdl/misc/nsl3.spdl b/spdl/misc/nsl3.spdl new file mode 100644 index 0000000..874a439 --- /dev/null +++ b/spdl/misc/nsl3.spdl @@ -0,0 +1,43 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol nsl3(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, {ni,nr,R}pk(I) ); + send_3(I,R, {nr}pk(R) ); + + claim_i1(I,Secret,ni); + claim_i2(I,Secret,nr); + claim_i3(I,Niagree); + claim_i4(I,Nisynch); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, {ni,nr,R}pk(I) ); + read_3(I,R, {nr}pk(R) ); + + claim_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + claim_r3(R,Niagree); + claim_r4(R,Nisynch); + } +} + +const Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + diff --git a/spdl/misc/nsl7.spdl b/spdl/misc/nsl7.spdl new file mode 100644 index 0000000..452978f --- /dev/null +++ b/spdl/misc/nsl7.spdl @@ -0,0 +1,26 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol nsl7(I,R) +{ + role R + { + var ni; + const nr; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, {ni,nr,R}pk(I) ); + read_3(I,R, {nr}pk(R) ); + claim_4(R,Secret,ni); + claim_5(R,Secret,nr); + } +} + +const Alice,Bob,Eve; +const ne; +untrusted Eve; +compromised sk(Eve); + +run nsl7.R(Agent,Agent); +run nsl7.R(Agent,Agent); diff --git a/spdl/misc/onetrace.spdl b/spdl/misc/onetrace.spdl new file mode 100644 index 0000000..5901396 --- /dev/null +++ b/spdl/misc/onetrace.spdl @@ -0,0 +1,30 @@ +usertype String; + +const Alice,Bob,Charlie: Agent; +const Hallo: String; + +protocol onetrace(I) +{ + role I + { + var input: String; + + read_1(I,I, input); + send_2(I,I, Hallo); + read_3(I,I, input); + claim_4(I, Secret, input); + } +} + +run onetrace.I(Alice); +run onetrace.I(Alice); +run onetrace.I(Alice); +run onetrace.I(Alice); + +run onetrace.I(Alice); +run onetrace.I(Alice); +run onetrace.I(Alice); +run onetrace.I(Alice); + +run onetrace.I(Alice); +run onetrace.I(Alice); diff --git a/spdl/misc/otwayrees.spdl b/spdl/misc/otwayrees.spdl new file mode 100644 index 0000000..b26552a --- /dev/null +++ b/spdl/misc/otwayrees.spdl @@ -0,0 +1,66 @@ +secret const k : Function; + +/* Version from the Spore Librairy + http://www.lsv.ens-cachan.fr/spore/otwayRees.html +*/ + +usertype String, SesKey, Ticket, Server; + +protocol otwayrees(A,B,S) +{ + role A + { + const na : Nonce; + const M : String; + var kab : SesKey; + + send_1(A,B, M,A,B, { na,M,A,B }k(A,S) ); + read_4(B,A, M, { na,kab }k(A,S) ); + + claim_5(A, Secret,kab); + claim_5b(A, Niagree); + claim_5c(A, Nisynch); + } + + role B + { + var M : String; + const nb : Nonce; + var kab : SesKey; + var t1,t2; + + read_1(A,B, M,A,B, t1 ); + send_2(B,S, M,A,B, t1, { nb,M,A,B }k(B,S) ); + read_3(S,B, M, t2, { nb,kab }k(B,S) ); + send_4(B,A, M, t2 ); + + claim_6(B, Secret,kab); + claim_6a(B, Niagree); + claim_6b(B, Nisynch); + } + + role S + { + var na,nb : Nonce; + var M : String; + const kab : SesKey; + + read_2(B,S, M,A,B, { na,M,A,B }k(A,S), { nb,M,A,B }k(B,S) ); + send_3(S,B, M, { na,kab }k(A,S) , { nb,kab }k(B,S) ); + } +} + +const Alice, Bob, Eve: Agent; +const Simon: Server; + +untrusted Eve; +compromised k(Eve,Simon); + +run otwayrees.A(Alice, Agent, Simon); +run otwayrees.B(Agent, Bob, Simon); +run otwayrees.S(Agent, Agent, Simon); + +run otwayrees.A(Agent, Agent, Simon); +run otwayrees.B(Agent, Agent, Simon); +run otwayrees.S(Agent, Agent, Simon); + diff --git a/spdl/misc/protocol-list.txt b/spdl/misc/protocol-list.txt new file mode 100644 index 0000000..b395f33 --- /dev/null +++ b/spdl/misc/protocol-list.txt @@ -0,0 +1,52 @@ +# List of protocols to test +# +andrew-ban.spdl +andrew-lowe-ban.spdl +#bke-broken.spdl +#bke-one.spdl +#bkepk-ce2.spdl +#bkepk-ce.spdl +#bkepk.spdl +bke.spdl +#boyd.spdl +broken1.spdl +#carkey-broken-limited.spdl +#carkey-broken.spdl +carkey-ni2.spdl +carkey-ni.spdl +ccitt509-ban.spdl +denning-sacco-shared.spdl +five-run-bound.spdl +#gong-nonce-b.spdl +#gong-nonce.spdl +helloworld.spdl +isoiec11770-2-13.spdl +#kaochow-palm.spdl +kaochow.spdl +ns-symmetric.spdl +ns-symmetric-amended.spdl +ns3-brutus.spdl +ns3.spdl +nsl3-nisynch-rep.spdl +nsl3.spdl +nsl7.spdl +#onetrace.spdl +otwayrees.spdl +#samasc-broken.spdl +#simplest.spdl +#soph-keyexch.spdl +#soph.spdl +#speedtest.spdl +splice-as-hc-cj.spdl +#splice-as-hc.spdl +splice-as.spdl +#tls-paulson.spdl +tmn.spdl +#unknown2.spdl +wmf-brutus.spdl +woolam-ce.spdl +woolam-cmv.spdl +yahalom-ban.spdl +yahalom-lowe.spdl +yahalom-paulson.spdl +yahalom.spdl diff --git a/spdl/misc/samasc-broken.spdl b/spdl/misc/samasc-broken.spdl new file mode 100644 index 0000000..d97f7fd --- /dev/null +++ b/spdl/misc/samasc-broken.spdl @@ -0,0 +1,36 @@ +/* + Samasc broken +*/ + +usertype Key; + +const pk: Function; +secret sk: Function; + +inversekeys (pk,sk); + +protocol samascbroken(I,R) +{ + role R + { + const nr: Nonce; + var kir: Key; + + read_1a (I,R, { kir,I }pk(R) ); + send_1b (R,I, {nr,R}pk(I) ); + + /* Commenting out these two lines yields an attack: */ + read_2a (I,R, { nr }kir ); + send_2b (R,I, { I,R,nr }kir ); + + read_3 (I,R, { I,R }kir ); + + claim_4 (R, Secret, kir ); + } +} + +const a,b,e: Agent; + +untrusted e; +compromised sk(e); +const ne: Nonce; diff --git a/spdl/misc/simplest.spdl b/spdl/misc/simplest.spdl new file mode 100644 index 0000000..d96633f --- /dev/null +++ b/spdl/misc/simplest.spdl @@ -0,0 +1,20 @@ + +secret k: Nonce; +const Alice,Bob,Charlie: Agent; +const ne: Nonce; + +protocol simplest(I) +{ + role I + { + var x: Nonce; + const n: Nonce; + + read_1(I,I, x); + send_2(I,I, n, {n, x}k ); + claim_3(I, Secret, n); + } +} + +run simplest.I(Alice); +run simplest.I(Alice); diff --git a/spdl/misc/soph-keyexch.spdl b/spdl/misc/soph-keyexch.spdl new file mode 100644 index 0000000..611ba09 --- /dev/null +++ b/spdl/misc/soph-keyexch.spdl @@ -0,0 +1,39 @@ +usertype Sessionkey; +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol sophkx(I,R) +{ + role I + { + const ni: Nonce; + const kir: Sessionkey; + var nr: Nonce; + + send_1(I,R, ni, {I,kir}pk(R) ); + read_2(R,I, {ni}kir ); + claim_4(I,Secret,kir); + } + + role R + { + var ni: Nonce; + var kir: Sessionkey; + const nr: Nonce; + + read_1(I,R, ni, {I,kir}pk(R) ); + send_2(R,I, {ni}kir ); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const nc: Nonce; +const ke: Sessionkey; +compromised sk(Eve); + +run sophkx.I(Agent,Agent); +run sophkx.R(Agent,Agent); +run sophkx.I(Agent,Agent); diff --git a/spdl/misc/soph.spdl b/spdl/misc/soph.spdl new file mode 100644 index 0000000..174f9e1 --- /dev/null +++ b/spdl/misc/soph.spdl @@ -0,0 +1,34 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol soph(I,R) +{ + role I + { + const ni: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, ni ); + claim_3(I,Niagree); + } + + role R + { + var ni: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, ni ); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const nc: Nonce; +compromised sk(Eve); + +run soph.I(Agent,Agent); +run soph.R(Agent,Agent); +run soph.I(Agent,Agent); +run soph.R(Agent,Agent); diff --git a/spdl/misc/spdl-defaults.inc b/spdl/misc/spdl-defaults.inc new file mode 100644 index 0000000..c88b8de --- /dev/null +++ b/spdl/misc/spdl-defaults.inc @@ -0,0 +1,34 @@ +/* default includes */ + +/* asymmetric */ + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys (pk,sk); +inversekeys (hash,unhash); + + +/* symmetric */ + +usertype SessionKey; +secret k: Function; + +/* agents */ + +const A,B,E: Agent; + + +/* untrusted E */ + +untrusted E; +compromised sk(E); +const nE: Nonce; +const kEE: SessionKey; + +compromised k(E,E); +compromised k(E,A); +compromised k(E,B); +compromised k(A,E); +compromised k(B,E); + + diff --git a/spdl/misc/spdl-intruder.inc b/spdl/misc/spdl-intruder.inc new file mode 100644 index 0000000..14e1204 --- /dev/null +++ b/spdl/misc/spdl-intruder.inc @@ -0,0 +1,44 @@ + + +protocol myintruder (encr,decr,tupl,proj,m0) +{ + role encr + { + var R,X,Y: Ticket; + + read_e1 (R,encr, X); + read_e2 (R,encr, Y); + send_e3 (encr,R, {X}Y ); + } + + role decr + { + var R,X: Ticket; + + read_d1 (R,decr, {X}pk(E)); + send_d2 (decr,R, X ); + } + + role tupl + { + var R,X,Y: Ticket; + + read_t1 (R,tupl, X); + read_t2 (R,tupl, Y); + send_t3 (tupl,R, X,Y ); + } + + role proj + { + var R,X,Y: Ticket; + + read_p1 (R,proj, X,Y ); + send_p2 (proj,R, X ); + send_p3 (proj,R, Y ); + } + + singular role m0 + { + send_m0 (m0,m0, pk, pk(A), pk(B), nE, sk(E), E); + } +} diff --git a/spdl/misc/splice-as-hc-cj.spdl b/spdl/misc/splice-as-hc-cj.spdl new file mode 100644 index 0000000..1463e61 --- /dev/null +++ b/spdl/misc/splice-as-hc-cj.spdl @@ -0,0 +1,66 @@ +usertype TimeStamp, LifeTime; + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol spliceAShcCJ(C,AS,S) +{ + role C + { + const N1,N2: Nonce; + const T: TimeStamp; + const L: LifeTime; + + send_1(C,AS, C, S, N1 ); + read_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); + send_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) ); + read_6(S,C, S, C, {N2}pk(C) ); + + claim_7(C, Secret, N2); + claim_9(C, Niagree); + claim_10(C, Nisynch); + } + + role AS + { + var N1,N3: Nonce; + + read_1(C,AS, C, S, N1 ); + send_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); + read_4(S,AS, S, C, N3 ); + send_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) ); + } + + role S + { + const N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; + + var ni: Nonce; + const nr: Nonce; + + read_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) ); + send_4(S,AS, S, C, N3 ); + read_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) ); + send_6(S,C, S, C, {N2}pk(C) ); + + claim_8(S, Secret, N2); + claim_11(S, Niagree); + claim_12(S, Nisynch); + } +} + +const Al,Bo,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + +run spliceAShcCJ.C(Agent,Agent,Agent); +run spliceAShcCJ.AS(Agent,Agent,Agent); +run spliceAShcCJ.S(Agent,Agent,Agent); + + diff --git a/spdl/misc/splice-as-hc.spdl b/spdl/misc/splice-as-hc.spdl new file mode 100644 index 0000000..d2bf6d5 --- /dev/null +++ b/spdl/misc/splice-as-hc.spdl @@ -0,0 +1,66 @@ +usertype TimeStamp, LifeTime; + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol spliceAShc(C,AS,S) +{ + role C + { + const N1,N2: Nonce; + const T: TimeStamp; + const L: LifeTime; + + send_1(C,AS, C, S, N1 ); + read_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); + send_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); + read_6(S,C, S, C, {S, N2}pk(C) ); + + claim_7(C, Secret, N2); + claim_9(C, Niagree); + claim_10(C, Nisynch); + } + + role AS + { + var N1,N3: Nonce; + + read_1(C,AS, C, S, N1 ); + send_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); + read_4(S,AS, S, C, N3 ); + send_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) ); + } + + role S + { + const N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; + + var ni: Nonce; + const nr: Nonce; + + read_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); + send_4(S,AS, S, C, N3 ); + read_5(AS,S, AS, {AS, S, N3, C, pk(C)}sk(AS) ); + send_6(S,C, S, C, {S, N2}pk(C) ); + + claim_8(S, Secret, N2); + claim_11(S, Niagree); + claim_12(S, Nisynch); + } +} + +const Al,Bo,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + +run spliceAShc.C(Agent,Agent,Agent); +run spliceAShc.AS(Agent,Agent,Agent); +run spliceAShc.S(Agent,Agent,Agent); + + diff --git a/spdl/misc/splice-as.spdl b/spdl/misc/splice-as.spdl new file mode 100644 index 0000000..788cdca --- /dev/null +++ b/spdl/misc/splice-as.spdl @@ -0,0 +1,66 @@ +usertype TimeStamp, LifeTime; + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol spliceAS(C,AS,S) +{ + role C + { + const N1,N2: Nonce; + const T: TimeStamp; + const L: LifeTime; + + send_1(C,AS, C, S, N1 ); + read_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) ); + send_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); + read_6(S,C, S, C, {S, N2}pk(C) ); + + claim_7(C, Secret, N2); + claim_9(C, Niagree); + claim_10(C, Nisynch); + } + + role AS + { + var N1,N3: Nonce; + + read_1(C,AS, C, S, N1 ); + send_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) ); + read_4(S,AS, S, C, N3 ); + send_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) ); + } + + role S + { + const N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; + + var ni: Nonce; + const nr: Nonce; + + read_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); + send_4(S,AS, S, C, N3 ); + read_5(AS,S, AS, {AS, S, N3, pk(C)}sk(AS) ); + send_6(S,C, S, C, {S, N2}pk(C) ); + + claim_8(S, Secret, N2); + claim_11(S, Niagree); + claim_12(S, Nisynch); + } +} + +const Al,Bo,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +compromised sk(Eve); + +run spliceAS.C(Agent,Agent,Agent); +run spliceAS.AS(Agent,Agent,Agent); +run spliceAS.S(Agent,Agent,Agent); + + diff --git a/spdl/misc/tls-HSDDM05.cpp b/spdl/misc/tls-HSDDM05.cpp new file mode 100644 index 0000000..27c6787 --- /dev/null +++ b/spdl/misc/tls-HSDDM05.cpp @@ -0,0 +1,81 @@ +/* + * This is a model of a version of the TLS protocol as modeled by + * He,Sundararajan,Datta,Derek and Mitchell in the paper: "A modular + * correctness proof of IEEE 802.11i and TLS". + * + * The .cpp file cannot be fed into scyther directly; rather, one needs + * to type: (for *nix type systems with cpp) + * + * cpp tls-mitchell.cpp >tls-mitchell.spdl + * + * in order to generate a valid spdl file for the Scyther. + * + * This allows for macro expansion, as seen in the next part, which is + * particularly useful for expanding the handshakes. + * + */ +#define CERT(a) { a,pk(a) }sk(Terence) +#define handShake1 X,Nx,pa,Ny,pb,CERT(Y) +#define handShake2 handShake1,CERT(X),{ handShake1 }sk(X),{ msecret }pk(Y), hash(msecret, handShake1, clientstring) + +/* below is just Scyther input and no further macro definitions */ + +usertype Params, String; + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys(pk,sk); +inversekeys(hash,unhash); + +const clientstring,serverstring: String; + +const Alice, Bob, Eve: Agent; +const Terence: Agent; + +protocol tlsmitchell(X,Y) +{ + role X + { + const Nx: Nonce; + const msecret: Nonce; + const pa: Params; + var Ny: Nonce; + var pb: Params; + + send_1( X,Y, X,Nx,pa ); + read_2( Y,X, Ny,pb,CERT(Y) ); + send_3( X,Y, CERT(X), + { handShake1 }sk(X), + { msecret }pk(Y), + hash(msecret, handShake1, clientstring) + ); + read_4( Y,X, hash(msecret, handShake2, serverstring) ); + + claim_X1( X, Secret, msecret ); + } + + role Y + { + var Nx: Nonce; + var msecret: Nonce; + var pa: Params; + const Ny: Nonce; + const pb: Params; + + read_1( X,Y, X,Nx,pa ); + send_2( Y,X, Ny,pb,CERT(Y) ); + read_3( X,Y, CERT(X), + { handShake1 }sk(X), + { msecret }pk(Y), + hash(msecret, handShake1, clientstring) + ); + send_4( Y,X, hash(msecret, handShake2, serverstring) ); + + claim_Y1( Y, Secret, msecret ); + } +} + + +untrusted Eve; +compromised sk(Eve); + diff --git a/spdl/misc/tls-HSDDM05.spdl b/spdl/misc/tls-HSDDM05.spdl new file mode 100644 index 0000000..19c647b --- /dev/null +++ b/spdl/misc/tls-HSDDM05.spdl @@ -0,0 +1,63 @@ +# 1 "tls-HSDDM05.cpp" +# 1 "" +# 1 "" +# 1 "tls-HSDDM05.cpp" +# 23 "tls-HSDDM05.cpp" +usertype Params, String; + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys(pk,sk); +inversekeys(hash,unhash); + +const clientstring,serverstring: String; + +const Alice, Bob, Eve: Agent; +const Terence: Agent; + +protocol tlsmitchell(X,Y) +{ + role X + { + const Nx: Nonce; + const msecret: Nonce; + const pa: Params; + var Ny: Nonce; + var pb: Params; + + send_1( X,Y, X,Nx,pa ); + read_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); + send_3( X,Y, { X,pk(X) }sk(Terence), + { X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence) }sk(X), + { msecret }pk(Y), + hash(msecret, X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence), clientstring) + ); + read_4( Y,X, hash(msecret, X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{ X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence) }sk(X),{ msecret }pk(Y), hash(msecret, X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence), clientstring), serverstring) ); + + claim_X1( X, Secret, msecret ); + } + + role Y + { + var Nx: Nonce; + var msecret: Nonce; + var pa: Params; + const Ny: Nonce; + const pb: Params; + + read_1( X,Y, X,Nx,pa ); + send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); + read_3( X,Y, { X,pk(X) }sk(Terence), + { X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence) }sk(X), + { msecret }pk(Y), + hash(msecret, X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence), clientstring) + ); + send_4( Y,X, hash(msecret, X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence),{ X,pk(X) }sk(Terence),{ X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence) }sk(X),{ msecret }pk(Y), hash(msecret, X,Nx,pa,Ny,pb,{ Y,pk(Y) }sk(Terence), clientstring), serverstring) ); + + claim_Y1( Y, Secret, msecret ); + } +} + + +untrusted Eve; +compromised sk(Eve); diff --git a/spdl/misc/tls-paulson-avispa.cpp b/spdl/misc/tls-paulson-avispa.cpp new file mode 100644 index 0000000..0fa2389 --- /dev/null +++ b/spdl/misc/tls-paulson-avispa.cpp @@ -0,0 +1,96 @@ +/* + * This is a model of the TLS version as modeled by Paulson + * + * Slightly modified to correspond exactly to the version in the Avispa + * repository by Paul Hankes Drielsma. + * + * The .cpp file cannot be fed into scyther directly; rather, one needs + * to type: + * + * cpp tls-paulson.cpp >tls-paulson.spdl + * + * in order to generate a valid spdl file for scyther. + * + * This allows for macro expansion, as seen in the next part. + * + */ + +#define CERT(a) { a,pk(a) }sk(Terence) +#define MSG a,na,sid,pa,pb,nb,sid,pb,CERT(a),CERT(b),{pms}pk(b) +#define M hash(pms,na,nb) +#define F hash(M,MSG) +#define CLIENTK keygen(a,na,nb,M) +#define SERVERK keygen(b,na,nb,M) + +usertype Params, Bool, SessionID; + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys(pk,sk); +inversekeys(hash,unhash); + +const keygen: Function; +secret unkeygen: Function; +inversekeys(keygen, unkeygen); + +const pa,pb: Params; +const Terence: Agent; +const false,true: Bool; + + +protocol tlspaulson-avispa(a,b) +{ + role a + { + const na: Nonce; + const sid: SessionID; + const pms: Nonce; + var nb: Nonce; + var pb: Params; + + send_1( a,b, a,na,sid,pa ); + read_2( b,a, nb,sid,pb ); + read_3( b,a, CERT(b) ); + send_4( a,b, CERT(a) ); + send_5( a,b, { pms }pk(b) ); + send_6( a,b, { hash(nb,b,pms) }sk(a) ); + send_7( a,b, { F }CLIENTK ); + read_8( b,a, { F }SERVERK ); + + claim_9a(a, Secret, SERVERK); + claim_9b(a, Secret, CLIENTK); + claim_9c(a, Niagree); + + } + + role b + { + var na: Nonce; + var sid: SessionID; + var pms: Nonce; + const nb: Nonce; + const pb: Params; + + read_1( a,b, a,na,sid,pa ); + send_2( b,a, nb,sid,pb ); + send_3( b,a, CERT(b) ); + read_4( a,b, CERT(a) ); + read_5( a,b, { pms }pk(b) ); + read_6( a,b, { hash(nb,b,pms) }sk(a) ); + read_7( a,b, { F }CLIENTK ); + send_8( b,a, { F }SERVERK ); + + claim_10a(b, Secret, SERVERK); + claim_10b(b, Secret, CLIENTK); + claim_10c(b, Niagree); + } +} + +const Alice, Bob, Eve: Agent; + +untrusted Eve; +compromised sk(Eve); +const ne: Nonce; +const side: SessionID; +const pe: Params; + diff --git a/spdl/misc/tls-paulson-avispa.spdl b/spdl/misc/tls-paulson-avispa.spdl new file mode 100644 index 0000000..5fc352d --- /dev/null +++ b/spdl/misc/tls-paulson-avispa.spdl @@ -0,0 +1,76 @@ +# 1 "tls-paulson-avispa.cpp" +# 1 "" +# 1 "" +# 1 "tls-paulson-avispa.cpp" +# 25 "tls-paulson-avispa.cpp" +usertype Params, Bool, SessionID; + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys(pk,sk); +inversekeys(hash,unhash); + +const keygen: Function; +secret unkeygen: Function; +inversekeys(keygen, unkeygen); + +const pa,pb: Params; +const Terence: Agent; +const false,true: Bool; + + +protocol tlspaulson-avispa(a,b) +{ + role a + { + const na: Nonce; + const sid: SessionID; + const pms: Nonce; + var nb: Nonce; + var pb: Params; + + send_1( a,b, a,na,sid,pa ); + read_2( b,a, nb,sid,pb ); + read_3( b,a, { b,pk(b) }sk(Terence) ); + send_4( a,b, { a,pk(a) }sk(Terence) ); + send_5( a,b, { pms }pk(b) ); + send_6( a,b, { hash(nb,b,pms) }sk(a) ); + send_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(a,na,nb,hash(pms,na,nb)) ); + read_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(b,na,nb,hash(pms,na,nb)) ); + + claim_9a(a, Secret, keygen(b,na,nb,hash(pms,na,nb))); + claim_9b(a, Secret, keygen(a,na,nb,hash(pms,na,nb))); + claim_9c(a, Niagree); + + } + + role b + { + var na: Nonce; + var sid: SessionID; + var pms: Nonce; + const nb: Nonce; + const pb: Params; + + read_1( a,b, a,na,sid,pa ); + send_2( b,a, nb,sid,pb ); + send_3( b,a, { b,pk(b) }sk(Terence) ); + read_4( a,b, { a,pk(a) }sk(Terence) ); + read_5( a,b, { pms }pk(b) ); + read_6( a,b, { hash(nb,b,pms) }sk(a) ); + read_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(a,na,nb,hash(pms,na,nb)) ); + send_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }keygen(b,na,nb,hash(pms,na,nb)) ); + + claim_10a(b, Secret, keygen(b,na,nb,hash(pms,na,nb))); + claim_10b(b, Secret, keygen(a,na,nb,hash(pms,na,nb))); + claim_10c(b, Niagree); + } +} + +const Alice, Bob, Eve: Agent; + +untrusted Eve; +compromised sk(Eve); +const ne: Nonce; +const side: SessionID; +const pe: Params; diff --git a/spdl/misc/tls-paulson.cpp b/spdl/misc/tls-paulson.cpp new file mode 100644 index 0000000..5d0369e --- /dev/null +++ b/spdl/misc/tls-paulson.cpp @@ -0,0 +1,95 @@ +/* + * This is a model of the TLS version as modeled by Paulson + * + * The .cpp file cannot be fed into scyther directly; rather, one needs + * to type: + * + * cpp tls-paulson.cpp >tls-paulson.spdl + * + * in order to generate a valid spdl file for scyther. + * + * This allows for macro expansion, as seen in the next part. + * + */ +#define CERT(a) { a,pk(a) }sk(Terence) +#define MSG a,na,sid,pa,pb,nb,sid,pb,CERT(a),CERT(b),{pms}pk(b) +#define M hash(pms,na,nb) +#define F hash(M,MSG) +#define CLIENTK hash(sid,M,na,pa,a,nb,pb,b,false) +#define SERVERK hash(sid,M,na,pa,a,nb,pb,b,true) + +usertype Params, Bool, SessionID; + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys(pk,sk); +inversekeys(hash,unhash); + +const pa,pb: Params; +const Terence: Agent; +const false,true: Bool; + + +protocol tlspaulson(a,b) +{ + role a + { + const na: Nonce; + const sid: SessionID; + const pms: Nonce; + var nb: Nonce; + var pb: Params; + + send_1( a,b, a,na,sid,pa ); + read_2( b,a, nb,sid,pb ); + read_3( b,a, CERT(b) ); + send_4( a,b, CERT(a) ); + send_5( a,b, { pms }pk(b) ); + send_6( a,b, { hash(nb,b,pms) }sk(a) ); + send_7( a,b, { F }CLIENTK ); + read_8( b,a, { F }SERVERK ); + + claim_9a(a, Secret, SERVERK); + claim_9b(a, Secret, CLIENTK); + + } + + role b + { + var na: Nonce; + var sid: SessionID; + var pms: Nonce; + const nb: Nonce; + const pb: Params; + + read_1( a,b, a,na,sid,pa ); + send_2( b,a, nb,sid,pb ); + send_3( b,a, CERT(b) ); + read_4( a,b, CERT(a) ); + read_5( a,b, { pms }pk(b) ); + read_6( a,b, { hash(nb,b,pms) }sk(a) ); + read_7( a,b, { F }CLIENTK ); + send_8( b,a, { F }SERVERK ); + + claim_10a(b, Secret, SERVERK); + claim_10b(b, Secret, CLIENTK); + } +} + +const Alice, Bob, Eve: Agent; + +untrusted Eve; +compromised sk(Eve); +const ne: Nonce; +const side: SessionID; +const pe: Params; + +run tlspaulson.a(Agent,Agent); +run tlspaulson.b(Agent,Agent); +run tlspaulson.a(Agent,Agent); +run tlspaulson.b(Agent,Agent); +run tlspaulson.a(Agent,Agent); +run tlspaulson.b(Agent,Agent); +run tlspaulson.a(Agent,Agent); +run tlspaulson.b(Agent,Agent); + diff --git a/spdl/misc/tls-paulson.spdl b/spdl/misc/tls-paulson.spdl new file mode 100644 index 0000000..d750c36 --- /dev/null +++ b/spdl/misc/tls-paulson.spdl @@ -0,0 +1,79 @@ +# 1 "tls-paulson.cpp" +# 1 "" +# 1 "" +# 1 "tls-paulson.cpp" +# 21 "tls-paulson.cpp" +usertype Params, Bool, SessionID; + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys(pk,sk); +inversekeys(hash,unhash); + +const pa,pb: Params; +const Terence: Agent; +const false,true: Bool; + + +protocol tlspaulson(a,b) +{ + role a + { + const na: Nonce; + const sid: SessionID; + const pms: Nonce; + var nb: Nonce; + var pb: Params; + + send_1( a,b, a,na,sid,pa ); + read_2( b,a, nb,sid,pb ); + read_3( b,a, { b,pk(b) }sk(Terence) ); + send_4( a,b, { a,pk(a) }sk(Terence) ); + send_5( a,b, { pms }pk(b) ); + send_6( a,b, { hash(nb,b,pms) }sk(a) ); + send_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) ); + read_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) ); + + claim_9a(a, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true)); + claim_9b(a, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false)); + + } + + role b + { + var na: Nonce; + var sid: SessionID; + var pms: Nonce; + const nb: Nonce; + const pb: Params; + + read_1( a,b, a,na,sid,pa ); + send_2( b,a, nb,sid,pb ); + send_3( b,a, { b,pk(b) }sk(Terence) ); + read_4( a,b, { a,pk(a) }sk(Terence) ); + read_5( a,b, { pms }pk(b) ); + read_6( a,b, { hash(nb,b,pms) }sk(a) ); + read_7( a,b, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false) ); + send_8( b,a, { hash(hash(pms,na,nb),a,na,sid,pa,pb,nb,sid,pb,{ a,pk(a) }sk(Terence),{ b,pk(b) }sk(Terence),{pms}pk(b)) }hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true) ); + + claim_10a(b, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,true)); + claim_10b(b, Secret, hash(sid,hash(pms,na,nb),na,pa,a,nb,pb,b,false)); + } +} + +const Alice, Bob, Eve: Agent; + +untrusted Eve; +compromised sk(Eve); +const ne: Nonce; +const side: SessionID; +const pe: Params; + +run tlspaulson.a(Agent,Agent); +run tlspaulson.b(Agent,Agent); +run tlspaulson.a(Agent,Agent); +run tlspaulson.b(Agent,Agent); +run tlspaulson.a(Agent,Agent); +run tlspaulson.b(Agent,Agent); +run tlspaulson.a(Agent,Agent); +run tlspaulson.b(Agent,Agent); diff --git a/spdl/misc/tmn-Gijs.spdl b/spdl/misc/tmn-Gijs.spdl new file mode 100644 index 0000000..b9179cf --- /dev/null +++ b/spdl/misc/tmn-Gijs.spdl @@ -0,0 +1,56 @@ + +usertype Key; + +const pk: Function; +secret sk: Function; +inversekeys(pk,sk); + +protocol tmn(A,B,S) +{ + role A + { + const Ka: Key; + var Kb: Key; + + send_1(A,S, B,{Ka}pk(S) ); + read_4(S,A, B,{Kb}Ka ); + + #claim_5(A,Secret,Ka); + #claim_8(A,Secret,Kb); + } + + role B + { + const Kb: Key; + + read_2(S,B, A ); + send_3(B,S, A, { Kb }pk(S) ); + + claim_6(B,Secret,Kb); + } + + role S + { + var Ka,Kb: Key; + + read_1(A,S, B,{Ka}pk(S) ); + send_2(S,B, A ); + read_3(B,S, A, { Kb }pk(S) ); + send_4(S,A, B,{Kb}Ka ); + + #claim_7(S,Secret,Ka); + } +} + +const Alice,Bob,Eve,Simon: Agent; +const Ke: Key; + + +untrusted Eve; +compromised sk(Eve); + +# Scenario to recreate an attack in SPORE +run tmn.B (Alice,Bob,Simon); +run tmn.S (Alice,Bob,Simon); + + diff --git a/spdl/misc/tmn.spdl b/spdl/misc/tmn.spdl new file mode 100644 index 0000000..bdd0dab --- /dev/null +++ b/spdl/misc/tmn.spdl @@ -0,0 +1,56 @@ +usertype Key; + +const pk: Function; +secret sk: Function; +inversekeys(pk,sk); + +protocol tmn(A,B,S) +{ + role A + { + const Ka: Key; + var Kb: Key; + + send_1(A,S, B,{Ka}pk(S) ); + read_4(S,A, B,{Kb}Ka ); + + claim_5(A,Secret,Ka); + claim_8(A,Secret,Kb); + } + + role B + { + const Kb: Key; + + read_2(S,B, A ); + send_3(B,S, A, { Kb }pk(S) ); + + claim_6(B,Secret,Kb); + } + + role S + { + var Ka,Kb: Key; + + read_1(A,S, B,{Ka}pk(S) ); + send_2(S,B, A ); + read_3(B,S, A, { Kb }pk(S) ); + send_4(S,A, B,{Kb}Ka ); + + claim_7(S,Secret,Ka); + } +} + +const Alice,Bob,Eve,Simon: Agent; + +untrusted Eve; +compromised sk(Eve); + +run tmn.A (Agent,Agent,Simon); +run tmn.A (Agent,Agent,Simon); +run tmn.B (Agent,Agent,Simon); +run tmn.B (Agent,Agent,Simon); +run tmn.S (Agent,Agent,Simon); +run tmn.S (Agent,Agent,Simon); + + diff --git a/spdl/misc/unknown2.spdl b/spdl/misc/unknown2.spdl new file mode 100644 index 0000000..acfefcb --- /dev/null +++ b/spdl/misc/unknown2.spdl @@ -0,0 +1,69 @@ +usertype SessionKey; +secret k: Function; + +protocol unknown2(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: SessionKey; + var T; + + send_1(I,R, ni ); + read_3(S,I, { I,R,kir,ni,nr }k(I,S), T ); + send_4(I,R, T, {nr}kir ); + + claim_i1(I,Nisynch); + claim_i2(I,Niagree); + claim_i3(I,Secret, kir); + } + + role R + { + const nr: Nonce; + var ni: Nonce; + var kir: SessionKey; + + read_1(I,R, ni ); + send_2(R,S, { I,R,ni,nr }k(R,S) ); + read_4(I,R, { I,R,kir,ni,nr }k(R,S), {nr}kir ); + + claim_r1(R,Nisynch); + claim_r2(R,Niagree); + claim_r3(R,Secret, kir); + } + + role S + { + const kir: SessionKey; + var ni,nr: Nonce; + + read_2(R,S, { I,R,ni,nr }k(R,S) ); + send_3(S,I, { I,R,kir,ni,nr }k(I,S), { I,R,kir,ni,nr }k(R,S) ); + +/* + claim_s1(S,Nisynch); + claim_s2(S,Niagree); + claim_s3(S,Secret, kir); + */ + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const kee: SessionKey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Alice,Eve); +compromised k(Bob,Eve); + +run unknown2.I(Agent,Agent,Agent); +run unknown2.R(Agent,Agent,Agent); +run unknown2.S(Agent,Agent,Agent); +run unknown2.R(Agent,Agent,Agent); +run unknown2.I(Agent,Agent,Agent); +run unknown2.S(Agent,Agent,Agent); diff --git a/spdl/misc/wmf-brutus.spdl b/spdl/misc/wmf-brutus.spdl new file mode 100644 index 0000000..a68c7ac --- /dev/null +++ b/spdl/misc/wmf-brutus.spdl @@ -0,0 +1,48 @@ +usertype SesKey, Server; +secret const k : Function; + +/* Version from the Brutus reports +*/ + +protocol wmfbrutus(A,B,S) +{ + role A + { + const kab : SesKey; + + send_1(A,S, A, { B,kab }k(A,S) ); + } + + role B + { + var kab : SesKey; + + read_2(S,B, { A, kab }k(B,S) ); + + claim_3(B, Secret,kab); + } + + role S + { + var kab : SesKey; + + read_1(A,S, A, { B,kab }k(A,S) ); + send_2(S,B, { A, kab }k(B,S) ); + } +} + +const Alice, Bob, Eve: Agent; +const Simon: Server; + +untrusted Eve; +compromised k(Eve,Simon); + +run wmfbrutus.A(Agent, Agent, Simon); +run wmfbrutus.B(Agent, Agent, Simon); +run wmfbrutus.A(Agent, Agent, Simon); +run wmfbrutus.B(Agent, Agent, Simon); +run wmfbrutus.A(Agent, Agent, Simon); +run wmfbrutus.B(Agent, Agent, Simon); + +run wmfbrutus.S(Agent, Agent, Simon); + diff --git a/spdl/misc/woolam-ce.spdl b/spdl/misc/woolam-ce.spdl new file mode 100644 index 0000000..5bbcc65 --- /dev/null +++ b/spdl/misc/woolam-ce.spdl @@ -0,0 +1,38 @@ +usertype Server, SessionKey, Token, SymmetricKey; +secret k: Function; + +const Alice, Bob, Charlie, Eve: Agent; +const Simon: Server; + +/* give the intruder something to work with */ +const ne: Nonce; +const ke: SessionKey; +untrusted Eve; +compromised k(Eve,Simon); + +const authToken: Token; + +protocol woolamce(A,B,S) +{ + role B + { + var Na: Nonce; + const Nb: Nonce; + var Kab: SessionKey; + var Kas : SymmetricKey; + + read_1(A,B, A,Na); + send_2(B,A, B,Nb); + read_3(A,B, { A,(B,(Na,Nb)) }Kas ); + send_4(B,S, { A,(B,(Na,Nb)) }Kas, { A,(B,(Na,Nb)) }k(B,S) ); + read_5(S,B, { B,(Na,(Nb,Kab)) }Kas, { A,(Na,(Nb,Kab)) }k(B,S) ); + send_6(B,A, { B,(Na,(Nb,Kab)) }Kas, { Na,Nb }Kab ); + read_7(A,B, { Nb }Kab ); + + claim_8(B,Secret,authToken); + } +} + +run woolamce.B(Agent,Agent,Simon); +run woolamce.B(Agent,Agent,Simon); + diff --git a/spdl/misc/woolam-cmv.spdl b/spdl/misc/woolam-cmv.spdl new file mode 100644 index 0000000..b20aeda --- /dev/null +++ b/spdl/misc/woolam-cmv.spdl @@ -0,0 +1,75 @@ +/* + * Woo-lam version from Spore, as it is in Sjouke's list + */ + +usertype Server, SessionKey, Token, Ticket; +secret k: Function; + +const Alice, Bob, Charlie, Eve: Agent; +const Simon: Server; + +/* give the intruder something to work with */ +// Scyther finds an attack using basic type flaws + +const ne: Nonce; +const ke: SessionKey; +untrusted Eve; +compromised k(Eve,Simon); + +const authToken: Token; + +protocol woolamcmv(A,B,S) +{ + role A + { + const Na: Nonce; + var Nb: Nonce; + var Kab: SessionKey; + var t1,t2; + + send_1(A,B, A,Na); + read_2(B,A, B,Nb); + send_3(A,B, { A,B, Na,Nb }k(A,S) ); + read_6(B,A, { B,Na,Nb,Kab }k(A,S), { Na,Nb }Kab ); + send_7(A,B, { Nb }Kab ); + + claim_8(A,Secret, Kab); + claim_9(A,Niagree); + claim_10(A,Nisynch); + } + + role B + { + var Na: Nonce; + const Nb: Nonce; + var Kab: SessionKey; + var t1,t2; + + read_1(A,B, A,Na); + send_2(B,A, B,Nb); + read_3(A,B, t1 ); + send_4(B,S, t1, { A,B,Na,Nb }k(B,S) ); + read_5(S,B, t2, { A,Na,Nb,Kab }k(B,S) ); + send_6(B,A, t2, { Na,Nb }Kab ); + read_7(A,B, { Nb }Kab ); + + claim_11(B,Secret, Kab); + claim_12(B,Niagree); + claim_13(B,Nisynch); + } + + role S + { + var Na, Nb: Nonce; + const Kab: SessionKey; + + read_4(B,S, { A,B, Na,Nb }k(A,S), { A,B,Na,Nb }k(B,S) ); + send_5(S,B, { B,Na,Nb,Kab }k(A,S), { A,Na,Nb,Kab }k(B,S) ); + + claim_14(S,Secret, Kab); + } +} + +run woolamcmv.B(Alice,Bob,Simon); +run woolamcmv.B(Alice,Bob,Simon); + diff --git a/spdl/misc/woolam-pi-f.spdl b/spdl/misc/woolam-pi-f.spdl new file mode 100644 index 0000000..20145da --- /dev/null +++ b/spdl/misc/woolam-pi-f.spdl @@ -0,0 +1,55 @@ +/* + * Woo-lam version from Spore, Pi f + * + * Only one-way verification version + */ + +usertype Server, SessionKey, Ticket; +secret k: Function; + +const Alice, Bob, Charlie, Eve: Agent; +const Simon: Server; + +const ne: Nonce; +const ke: SessionKey; +untrusted Eve; +compromised k(Eve,Simon); + +protocol woolampif(A,B,S) +{ + role A + { + var Nb: Nonce; + + send_1(A,B, A); + read_2(B,A, Nb); + send_3(A,B, { A,B,Nb }k(A,S) ); + } + + role B + { + const Nb: Nonce; + var T: Ticket; + + read_1(A,B, A); + send_2(B,A, Nb); + read_3(A,B, T); + send_4(B,S, { A,B,Nb, T }k(B,S) ); + read_5(S,B, { A,B,Nb }k(B,S) ); + + claim_6(B,Niagree); + claim_7(B,Nisynch); + } + + role S + { + var Nb: Nonce; + + read_4(B,S, { A,B,Nb, { A,B,Nb }k(A,S) }k(B,S) ); + send_5(S,B, { A,B,Nb }k(B,S) ); + } +} + +run woolampif.B(Alice,Bob,Simon); +run woolampif.B(Alice,Bob,Simon); + diff --git a/spdl/misc/yahalom-ban.spdl b/spdl/misc/yahalom-ban.spdl new file mode 100644 index 0000000..b3ee2cd --- /dev/null +++ b/spdl/misc/yahalom-ban.spdl @@ -0,0 +1,51 @@ +// BAN modified version of the yahalom protocol +// Type flaw +// This version actually works! + +usertype Server; + +const a,b,c : Agent; +const s : Server; +secret k : Function; + + + + +protocol yahalomBan(A,B,S) +{ + role A + { + const na; + var nb; + var ticket; + var kab; + + send_1(A,B, A,na); + read_3(S,A, nb, {B,kab,na}k(A,S), ticket ); + send_4(A,B, ticket, {nb}kab ); + claim_5(A, Secret,kab); + } + + role B + { + const nb; + var na; + var ticket; + var kab; + + read_1(A,B, A,na); + send_2(B,S, B,nb, {A,na}k(B,S) ); + read_4(A,B, {A,kab,nb}k(B,S) , {nb}kab ); + claim_6(B, Secret,kab); + } + + role S + { + const kab; + var na,nb; + + read_2(B,S, B,nb, {A,na}k(B,S) ); + send_3(S,A, nb, {B,kab,na}k(A,S), {A,kab,nb}k(B,S) ); + } +} + diff --git a/spdl/misc/yahalom-lowe.spdl b/spdl/misc/yahalom-lowe.spdl new file mode 100644 index 0000000..dc6251b --- /dev/null +++ b/spdl/misc/yahalom-lowe.spdl @@ -0,0 +1,65 @@ +/* + * Yahalom Lowe + * As in Sjouke's list + */ + +usertype Sessionkey; + +const Alice,Bob,Simon,Eve : Agent; +secret k : Function; + +untrusted Eve; +compromised k(Eve,Simon); +const ne: Nonce; +const kee: Sessionkey; + +protocol yahalomlowe(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Sessionkey; + + send_1(I,R, I,ni); + read_3(S,I, {R,kir,ni,nr}k(I,S) ); + send_5(I,R, {I,R,S,nr}kir ); + + claim_8(I, Secret,kir); + claim_9(I, Niagree); + claim_10(I, Nisynch); + } + + role R + { + const nr: Nonce; + var ni: Nonce; + var kir: Sessionkey; + + read_1(I,R, I,ni); + send_2(R,S, {I,ni,nr}k(R,S) ); + read_4(S,R, {I,kir}k(R,S) ); + read_5(I,R, {I,R,S,nr}kir ); + claim_11(R, Secret,kir); + claim_12(R, Nisynch); + claim_13(R, Niagree); + } + + role S + { + const kir: Sessionkey; + var ni,nr: Nonce; + + read_2(R,S, {I,ni,nr}k(R,S) ); + send_3(S,I, {R,kir,ni,nr}k(I,S) ); + send_4(S,R, {I,kir}k(R,S) ); + } +} + +run yahalomlowe.I(Agent,Agent,Simon); +run yahalomlowe.R(Agent,Agent,Simon); +run yahalomlowe.S(Agent,Agent,Simon); + +run yahalomlowe.I(Agent,Agent,Simon); +run yahalomlowe.R(Agent,Agent,Simon); + diff --git a/spdl/misc/yahalom-paulson.spdl b/spdl/misc/yahalom-paulson.spdl new file mode 100644 index 0000000..282c02a --- /dev/null +++ b/spdl/misc/yahalom-paulson.spdl @@ -0,0 +1,65 @@ +/* + * Yahalom Paulson-strengthened + * As in Sjouke's list + */ + +usertype Sessionkey, Ticket; + +const Alice,Bob,Simon,Eve : Agent; +secret k : Function; + +untrusted Eve; +compromised k(Eve,Simon); +const ne: Nonce; +const kee: Sessionkey; + +protocol yahalompaulson(I,R,S) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + var kir: Sessionkey; + var T: Ticket; + + send_1(I,R, I,ni); + read_3(S,I, nr, {R,kir,ni}k(I,S), T ); + send_4(I,R, T, {nr}kir ); + + claim_8(I, Secret,kir); + claim_9(I, Nisynch); + claim_10(I, Niagree); + } + + role R + { + const nr: Nonce; + var ni: Nonce; + var kir: Sessionkey; + + read_1(I,R, I,ni); + send_2(R,S, R,nr,{I,ni}k(R,S) ); + read_4(I,R, {I,R,kir,nr}k(R,S), {nr}kir ); + + claim_11(R, Secret,kir); + claim_12(R, Nisynch); + claim_13(R, Niagree); + } + + role S + { + const kir: Sessionkey; + var ni,nr: Nonce; + + read_2(R,S, R,nr, {I,ni}k(R,S) ); + send_3(S,I, nr, { R,kir,ni }k(I,S), {I,R,kir,nr}k(R,S) ); + } +} + +run yahalompaulson.I(Agent,Agent,Simon); +run yahalompaulson.R(Agent,Agent,Simon); +run yahalompaulson.S(Agent,Agent,Simon); + +run yahalompaulson.I(Agent,Agent,Simon); +run yahalompaulson.R(Agent,Agent,Simon); + diff --git a/spdl/misc/yahalom.spdl b/spdl/misc/yahalom.spdl new file mode 100644 index 0000000..5b62b62 --- /dev/null +++ b/spdl/misc/yahalom.spdl @@ -0,0 +1,54 @@ +// Yahalom protocol + +const a,b,s : Agent; +secret k : Function; + +usertype Nonce, Ticket, SessionKey; + + +protocol yahalom(A,B,S) +{ + role A + { + const na: Nonce; + var nb: Nonce; + var ticket: Ticket; + var kab: SessionKey; + + send_1(A,B, A,na); + read_3(S,A, nb, {B,kab,na,nb}k(A,S), ticket ); + send_4(A,B, ticket, {nb}kab ); + + claim_5(A, Secret,kab); + } + + role B + { + const nb: Nonce; + var na: Nonce; + var ticket: Ticket; + var kab: SessionKey; + + read_1(A,B, A,na); + send_2(B,S, B,nb, {A,na,nb}k(B,S) ); + read_4(A,B, {A,kab}k(B,S) , {nb}kab ); + + claim_6(B, Secret,kab); + } + + role S + { + const kab: SessionKey; + var na,nb: Nonce; + + read_2(B,S, B,nb, {A,na}k(B,S) ); + send_3(S,A, nb, {B,kab,na,nb}k(A,S), {A,kab}k(B,S) ); + } +} + +run yahalom.A(Agent,Agent,s); +run yahalom.A(Agent,Agent,s); +run yahalom.B(Agent,Agent,s); +run yahalom.B(Agent,Agent,s); +run yahalom.S(Agent,Agent,s); + diff --git a/spdl/multiparty/heuristics-results.txt b/spdl/multiparty/heuristics-results.txt new file mode 100644 index 0000000..cc55c31 --- /dev/null +++ b/spdl/multiparty/heuristics-results.txt @@ -0,0 +1,776 @@ +Slave1:multiparty% ./test-heuristics.py +Starting with [11, 15] +Testing using P 3 and 5 runs. +Testing protocol 11. +Heuristic 0: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=0 --timer=20 +states 7488 +attack NoClaim +time 2.007e+01 +st/sec 3.731e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 1: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=1 --timer=20 +states 3869 +attack NoClaim +time 2.004e+01 +st/sec 1.931e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 2: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=2 --timer=20 +states 6543 +attack NoClaim +time 2.006e+01 +st/sec 3.262e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 3: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=3 --timer=20 +states 9003 +attack NoClaim +time 2.005e+01 +st/sec 4.490e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 1 correct: bounded_proof +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 4: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=4 --timer=20 +states 6375 +attack NoClaim +time 2.008e+01 +st/sec 3.175e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 5: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=5 --timer=20 +states 4282 +attack NoClaim +time 2.007e+01 +st/sec 2.134e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 4 correct: bounded_proof time=20 +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 6: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=6 --timer=20 +states 6791 +attack NoClaim +time 2.002e+01 +st/sec 3.392e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 7: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=7 --timer=20 +states 8115 +attack NoClaim +time 2.004e+01 +st/sec 4.049e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 14 correct: bounded_proof time=20 +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 8: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=8 --timer=20 +states 9649 +attack NoClaim +time 2.003e+01 +st/sec 4.817e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 9: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=9 --timer=20 +states 3873 +attack NoClaim +time 2.005e+01 +st/sec 1.932e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 10: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=10 --timer=20 +states 11954 +attack NoClaim +time 2.007e+01 +st/sec 5.956e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 11: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=11 --timer=20 +states 7367 +attack NoClaim +time 2.003e+01 +st/sec 3.678e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 12: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=12 --timer=20 +states 6271 +attack NoClaim +time 2.005e+01 +st/sec 3.128e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 13: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=13 --timer=20 +states 4729 +attack NoClaim +time 2.006e+01 +st/sec 2.357e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 14: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=14 --timer=20 +states 7566 +attack NoClaim +time 2.002e+01 +st/sec 3.779e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 15: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=15 --timer=20 +states 8496 +attack NoClaim +time 2.005e+01 +st/sec 4.237e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 16: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=16 --timer=20 +states 7453 +attack NoClaim +time 2.003e+01 +st/sec 3.721e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 17: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=17 --timer=20 +states 3888 +attack NoClaim +time 2.004e+01 +st/sec 1.940e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 18: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=18 --timer=20 +states 6582 +attack NoClaim +time 2.003e+01 +st/sec 3.286e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 19: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=19 --timer=20 +states 9022 +attack NoClaim +time 2.001e+01 +st/sec 4.509e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 1 correct: bounded_proof +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 20: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=20 --timer=20 +states 6393 +attack NoClaim +time 2.003e+01 +st/sec 3.192e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 21: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=21 --timer=20 +states 4284 +attack NoClaim +time 2.002e+01 +st/sec 2.140e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 4 correct: bounded_proof time=20 +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 22: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=22 --timer=20 +states 6769 +attack NoClaim +time 2.001e+01 +st/sec 3.383e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 23: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=23 --timer=20 +states 8175 +attack NoClaim +time 2.002e+01 +st/sec 4.083e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 14 correct: bounded_proof time=20 +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 24: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=24 --timer=20 +states 9625 +attack NoClaim +time 2.003e+01 +st/sec 4.805e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 25: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=25 --timer=20 +states 3883 +attack NoClaim +time 2.002e+01 +st/sec 1.940e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 26: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=26 --timer=20 +states 11992 +attack NoClaim +time 2.004e+01 +st/sec 5.984e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 27: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=27 --timer=20 +states 7361 +attack NoClaim +time 2.004e+01 +st/sec 3.673e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 28: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=28 --timer=20 +states 6277 +attack NoClaim +time 2.004e+01 +st/sec 3.132e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 29: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=29 --timer=20 +states 4728 +attack NoClaim +time 2.005e+01 +st/sec 2.358e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 30: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=30 --timer=20 +states 7610 +attack NoClaim +time 2.004e+01 +st/sec 3.797e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 31: +./multinsl-generator.py 3 11 | scyther -a -r5 -m2 --summary --goal-select=31 --timer=20 +states 8506 +attack NoClaim +time 2.003e+01 +st/sec 4.247e+02 +claim mnsl3v11 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v11 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v11 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v11 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v11 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Testing protocol 15. +Heuristic 0: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=0 --timer=20 +states 7499 +attack NoClaim +time 2.003e+01 +st/sec 3.744e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 1: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=1 --timer=20 +states 3866 +attack NoClaim +time 2.004e+01 +st/sec 1.929e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 2: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=2 --timer=20 +states 6558 +attack NoClaim +time 2.003e+01 +st/sec 3.274e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 3: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=3 --timer=20 +states 8933 +attack NoClaim +time 2.002e+01 +st/sec 4.462e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 1 correct: bounded_proof +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 4: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=4 --timer=20 +states 6354 +attack NoClaim +time 2.002e+01 +st/sec 3.174e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 5: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=5 --timer=20 +states 4278 +attack NoClaim +time 2.004e+01 +st/sec 2.135e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 4 correct: bounded_proof time=20 +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 6: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=6 --timer=20 +states 6749 +attack NoClaim +time 2.002e+01 +st/sec 3.371e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 7: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=7 --timer=20 +states 8166 +attack NoClaim +time 2.003e+01 +st/sec 4.077e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 14 correct: bounded_proof time=20 +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 8: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=8 --timer=20 +states 9805 +attack NoClaim +time 2.006e+01 +st/sec 4.888e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 9: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=9 --timer=20 +states 3873 +attack NoClaim +time 2.004e+01 +st/sec 1.933e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 10: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=10 --timer=20 +states 10729 +attack NoClaim +time 2.006e+01 +st/sec 5.348e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 11: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=11 --timer=20 +states 6679 +attack NoClaim +time 2.005e+01 +st/sec 3.331e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 12: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=12 --timer=20 +states 6119 +attack NoClaim +time 2.005e+01 +st/sec 3.052e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 13: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=13 --timer=20 +states 3513 +attack NoClaim +time 2.009e+01 +st/sec 1.749e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 14: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=14 --timer=20 +states 7548 +attack NoClaim +time 2.004e+01 +st/sec 3.766e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 15: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=15 --timer=20 +states 8461 +attack NoClaim +time 2.002e+01 +st/sec 4.226e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 16: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=16 --timer=20 +states 7503 +attack NoClaim +time 2.003e+01 +st/sec 3.746e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 17: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=17 --timer=20 +states 3837 +attack NoClaim +time 2.003e+01 +st/sec 1.916e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 18: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=18 --timer=20 +states 6537 +attack NoClaim +time 2.005e+01 +st/sec 3.260e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 19: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=19 --timer=20 +states 8893 +attack NoClaim +time 2.004e+01 +st/sec 4.438e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 1 correct: bounded_proof +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 20: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=20 --timer=20 +states 6325 +attack NoClaim +time 2.003e+01 +st/sec 3.158e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 21: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=21 --timer=20 +states 4253 +attack NoClaim +time 2.005e+01 +st/sec 2.121e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 4 correct: bounded_proof time=20 +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 22: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=22 --timer=20 +states 6756 +attack NoClaim +time 2.004e+01 +st/sec 3.371e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 23: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=23 --timer=20 +states 8149 +attack NoClaim +time 2.003e+01 +st/sec 4.068e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 14 correct: bounded_proof time=20 +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 24: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=24 --timer=20 +states 9785 +attack NoClaim +time 2.004e+01 +st/sec 4.883e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 25: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=25 --timer=20 +states 3832 +attack NoClaim +time 2.006e+01 +st/sec 1.910e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 26: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=26 --timer=20 +states 10699 +attack NoClaim +time 2.009e+01 +st/sec 5.326e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 27: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=27 --timer=20 +states 6672 +attack NoClaim +time 2.006e+01 +st/sec 3.326e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 28: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=28 --timer=20 +states 6136 +attack NoClaim +time 2.010e+01 +st/sec 3.053e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 29: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=29 --timer=20 +states 3521 +attack NoClaim +time 2.009e+01 +st/sec 1.753e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 30: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=30 --timer=20 +states 7584 +attack NoClaim +time 2.006e+01 +st/sec 3.781e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 +Heuristic 31: +./multinsl-generator.py 3 15 | scyther -a -r5 -m2 --summary --goal-select=31 --timer=20 +states 8369 +attack NoClaim +time 2.004e+01 +st/sec 4.176e+02 +claim mnsl3v15 R2V Nisynch_R2b found: 0 correct: does_not_occur +claim mnsl3v15 R2V Secret_R2a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R1V Nisynch_R1b found: 0 correct: does_not_occur +claim mnsl3v15 R1V Secret_R1a found: 1 correct: bounded_proof time=20 +claim mnsl3v15 R0V Nisynch_R0b found: 0 correct: does_not_occur +claim mnsl3v15 R0V Secret_R0a found: 1 correct: bounded_proof time=20 + + +13,25 work well. diff --git a/spdl/multiparty/mnsl-results.txt b/spdl/multiparty/mnsl-results.txt new file mode 100644 index 0000000..a04a56f --- /dev/null +++ b/spdl/multiparty/mnsl-results.txt @@ -0,0 +1,33 @@ +Report: +------- + +Using P 3 and 2 runs, we find attacks on [1, 5, 9, 13, 18, 22, 26, 30] +Using P 3 and 3 runs, we find attacks on [0, 3, 4, 7, 16, 19, 20, 23] +Using P 3 and 4 runs, we find attacks on [2, 6, 10, 14, 17, 21, 27, 31] +Using P 3 and 5 runs, we find attacks on [25, 29] +Using P 4 and 3 runs, we find attacks on [8, 24] +Using P 4 and 5 runs, we find attacks on [12, 28] + +Log: +---- +Slave1:multiparty% ./test-variants.py +Testing using P 3 and 2 runs. +Using P 3 and 2 runs, we find attacks on [1, 5, 9, 13, 18, 22, 26, 30] +Therefore, we are left with 24 candidates: [0, 2, 3, 4, 6, 7, 8, 10, 11, 12, 14, 15, 16, 17, 19, 20, 21, 23, 24, 25, 27, 28, 29, 31] +Testing using P 3 and 3 runs. +Using P 3 and 3 runs, we find attacks on [0, 3, 4, 7, 16, 19, 20, 23] +Therefore, we are left with 16 candidates: [2, 6, 8, 10, 11, 12, 14, 15, 17, 21, 24, 25, 27, 28, 29, 31] +Testing using P 3 and 4 runs. +Using P 3 and 4 runs, we find attacks on [2, 6, 10, 14, 17, 21, 27, 31] +Therefore, we are left with 8 candidates: [8, 11, 12, 15, 24, 25, 28, 29] +Testing using P 3 and 5 runs. +Using P 3 and 5 runs, we find attacks on [25, 29] +Therefore, we are left with 6 candidates: [8, 11, 12, 15, 24, 28] +Testing using P 4 and 3 runs. +Using P 4 and 3 runs, we find attacks on [8, 24] +Therefore, we are left with 4 candidates: [11, 12, 15, 28] +Testing using P 4 and 4 runs. +Testing using P 4 and 5 runs. +Using P 4 and 5 runs, we find attacks on [12, 28] +Therefore, we are left with 2 candidates: [11, 15] +Testing using P 4 and 6 runs. diff --git a/spdl/multiparty/multinsl-generator.py b/spdl/multiparty/multinsl-generator.py new file mode 100755 index 0000000..003de06 --- /dev/null +++ b/spdl/multiparty/multinsl-generator.py @@ -0,0 +1,355 @@ +#!/usr/bin/python +# +# Generate Multi-party NSL protocol description for n parties +# +# Input: P variant +# +# variant uses some bits: +# bit mask meaning if set to '1' +# (message type 1) +# 0 1 nonces in reverse +# 1 2 nonces after agents +# 2 4 agents in reverse +# 3 8 interleaved variant +# (message type 2) +# 4 16 nonces in reverse in message 2 +# +# Convention similar to e.g. Prolog: capitals indicate open variables; +# in particular, they can be bound by _any_ value during the run, +# assuming full type flaws. +# +import sys +from optparse import OptionParser + +def parseArgs(): + usage = "usage: %s [opts] Parties Variant" % sys.argv[0] + parser = OptionParser(usage=usage) + parser.add_option('-p','--protocol', dest='protocol', + help='Generate another protocol [nsl,bke]', default="nsl", + action='store') + (opts, args) = parser.parse_args() + if len(args) != 2: + parser.print_help() + sys.exit(0) + if opts.protocol not in ["nsl","bke","nsl-priv-noprop","nsl-pub-nap","bke-nap"]: + print "I don't know the %s protocol." % (opts.protocol) + sys.exit(0) + return (opts,args) + + +def variablerole (r, inrole): + if r == inrole or inrole == 0: + return False + else: + return True + +def role (r,inrole): + global P + + return "r%i" % (r % P) + +def zeroconst (): + + """ This is 0 or some other stupid constant """ + + return "zeroconst" + +def nonce (r,inrole): + global P + + if r == inrole: + # nonce of our own + return "n%i" % (r % P) + else: + # a variable: we want to see this in the notation + return "N%i" % (r % P) + +def extend (s1, s2): + if s1 == "": + return s2 + else: + return s1 + "," + s2 + +def weavel (l1,l2,reverse1,swap,reverse2,interleave): + """ l1 is typically a list of nonces, l2 might be empty (names) """ + global variant + + if reverse1: + l1.reverse() + if l2 == []: + return l1 + else: + if reverse2: + l2.reverse() + if swap: + # swap + l3 = l1 + l1 = l2 + l2 = l3 + if interleave: + rl = [] + largest = max(len(l1),len(l2)) + for i in range (0,largest): + if i < len(l1): + rl.append(l1[i]) + if i < len(l2): + rl.append(l2[i]) + return rl + else: + return l1 + l2 + +def message1 (label,inrole): + global P,variant,opts + + if opts.protocol in ['bke','nsl']: + noncelist = [] + for i in range(0,label+1): + noncelist.append(nonce(i,inrole)) + rolelist = [] + for i in range(0,P): + if i != (label+1) % P: + rolelist.append(role(i,inrole)) + + return ",".join(weavel(noncelist,rolelist, + (variant & 1 != 0), + (variant & 2 != 0), + (variant & 4 != 0), + (variant & 8 != 0) + )) + elif opts.protocol == 'nsl-priv-noprop': + + list = [] + for i in range(0,P): + list.append(role(i,inrole)) + list.append(nonce(0,inrole)) + msg = ",".join(list) + + for i in range(1,label+1): + msg = "{ %s,%s }sk(%s)" % (msg,nonce(i,inrole),role(i,inrole)) + + return msg + + elif opts.protocol == 'nsl-pub-nap': + + list = [] + for i in range(0,P): + list.append(role(i,inrole)) + list.append(nonce(0,inrole)) + msg = ",".join(list) + + for i in range(1,label+1): + msg = "{ %s }sk(%s), %s" % (msg,role(i,inrole),nonce(i,inrole)) + + msg = "{ %s }pk(%s)" % (msg,role(label+1,inrole)) + + return msg + elif opts.protocol == 'bke-nap': + + list = [] + for i in range(0,P): + list.append(role(i,inrole)) + list.append(nonce(0,inrole)) + msg = ",".join(list) + + for i in range(1,label+1): + msg = "{ %s }sk(%s), %s" % (msg,role(i,inrole),nonce(i,inrole)) + + msg = "{ %s }pk(%s)" % (msg,role(label+1,inrole)) + + return msg + else: + print "Hmm, I don't know how to create the first message for protocol %s" % (opts.protocol) + +def message2 (label,inrole): + global P,variant,opts + + if opts.protocol == "nsl": + noncelist = [] + for i in range (((label + 1) % P),P): + noncelist.append(nonce(i,inrole)) + + return ",".join(weavel(noncelist,[], + (variant & 16 != 0), + False, + False, + False + )) + elif opts.protocol == "bke": + noncelist = [] + for i in range (((label + 1) % P) + 1,P): + noncelist.append(nonce(i,inrole)) + if len(noncelist) == 0: + noncelist.append(zeroconst()) + + return ",".join(weavel(noncelist,[], + (variant & 16 != 0), + False, + False, + False + )) + elif opts.protocol in ['nsl-priv-noprop','nsl-pub-nap']: + msg = message1(P-1,inrole) + for i in range(0,label-P+1): + msg = "{ %s }sk(%s)" % (msg,role(i,inrole)) + + if opts.protocol == 'nsl-pub-nap': + msg = "{ %s }pk(%s)" % (msg,role(label+1,inrole)) + + return msg + elif opts.protocol == 'bke-nap': + msg = message1(P-1,inrole) + for i in range(0,label-P+1): + msg = "{ %s }sk(%s)" % (msg,role(i,inrole)) + + msg = "{ %s }%s" % (msg,nonce((label+1) % P,inrole)) + + return msg + else: + print "Hmm, I don't know how to create the final message for protocol %s" % (opts.protocol) + +def message (label,inrole): + global P,opts + + if opts.protocol in ['bke','nsl']: + s = "{ " + if label < P: + s = s + message1 (label,inrole) + else: + s = s + message2 (label,inrole) + + if opts.protocol == "bke" and not (label < P): + s = s + " }" + nonce((label+1) % P, inrole) + else: + s = s + " }pk(%s)" % role(label+1,inrole) + return s + else: + if label < P: + return message1 (label,inrole) + else: + return message2 (label,inrole) + + +def action (event,label,inrole): + s = "\t\t%s_%i(%s,%s, " % (event,label, role(label,inrole), + role(label+1,inrole)) + s += message (label,inrole) + s += " );\n" + return s + +def read (label,inrole): + return action ("read", label,inrole) + + +def send (label,inrole): + return action ("send", label,inrole) + +def roledef (r): + global P,opts + + s = "" + s += "\trole " + role(r,r) + "\n\t{\n" + + # constants for this role + + s += "\t\tconst " + nonce (r,r) + ": Nonce;\n" + + # variables + + s += "\t\tvar " + nr = 0 + for i in range (0,P): + if r != i: + if nr > 0: + s += "," + s += nonce(i,r) + nr += 1 + + s += ": Nonce;\n" + + # implicit role variables + + rolevars = [] + for i in range (0,P): + if variablerole(i,r): + rolevars.append(role(i,r)) + + if rolevars != []: + s += "\t\t// Implicit role variables: " + s += ",".join(rolevars) + s += ": Role;\n" + + # actions + + s += "\n" + if r > 0: + # Initial read + s += read(r-1,r) + s += send(r,r) + s += read(P+r-1,r) + if r < (P-1): + # Final send + s += send(P+r,r) + + # claims + + if opts.protocol in ['bke','nsl','nsl-pub-nap','bke-nap']: + s += "\t\tclaim_%sa( %s, Secret, %s );\n" % (role(r,r), role(r,r), + nonce(r,r)) + s += "\t\tclaim_%sb( %s, Nisynch );\n" % (role(r,r), role(r,r)) + + # close + s += "\t}\n\n" + return s + + +def protocol (args): + global P,variant,opts + + P = int(args[0]) + variant = int(args[1]) + + s = "" + s += "// Generalized %s protocol for %i parties\n\n" % (opts.protocol,P) + s += "// " + str(opts) + "\n\n" + s += "// Variant %i\n" % variant + s += "const pk: Function;\n" + s += "secret sk: Function;\n" + s += "inversekeys (pk,sk);\n" + + if opts.protocol == "bke": + s += "usertype Globalconstant;\n" + s += "const %s: Globalconstant;\n" % (zeroconst()) + + s += "\n" + + s += "protocol mnsl%iv%i(" % (P,variant) + for i in range (0,P): + if i > 0: + s += "," + s += role(i,i) + s += ")\n{\n" + + for i in range (0,P): + s += roledef(i) + + s += "}\n\n" + + s += "const Alice, Bob: Agent;\n\n" + + s += "const Eve: Agent;\n" + s += "untrusted Eve;\n" + s += "const ne: Nonce;\n" + s += "compromised sk(Eve);\n" + + s += "\n" + return s + +def main(): + global opts + + (opts,args) = parseArgs() + print protocol(args) + +# Only if main stuff +if __name__ == '__main__': + main() diff --git a/spdl/multiparty/test-heuristics.py b/spdl/multiparty/test-heuristics.py new file mode 100755 index 0000000..34c03fc --- /dev/null +++ b/spdl/multiparty/test-heuristics.py @@ -0,0 +1,69 @@ +#!/usr/bin/python +# +# +# Idea: +# +# We test all options for the heuristics [0..31] to compare, +# and sincerely hope on gives a complete proof. +# we slowly refine the tests. +# +import commands + +def startset(): + mainlist = [11, 15] + print "Starting with", mainlist + return mainlist + +def tuplingchoice(heur,variant,P,runs,latupling): + # variant is in range [0..64>, + # where we use the highest bid to signify the + # associativity of the tupling. + + extraflags = "" + if latupling: + extraflags += " --la-tupling" + + # Choose heuristics + extraflags += " --goal-select=%i" % (heur) + + # Time limit + extraflags += " --timer=20" + + s = "./multinsl-generator.py" + s += " %i %i" % (P,variant) + s += " | scyther -a -r%i -m2 --summary %s" % (runs, extraflags) + + ## Old stuff + #s += " | scyther -a -r%i --summary" % runs + + # Show what we're doing + print s + + #s += " | grep \"complete\"" + out = commands.getoutput(s) + if out == "": + #print "Okay" + return False + else: + print out + return True + +def testvariant(h,v,p,r): + if tuplingchoice (h,v,p,r, False): + return True + else: + return tuplingchoice (h,v,p,r, True) + +def scan(testlist, P, runs): + print "Testing using P %i and %i runs." % (P,runs) + for i in testlist: + print "Testing protocol %i." % (i) + for h in range (0,32): + print "Heuristic %i:" % (h) + testvariant (h,i,P,runs) + +def main(): + candidates = startset() + scan(candidates,3,5) + +main() diff --git a/spdl/multiparty/test-variants.py b/spdl/multiparty/test-variants.py new file mode 100755 index 0000000..ae00ce7 --- /dev/null +++ b/spdl/multiparty/test-variants.py @@ -0,0 +1,79 @@ +#!/usr/bin/python +# +# +# Idea: +# +# We test all variants [0..31] until we are sure they work. Thus, +# we slowly refine the tests. +# +import commands + +def startset(): + return range(0,32) + + mainlist = [11, 15] + print "Starting with", mainlist + return mainlist + +def tuplingchoice(variant,P,runs,latupling): + # variant is in range [0..64>, + # where we use the highest bid to signify the + # associativity of the tupling. + + extraflags = "" + if latupling: + extraflags += " --la-tupling" + + s = "./multinsl-generator.py" + s += " %i %s" % (P,variant) + s += " | scyther -r%i --untyped %s" % (runs, extraflags) + #s += " | scyther -a -r%i --summary" % runs + #print s + s += " | grep \"Fail\"" + out = commands.getoutput(s) + if out == "": + #print "Okay" + return True + else: + #print out + # Thus, MultiNSL P variant has the first attack for n runs + return False + +def testvariant(v,p,r): + if not tuplingchoice (v,p,r, False): + return False + else: + return tuplingchoice (v,p,r, True) + +def removeattacks (testlist, P, runs): + okaylist = [] + for v in testlist: + if testvariant (v, P, runs): + okaylist.append(v) + return okaylist + +def scan(testlist, P, runs): + print "Testing using P %i and %i runs." % (P,runs) + results = removeattacks (testlist, P, runs) + if len(results) < len(testlist): + attacked = [] + for i in range(0,len(testlist)): + if testlist[i] not in results: + attacked.append(testlist[i]) + print "Using P %i and %i runs, we find attacks on %s" % (P,runs, str(attacked)) + print "Therefore, we are left with %i candidates: " % (len(results)), results + + return results + +def main(): + candidates = startset() + for P in range(3,7): + for rundiff in range(0,5): + candidates = scan(candidates,P,P+rundiff) + + print + print "Good variants:" + print candidates + + +main() diff --git a/spdl/spdl-defaults.inc b/spdl/spdl-defaults.inc new file mode 100644 index 0000000..9a0b77c --- /dev/null +++ b/spdl/spdl-defaults.inc @@ -0,0 +1,34 @@ +/* default includes */ + +/* asymmetric */ + +const pk,hash: Function; +secret sk,unhash: Function; +inversekeys (pk,sk); +inversekeys (hash,unhash); + + +/* symmetric */ + +usertype SessionKey; +secret k: Function; + +/* agents */ + +const a,b,e: Agent; + + +/* untrusted e */ + +untrusted e; +compromised sk(e); +const ne: Nonce; +const kee: SessionKey; + +compromised k(e,e); +compromised k(e,a); +compromised k(e,b); +compromised k(a,e); +compromised k(b,e); + +