- Adding Yahalom and variants

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