From 5570389c16ec87c6e8802988e5cd51d572b1fcd0 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Mon, 23 May 2005 10:36:42 +0000
Subject: [PATCH] - A first generalization of NSL.

---
 spdl/nsl-generalized-4.spdl | 99 +++++++++++++++++++++++++++++++++++++
 1 file changed, 99 insertions(+)
 create mode 100644 spdl/nsl-generalized-4.spdl

diff --git a/spdl/nsl-generalized-4.spdl b/spdl/nsl-generalized-4.spdl
new file mode 100644
index 0000000..e03a3e5
--- /dev/null
+++ b/spdl/nsl-generalized-4.spdl
@@ -0,0 +1,99 @@
+/*
+ * Generalized Needham-Schroeder-Lowe protocol.
+ * Four-party version.
+ *
+ * Cas Cremers
+ * Mon May 23 11:49:29 CEST 2005
+ */
+
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+protocol nslgen4(R1,R2,R3,R4)
+{
+	role R1
+	{
+		const n1: Nonce;
+		var n2,n3,n4: Nonce;
+
+		send_1(R1,R2, {R1,R3,R4,n1}pk(R2) );
+		read_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
+		send_5(R1,R2, {n2,n3,n4,R3,R4}pk(R2) );
+
+		claim_r1a(R1,Secret,n1);
+		claim_r1b(R1,Secret,n2);
+		claim_r1c(R1,Secret,n3);
+		claim_r1d(R1,Secret,n4);
+
+		claim_r1A(R1,Niagree);
+		claim_r1S(R1,Nisynch);
+	}	
+	
+	role R2
+	{
+		const n2: Nonce;
+		var n1,n3,n4: Nonce;
+
+		read_1(R1,R2, {R1,R3,R4,n1}pk(R2) );
+		send_2(R2,R3, {n1,n2,R1,R2,R4}pk(R3) );
+		read_5(R1,R2, {n2,n3,n4,R3,R4}pk(R2) );
+		send_6(R2,R3, {n3,n4,R4}pk(R3) );
+
+		claim_r2a(R2,Secret,n1);
+		claim_r2b(R2,Secret,n2);
+		claim_r2c(R2,Secret,n3);
+		claim_r2d(R2,Secret,n4);
+
+		claim_r2A(R2,Niagree);
+		claim_r2S(R2,Nisynch);
+	}
+
+	role R3
+	{
+		const n3: Nonce;
+		var n1,n2,n4: Nonce;
+
+		read_2(R2,R3, {n1,n2,R1,R2,R4}pk(R3) );
+		send_3(R3,R4, {n1,n2,n3,R1,R2,R3}pk(R4) );
+		read_6(R2,R3, {n3,n4,R4}pk(R3) );
+		send_7(R3,R4, {n4}pk(R4) );
+
+		claim_r3a(R3,Secret,n1);
+		claim_r3b(R3,Secret,n2);
+		claim_r3c(R3,Secret,n3);
+		claim_r3d(R3,Secret,n4);
+
+		claim_r3A(R3,Niagree);
+		claim_r3S(R3,Nisynch);
+	}
+
+	role R4
+	{
+		const n4: Nonce;
+		var n1,n2,n3: Nonce;
+
+		read_3(R3,R4, {n1,n2,n3,R1,R2,R3}pk(R4) );
+		send_4(R4,R1, {n1,n2,n3,n4,R2,R3,R4}pk(R1) );
+		read_7(R3,R4, {n4}pk(R4) );
+
+		claim_r4a(R4,Secret,n1);
+		claim_r4b(R4,Secret,n2);
+		claim_r4c(R4,Secret,n3);
+		claim_r4d(R4,Secret,n4);
+
+		claim_r4A(R4,Niagree);
+		claim_r4S(R4,Nisynch);
+	}
+}
+
+const Alice,Bob,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+compromised sk(Eve);
+
+run nslgen4.R1(Agent,Agent,Agent,Agent);
+run nslgen4.R2(Agent,Agent,Agent,Agent);
+run nslgen4.R3(Agent,Agent,Agent,Agent);
+run nslgen4.R4(Agent,Agent,Agent,Agent);