Initial revision

spdl/bkepk-ce.spdl

@@ -0,0 +1,59 @@
+/* 
+	Bilateral Key Exchange with Public Key protocol (BKEPK)
+
+	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.
+*/
+
+const pk,hash: Function;
+secret sk: Function;
+
+inversekeys (pk,sk);
+
+protocol bkepk(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 (A,A, n);
+	}
+}
+
+const Alice,Bob,Eve;
+
+compromised sk(Eve);
+
+
+run bkepk.A(Alice,Bob,Alice);
+run bkepk.A(Alice,Bob,Alice);
+run bkepk.A(Alice,Bob,Alice);
+run bkepk.B(Bob,Alice,Alice);
+run bkepk.B(Bob,Alice,Alice);
+run bkepk.B(Bob,Alice,Alice);
+
+run bkepk.testnonce(Alice,Bob,Alice);
+run bkepk.testnonce(Alice,Bob,Alice);
+run bkepk.testnonce(Alice,Bob,Alice);

spdl/bkepk.spdl

@@ -0,0 +1,60 @@
+/* 
+	Bilateral Key Exchange with Public Key protocol (BKEPK)
+
+	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.
+*/
+
+const pk,hash: Function;
+secret sk,unhash: Function;
+
+inversekeys (pk,sk);
+inversekeys (hash,unhash);
+
+protocol bkepk(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 (A,A, n);
+	}
+}
+
+const Alice,Bob,Eve;
+
+compromised sk(Eve);
+
+
+run bkepk.A(Alice,Bob,Alice);
+run bkepk.A(Alice,Bob,Alice);
+run bkepk.A(Alice,Bob,Alice);
+run bkepk.B(Bob,Alice,Alice);
+run bkepk.B(Bob,Alice,Alice);
+run bkepk.B(Bob,Alice,Alice);
+
+run bkepk.testnonce(Alice,Bob,Alice);
+run bkepk.testnonce(Alice,Bob,Alice);
+run bkepk.testnonce(Alice,Bob,Alice);

spdl/notes.txt

@@ -0,0 +1,2 @@
+- Paulson TLS -r4 -t4 -m0 doet 186m 11s time (top) over 160.390.000 states
+  ongeveer, en draait nog.

spdl/ns3-brutus.spdl

@@ -0,0 +1,50 @@
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+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(I,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(I,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 ns3.R(Agent,Bob);
+  run ns3.I(Alice,Agent);
+run ns3.R(Agent,Bob);
+  run ns3.I(Alice,Agent);
+run ns3.R(Agent,Bob);
+  run ns3.I(Alice,Agent);
+run ns3.R(Agent,Bob);
+  run ns3.I(Alice,Agent);
+run ns3.R(Agent,Bob);
+  run ns3.I(Alice,Agent);

spdl/ns3-extreme.spdl

@@ -0,0 +1,49 @@
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+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(I,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(I,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 */
+
+run ns3.I(Alice,Bob);
+	run ns3.R(Alice,Bob);
+run ns3.I(Alice,Eve);
+	run ns3.R(Eve,Bob);
+run ns3.I(Bob,Alice);
+	run ns3.R(Bob,Alice);
+run ns3.I(Bob,Eve);
+	run ns3.R(Eve,Alice);
+run ns3.I(Alice,Alice);
+	run ns3.R(Bob,Bob);

spdl/ns3-var.spdl

@@ -0,0 +1,37 @@
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+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(I,ni,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(R,ni,nr);
+	}
+}
+
+const Alice,Bob,Eve : Agent;
+
+untrusted Eve;
+const nc: Nonce;
+compromised sk(Eve);
+
+run ns3.I(Agent,Agent);
+run ns3.R(Agent,Agent);

spdl/ns3.spdl

@@ -0,0 +1,37 @@
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+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(I,ni,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(R,ni,nr);
+	}
+}
+
+const Alice,Bob,Eve: Agent;
+
+untrusted Eve;
+const nc: Nonce;
+compromised sk(Eve);
+
+run ns3.I(Alice,Eve);
+run ns3.R(Alice,Bob);

spdl/nsl3-var.spdl

@@ -0,0 +1,37 @@
+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(I,ni,nr);
+	}	
+	
+	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(I,ni,nr);
+	}
+}
+
+const Alice,Bob,Eve: Agent;
+
+untrusted Eve;
+const nc: Nonce;
+compromised sk(Eve);
+
+run nsl3.I(Agent,Agent);
+run nsl3.R(Agent,Agent);

