From 52e38f40e6e194ca4d6b22fed6742e9307a67c60 Mon Sep 17 00:00:00 2001
From: gijs <gijs@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Thu, 12 May 2005 12:27:18 +0000
Subject: [PATCH] Fixed scenario for needham-schroeder and added
 needham-shroeder-lowe

---
 spdl/SPORE/needham-schroeder-lowe.spdl | 69 ++++++++++++++++++++++++++
 spdl/SPORE/needham-schroeder.spdl      | 14 +++---
 2 files changed, 77 insertions(+), 6 deletions(-)
 create mode 100644 spdl/SPORE/needham-schroeder-lowe.spdl

diff --git a/spdl/SPORE/needham-schroeder-lowe.spdl b/spdl/SPORE/needham-schroeder-lowe.spdl
new file mode 100644
index 0000000..6b6393a
--- /dev/null
+++ b/spdl/SPORE/needham-schroeder-lowe.spdl
@@ -0,0 +1,69 @@
+# Lowe's fixed version of Needham Schroeder Public Key
+#
+# Modelled after the description in the SPORE library
+# http://www.lsv.ens-cachan.fr/spore/nspkLowe.html
+#
+#
+# Note:
+# The modelling in SPORE includes a server to distribute the public keys
+# of the agents, this is not necessary and it allows for attacks against
+# synchronisation and agreement, because the keys that the server sends
+# out can be replayed.
+
+const pk: Function;
+secret sk: Function;
+inversekeys(pk,sk);
+
+protocol needhamschroederpkLowe(I,R,S)
+{
+	role I
+	{
+        const Ni: Nonce;
+        var Nr: Nonce;
+
+		send_1(I,S, (I,R));
+        read_2(S,I, {pk(R), R}sk(S));
+        send_3(I,R,{Ni,I}pk(R));
+        read_6(R,I, {Ni,Nr,R}pk(I));
+        send_7(I,R, {Nr}pk(R));
+        claim_I1(I,Secret,Ni);
+        claim_I2(I,Secret,Nr);
+	}	
+	
+	role R
+	{
+        const Nr: Nonce;
+        var Ni: Nonce;
+        
+        read_3(I,R,{Ni,I}pk(R));
+        send_4(R,S,(R,I));
+        read_5(S,R,{pk(I),I}sk(S));
+        send_6(R,I,{Ni,Nr,R}pk(I));
+        read_7(I,R,{Nr}pk(R));
+        claim_R1(R,Secret,Nr);
+        claim_R2(R,Secret,Ni);
+	}
+
+    role S
+    {
+        read_1(I,S,(I,R));
+        send_2(S,I,{pk(R),R}sk(S));
+        read_4(R,S,(R,I));
+        send_5(S,R,{pk(I),I}sk(S));
+    }
+}
+
+const Alice,Bob,Simon,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+compromised sk(Eve);
+
+# General scenario, 2 parallel runs of the protocol
+ 
+run needhamschroederpkLowe.I(Agent,Agent,Simon);
+run needhamschroederpkLowe.S(Agent,Agent,Simon);
+run needhamschroederpkLowe.R(Agent,Agent,Simon);
+run needhamschroederpkLowe.I(Agent,Agent,Simon);
+run needhamschroederpkLowe.R(Agent,Agent,Simon);
+run needhamschroederpkLowe.S(Agent,Agent,Simon);
diff --git a/spdl/SPORE/needham-schroeder.spdl b/spdl/SPORE/needham-schroeder.spdl
index a0f07c8..b73385d 100644
--- a/spdl/SPORE/needham-schroeder.spdl
+++ b/spdl/SPORE/needham-schroeder.spdl
@@ -21,7 +21,7 @@ protocol needhamschroederpk(I,R,S)
         const Ni: Nonce;
         var Nr: Nonce;
 
-		send_1(I,S, (I,R));
+		send_1(I,S,(I,R));
         read_2(S,I, {pk(R), R}sk(S));
         send_3(I,R,{Ni,I}pk(R));
         read_6(R,I, {Ni, Nr}pk(I));
@@ -53,7 +53,7 @@ protocol needhamschroederpk(I,R,S)
     }
 }
 
-const Alice,Bob,Eve: Agent;
+const Alice,Bob,Simon,Eve: Agent;
 
 untrusted Eve;
 const ne: Nonce;
@@ -61,7 +61,9 @@ compromised sk(Eve);
 
 # General scenario, 2 parallel runs of the protocol
  
-run needhamschroederpk.I(Agent,Agent);
-run needhamschroederpk.R(Agent,Agent);
-run needhamschroederpk.I(Agent,Agent);
-run needhamschroederpk.R(Agent,Agent);
+run needhamschroederpk.I(Agent,Agent,Simon);
+run needhamschroederpk.R(Agent,Agent,Simon);
+run needhamschroederpk.S(Agent,Agent,Simon);
+run needhamschroederpk.I(Agent,Agent,Simon);
+run needhamschroederpk.R(Agent,Agent,Simon);
+run needhamschroederpk.S(Agent,Agent,Simon);