From 2df76cd0a25820827d7b8c7264fd2e4c401b1a6e Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Tue, 16 Nov 2004 13:40:24 +0000
Subject: [PATCH] - Added a first try for the course protocol.

---
 spdl/unknown2.spdl | 69 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)
 create mode 100644 spdl/unknown2.spdl

diff --git a/spdl/unknown2.spdl b/spdl/unknown2.spdl
new file mode 100644
index 0000000..acfefcb
--- /dev/null
+++ b/spdl/unknown2.spdl
@@ -0,0 +1,69 @@
+usertype SessionKey;
+secret k: Function;
+
+protocol unknown2(I,R,S)
+{
+	role I
+	{
+		const ni: Nonce;
+		var nr: Nonce;
+		var kir: SessionKey;
+		var T;
+
+		send_1(I,R, ni );
+		read_3(S,I, { I,R,kir,ni,nr }k(I,S), T );
+		send_4(I,R, T, {nr}kir );
+
+		claim_i1(I,Nisynch);
+		claim_i2(I,Niagree);
+		claim_i3(I,Secret, kir);
+	}	
+	
+	role R
+	{
+		const nr: Nonce;
+		var ni: Nonce;
+		var kir: SessionKey;
+
+		read_1(I,R, ni );
+		send_2(R,S, { I,R,ni,nr }k(R,S) );
+		read_4(I,R, { I,R,kir,ni,nr }k(R,S), {nr}kir );
+
+		claim_r1(R,Nisynch);
+		claim_r2(R,Niagree);
+		claim_r3(R,Secret, kir);
+	}
+
+	role S
+	{
+		const kir: SessionKey;
+		var ni,nr: Nonce;
+
+		read_2(R,S, { I,R,ni,nr }k(R,S) );
+		send_3(S,I, { I,R,kir,ni,nr }k(I,S), { I,R,kir,ni,nr }k(R,S) );
+
+/*
+		claim_s1(S,Nisynch);
+		claim_s2(S,Niagree);
+		claim_s3(S,Secret, kir);
+		*/
+	}
+}
+
+const Alice,Bob,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+const kee: SessionKey;
+compromised k(Eve,Eve);
+compromised k(Eve,Alice);
+compromised k(Eve,Bob);
+compromised k(Alice,Eve);
+compromised k(Bob,Eve);
+
+run unknown2.I(Agent,Agent,Agent);
+run unknown2.R(Agent,Agent,Agent);
+run unknown2.S(Agent,Agent,Agent);
+run unknown2.R(Agent,Agent,Agent);
+run unknown2.I(Agent,Agent,Agent);
+run unknown2.S(Agent,Agent,Agent);