spdl/nsl3.spdl

@@ -0,0 +1,37 @@
+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(I,ni,nr);
+	}	
+	
+	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(I,ni,nr);
+	}
+}
+
+const Alice,Bob,Eve: Agent;
+
+untrusted Eve;
+const nc: Nonce;
+compromised sk(Eve);
+
+run nsl3.I(Agent,Agent);
+run nsl3.R(Alice,Bob);

spdl/nsl7.spdl

@@ -0,0 +1,22 @@
+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(I,nr,ni);
+	}
+}
+
+const Alice,Bob;
+
+run nsl3.R(Alice,Bob);
+run nsl3.R(Alice,Bob);

spdl/otwayrees.spdl

@@ -0,0 +1,62 @@
+secret const k : Function;
+
+/* Version from the Spore Librairy
+   http://www.lsv.ens-cachan.fr/spore/otwayRees.html
+*/
+
+protocol otwayrees(A,B,S)
+{
+	role A
+	{
+		const na : Nonce;
+		const M : String;
+		var nb : Nonce;
+		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(A, kab);
+	}
+
+	role B
+	{
+		var na : Nonce;
+		var M : String;
+		const nb : Nonce;
+		var kab : SesKey;
+		var t1,t2 : Ticket;
+
+		read_1(A,B, M,A,B, t1 );
+		send_2(B,S, M,A,B, t2, { 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(B, kab);
+	}
+
+	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/test-clp.sh

@@ -0,0 +1,12 @@
+#!/bin/sh
+
+../scyther -d -p0 -m2 -t2 -r 2 <ns3-brutus.spdl >brutus-m2-t2-r2.out
+../scyther -d -p0 -m2 -t2 -r 3 <ns3-brutus.spdl >brutus-m2-t2-r3.out
+../scyther -d -p0 -m2 -t2 -r 4 <ns3-brutus.spdl >brutus-m2-t2-r4.out
+../scyther -d -p0 -m2 -t2 -r 5 <ns3-brutus.spdl >brutus-m2-t2-r5.out
+../scyther -d -p0 -m2 -t2 -r 6 <ns3-brutus.spdl >brutus-m2-t2-r6.out
+
+../scyther -d -p0 -m2 -t1 -r 2 <ns3-brutus.spdl >brutus-m2-t1-r2.out
+../scyther -d -p0 -m2 -t1 -r 3 <ns3-brutus.spdl >brutus-m2-t1-r3.out
+../scyther -d -p0 -m2 -t1 -r 4 <ns3-brutus.spdl >brutus-m2-t1-r4.out
+../scyther -d -p0 -m2 -t1 -r 5 <ns3-brutus.spdl >brutus-m2-t1-r5.out

spdl/test.sh

@@ -0,0 +1,18 @@
+#!/bin/sh
+
+../scyther -d -p0 -t4 -r 2 <ns3-brutus.spdl >brutus-t4-r2.out
+../scyther -d -p0 -t4 -r 3 <ns3-brutus.spdl >brutus-t4-r3.out
+../scyther -d -p0 -t4 -r 4 <ns3-brutus.spdl >brutus-t4-r4.out
+../scyther -d -p0 -t4 -r 5 <ns3-brutus.spdl >brutus-t4-r5.out
+../scyther -d -p0 -t4 -r 6 <ns3-brutus.spdl >brutus-t4-r6.out
+
+../scyther -d -p0 -t2 -r 2 <ns3-brutus.spdl >brutus-t2-r2.out
+../scyther -d -p0 -t2 -r 3 <ns3-brutus.spdl >brutus-t2-r3.out
+../scyther -d -p0 -t2 -r 4 <ns3-brutus.spdl >brutus-t2-r4.out
+../scyther -d -p0 -t2 -r 5 <ns3-brutus.spdl >brutus-t2-r5.out
+../scyther -d -p0 -t2 -r 6 <ns3-brutus.spdl >brutus-t2-r6.out
+
+../scyther -d -p0 -t1 -r 2 <ns3-brutus.spdl >brutus-t1-r2.out
+../scyther -d -p0 -t1 -r 3 <ns3-brutus.spdl >brutus-t1-r3.out
+../scyther -d -p0 -t1 -r 4 <ns3-brutus.spdl >brutus-t1-r4.out
+../scyther -d -p0 -t1 -r 5 <ns3-brutus.spdl >brutus-t1-r5.out

spdl/tls-paulson.spdl

@@ -0,0 +1,78 @@
+#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)
+
+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(a, CLIENTK, SERVERK);
+
+	}	
+	
+	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(a, CLIENTK, SERVERK);
+	}
+}
+
+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/tmn.spdl

