From 5ddcbd0fe528852529e12f41a22ea7b31b89807d Mon Sep 17 00:00:00 2001
From: gijs <gijs@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 18 May 2005 12:17:08 +0000
Subject: [PATCH] - Adding Wide Mouther Frog and modified versions

---
 spdl/SPORE/wmf-lowe.spdl | 74 ++++++++++++++++++++++++++++++++++++++++
 spdl/SPORE/wmf.spdl      | 60 ++++++++++++++++++++++++++++++++
 2 files changed, 134 insertions(+)
 create mode 100644 spdl/SPORE/wmf-lowe.spdl
 create mode 100644 spdl/SPORE/wmf.spdl

diff --git a/spdl/SPORE/wmf-lowe.spdl b/spdl/SPORE/wmf-lowe.spdl
new file mode 100644
index 0000000..a74118d
--- /dev/null
+++ b/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);
+
+
+
diff --git a/spdl/SPORE/wmf.spdl b/spdl/SPORE/wmf.spdl
new file mode 100644
index 0000000..cd953ff
--- /dev/null
+++ b/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);
+
+
+