- Adding Wide Mouther Frog and modified versions

spdl/SPORE/wmf-lowe.spdl

@@ -0,0 +1,74 @@
+# Lowe modified Wide Mouthed Frog
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/wideMouthedFrogLowe.html
+#
+# Note:
+# According to SPORE there are no known attacks on this protocol, scyther
+# finds one however this has to do with the unusual assumption that every 
+# agent can recognise and will reject to read messages that it has created
+# itself.
+
+usertype Key;
+usertype TimeStamp;
+const succ,pred: Function;
+inversekeys (succ,pred);
+
+secret k: Function;
+
+protocol wmfLowe(I,R,S)
+{
+	role I
+	{
+		const Kir: Key;
+        const Ti: TimeStamp;
+		var Kr: Key;
+        var Nr: Nonce;
+
+		send_1(I,S, I, {Ti, R, Kir}k(I,S)); 
+        read_3(R,I,{Nr}Kir);
+        send_4(I,R,{{Nr}succ}Kir);
+
+		claim_I1(I,Secret,Kir);
+        claim_I2(I,Nisynch);
+	}	
+	
+	role R
+	{
+        var Ts: TimeStamp;
+        var Kir: Key;
+        const Nr: Nonce;
+
+		read_2(S,R, {Ts, I, Kir}k(R,S) );
+        send_3(R,I, {Nr}Kir);
+        read_4(I,R, {{Nr}succ}Kir);
+
+		claim_R1(R,Secret,Kir);
+        claim_R2(R,Nisynch);
+	}
+
+	role S
+	{
+		var Kir: Key;
+        const Ts: TimeStamp;
+        var Ti: TimeStamp;
+
+		read_1(I,S, I,{Ti, R, Kir}k(I,S) );
+        send_2(S,R, {Ts, I, Kir}k(R,S));
+	}
+}
+
+const Alice,Bob,Eve,Simon: Agent;
+const Ke: Key;
+const Te: TimeStamp;
+
+
+untrusted Eve;
+compromised k(Eve,Simon);
+
+run wmfLowe.I (Agent,Agent,Simon);
+run wmfLowe.R (Agent,Agent,Simon);
+run wmfLowe.S (Agent,Agent,Simon);
+
+
+

spdl/SPORE/wmf.spdl

@@ -0,0 +1,60 @@
+# Wide Mouthed Frog
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/wideMouthedFrog.html
+#
+
+usertype Key;
+usertype TimeStamp;
+
+secret k: Function;
+
+protocol wmf(I,R,S)
+{
+	role I
+	{
+		const Kir: Key;
+        const Ti: TimeStamp;
+		var Kr: Key;
+
+		send_1(I,S, I, {Ti, R, Kir}k(I,S)); 
+
+		claim_I1(I,Secret,Kir);
+	}	
+	
+	role R
+	{
+        var Ts: TimeStamp;
+        var Kir: Key;
+
+		read_2(S,R, {Ts, I, Kir}k(R,S) );
+
+		claim_R1(R,Secret,Kir);
+        claim_R2(R,Nisynch);
+	}
+
+	role S
+	{
+		var Kir: Key;
+        const Ts: TimeStamp;
+        var Ti: TimeStamp;
+
+		read_1(I,S, I,{Ti, R, Kir}k(I,S) );
+        send_2(S,R, {Ts, I, Kir}k(R,S));
+	}
+}
+
+const Alice,Bob,Eve,Simon: Agent;
+const Ke: Key;
+const Te: TimeStamp;
+
+
+untrusted Eve;
+compromised k(Eve,Simon);
+
+run wmf.I (Agent,Agent,Simon);
+run wmf.R (Agent,Agent,Simon);
+run wmf.S (Agent,Agent,Simon);
+
+
+