@@ -0,0 +1,54 @@
+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(A,Ka,Kb);
+	}	
+	
+	role B
+	{
+		const Kb: Key;
+
+		read_2(S,B, A );
+		send_3(B,S, A, { Kb }pk(S) );
+
+		claim(B,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(S,Ka);
+	}
+}
+
+const Alice,Bob,Eve: Agent;
+const Simon: Server;
+
+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/wmf-brutus.spdl

@@ -0,0 +1,47 @@
+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(B, 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/woolam-ce.spdl

@@ -0,0 +1,37 @@
+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(B,authToken);
+	}
+}
+
+run woolamce.B(Agent,Agent,Simon);
+run woolamce.B(Agent,Agent,Simon);
+

spdl/woolam-cmv.spdl

@@ -0,0 +1,37 @@
+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 woolamcmv(A,B,S)
+{
+	role B
+	{
+		var Na: Nonce;
+		const Nb: Nonce;
+		var Kab: SessionKey;
+		var t1,t2: Ticket;
+
+		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(B,Kab,Nb,authToken);
+	}
+}
+
+run woolamcmv.B(Alice,Bob,Simon);
+run woolamcmv.B(Alice,Bob,Simon);
+

spdl/yahalom-ban.spdl

@@ -0,0 +1,53 @@
+// BAN modified version of the yahalom protocol
+// Type flaw
+// This version actually works!
+
+const a,b,c : Agent;
+const s : Simon;
+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(A, 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(B, 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) );
+	}
+}
+
+run yahalomBan.A(Agent,Agent,s);
+run yahalomBan.A(Agent,Agent,s);
+run yahalomBan.B(Agent,Agent,s);
+run yahalomBan.B(Agent,Agent,s);
+run yahalomBan.S(Agent,Agent,s);
+

spdl/yahalom-lowe.spdl

@@ -0,0 +1,53 @@
+// Yahalom protocol
+
+const a,b,s,Eve : Agent;
+secret k : Function;
+
+untrusted Eve;
+compromised k(Eve,s);
+
+protocol yahalomlowe(A,B,S)
+{
+	role A
+	{
+		const na: Nonce;
+		var nb: Nonce;
+		var kab: Sessionkey;
+
+		send_1(A,B, A,na);
+		read_3(S,A, {B,kab,na,nb}k(A,S) );
+		send_5(A,B, {A,B,S,nb}kab );
+		claim(A, kab);
+	}
+
+	role B
+	{
+		const nb: Nonce;
+		var na: Nonce;
+		var kab: Sessionkey;
+
+		read_1(A,B, A,na);
+		send_2(B,S, {A,na,nb}k(B,S) );
+		read_4(S,B, {A,kab}k(B,S) );
+		read_5(A,B, {A,B,S,nb}kab );
+		claim(B, kab);
+	}
+
+	role S
+	{
+		const kab: Sessionkey;
+		var na,nb: Nonce;
+
+		read_2(B,S, {A,na,nb}k(B,S) );
+		send_3(S,A, {B,kab,na,nb}k(A,S) );
+		send_4(S,B, {A,kab}k(B,S) );
+	}
+}
+
+run yahalomlowe.A(Agent,Agent,s);
+run yahalomlowe.B(Agent,Agent,s);
+run yahalomlowe.S(Agent,Agent,s);
+
+run yahalomlowe.A(Agent,Agent,s);
+run yahalomlowe.B(Agent,Agent,s);
+

spdl/yahalom.spdl

@@ -0,0 +1,50 @@
+// Yahalom protocol
+
+const a,b,s : Agent;
+secret k : Function;
+
+
+protocol yahalom(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,nb}k(A,S), ticket );
+		send_4(A,B, ticket, {nb}kab );
+		claim(A, 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,nb}k(B,S) );
+		read_4(A,B, {A,kab}k(B,S) , {nb}kab );
+		claim(B, 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,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);
+