- Added protocols

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);

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);

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);

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);
+

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);
+

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);
+

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);

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);

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);

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);

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);
+

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);

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);

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);

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);

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);

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);

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);

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);

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);

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);
+	}
+}
+
+

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);

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);

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);

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);

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);

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);
+

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);

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);

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);

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);

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);

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);

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);

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);
+

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);
+

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);
+
+

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);
+
+

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);
+	}
+}

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);
+	}
+}

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);

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);
+

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);

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);
+

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);

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);

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);
+

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

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;

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);

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);

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);

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);
+
+

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);
+	}
+}

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);
+
+

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);
+
+

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);
+
+

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);
+

spdl/misc/tls-HSDDM05.spdl

@@ -0,0 +1,63 @@
+# 1 "tls-HSDDM05.cpp"
+# 1 "<built-in>"
+# 1 "<command line>"
+# 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);

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;
+

spdl/misc/tls-paulson-avispa.spdl

@@ -0,0 +1,76 @@
+# 1 "tls-paulson-avispa.cpp"
+# 1 "<built-in>"
+# 1 "<command line>"
+# 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;

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);
+

spdl/misc/tls-paulson.spdl

@@ -0,0 +1,79 @@
+# 1 "tls-paulson.cpp"
+# 1 "<built-in>"
+# 1 "<command line>"
+# 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);

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);
+
+

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);
+
+

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);

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);
+

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);
+

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);
+

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);
+

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) );
+	}
+}
+

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);
+

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);
+

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);
+

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.

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.

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()

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()

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()

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);
+
+