diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl
new file mode 100644
index 0000000..17220b0
--- /dev/null
+++ b/spdl/SPORE/yahalom-ban.spdl
@@ -0,0 +1,63 @@
+# BAN simplified version of Yahalom
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/yahalomBAN.html
+#
+# Note:
+# This protocol uses a ticket so scyther will only be able to verify
+# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+#
+
+secret k : Function;
+
+usertype Ticket, Key;
+
+
+protocol yahalomBAN(I,R,S)
+{
+	role I
+	{
+		const Ni: Nonce;
+		var Nr: Nonce;
+		var T: Ticket;
+		var Kir: Key;
+
+		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_I1(I, Secret,Kir);
+		claim_I2(I, Nisynch);
+	}
+
+	role R
+	{
+		const Nr: Nonce;
+		var Ni: Nonce;
+		var T: Ticket;
+		var Kir: Key;
+
+		read_1(I,R, I,Ni);
+		send_2(R,S, R, Nr, {I,Ni}k(R,S) );
+		read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir );
+
+		claim_R1(R, Secret,Kir);
+        claim_R2(R, Nisynch);
+	}
+
+	role S
+	{
+		const Kir: Key;
+		var Ni,Nr: Nonce;
+
+		read_2(R,S, R, {I,Ni,Nr}k(R,S) );
+		send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
+	}
+}
+
+const Alice,Bob,Simon : Agent;
+
+run yahalomBAN.I(Agent,Agent,s);
+run yahalomBAN.I(Agent,Agent,s);
+run yahalomBAN.R(Agent,Agent,s);
+
diff --git a/spdl/SPORE/yahalom-lowe.spdl b/spdl/SPORE/yahalom-lowe.spdl
new file mode 100644
index 0000000..ab0c6e5
--- /dev/null
+++ b/spdl/SPORE/yahalom-lowe.spdl
@@ -0,0 +1,60 @@
+# Lowe's modified version of Yahalom
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/yahalomLowe.html
+#
+#
+
+secret k : Function;
+
+usertype Key;
+
+
+protocol yahalomLowe(I,R,S)
+{
+	role I
+	{
+		const Ni: Nonce;
+		var Nr: Nonce;
+		var Kir: Key;
+
+		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_I1(I, Secret,Kir);
+		claim_I2(I, Nisynch);
+	}
+
+	role R
+	{
+		const Nr: Nonce;
+		var Ni: Nonce;
+		var Kir: Key;
+
+		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_R1(R, Secret,Kir);
+        claim_R2(R, Nisynch);
+	}
+
+	role S
+	{
+		const Kir: Key;
+		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));
+	}
+}
+
+const Alice,Bob,Simon : Agent;
+
+run yahalomLowe.I(Agent,Agent,s);
+run yahalomLowe.I(Agent,Agent,s);
+run yahalomLowe.R(Agent,Agent,s);
+
diff --git a/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl
new file mode 100644
index 0000000..bed720d
--- /dev/null
+++ b/spdl/SPORE/yahalom-paulson.spdl
@@ -0,0 +1,63 @@
+# Paulson's strengthened version of Yahalom
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/yahalomPaulson.html
+#
+# Note:
+# This protocol uses a ticket so scyther will only be able to verify
+# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+#
+
+secret k : Function;
+
+usertype Ticket, Key;
+
+
+protocol yahalomPaulson(I,R,S)
+{
+	role I
+	{
+		const Ni: Nonce;
+		var Nr: Nonce;
+		var T: Ticket;
+		var Kir: Key;
+
+		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_I1(I, Secret,Kir);
+		claim_I2(I, Nisynch);
+	}
+
+	role R
+	{
+		const Nr: Nonce;
+		var Ni: Nonce;
+		var T: Ticket;
+		var Kir: Key;
+
+		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_R1(R, Secret,Kir);
+        claim_R2(R, Nisynch);
+	}
+
+	role S
+	{
+		const Kir: Key;
+		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) );
+	}
+}
+
+const Alice,Bob,Simon : Agent;
+
+run yahalomPaulson.I(Agent,Agent,s);
+run yahalomPaulson.I(Agent,Agent,s);
+run yahalomPaulson.R(Agent,Agent,s);
+
diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl
new file mode 100644
index 0000000..126f5f3
--- /dev/null
+++ b/spdl/SPORE/yahalom.spdl
@@ -0,0 +1,63 @@
+# Yahalom
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/yahalom.html
+#
+# Note:
+# This protocol uses a ticket so scyther will only be able to verify
+# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2)
+#
+
+secret k : Function;
+
+usertype Ticket, Key;
+
+
+protocol yahalom(I,R,S)
+{
+	role I
+	{
+		const Ni: Nonce;
+		var Nr: Nonce;
+		var T: Ticket;
+		var Kir: Key;
+
+		send_1(I,R, I,Ni);
+		read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T );
+		send_4(I,R, T, {Nr}Kir );
+
+		claim_I1(I, Secret,Kir);
+		claim_I2(I, Nisynch);
+	}
+
+	role R
+	{
+		const Nr: Nonce;
+		var Ni: Nonce;
+		var T: Ticket;
+		var Kir: Key;
+
+		read_1(I,R, I,Ni);
+		send_2(R,S, R, {I,Ni,Nr}k(R,S) );
+		read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir );
+
+		claim_R1(R, Secret,Kir);
+        claim_R2(R, Nisynch);
+	}
+
+	role S
+	{
+		const Kir: Key;
+		var Ni,Nr: Nonce;
+
+		read_2(R,S, R, {I,Ni,Nr}k(R,S) );
+		send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
+	}
+}
+
+const Alice,Bob,Simon : Agent;
+
+run yahalom.I(Agent,Agent,s);
+run yahalom.I(Agent,Agent,s);
+run yahalom.R(Agent,Agent,s);
+