From 46e46abb84e870ab06fbc2515e121c4f492d9cdb Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 13 Oct 2004 12:25:01 +0000
Subject: [PATCH] - Added andrew-ban and made the naming more consistent.

---
 spdl/andrew-ban.spdl      | 20 +++++++--------
 spdl/andrew-lowe-ban.spdl | 51 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 61 insertions(+), 10 deletions(-)
 create mode 100644 spdl/andrew-lowe-ban.spdl

diff --git a/spdl/andrew-ban.spdl b/spdl/andrew-ban.spdl
index af2a999..0c1801d 100644
--- a/spdl/andrew-ban.spdl
+++ b/spdl/andrew-ban.spdl
@@ -6,13 +6,13 @@ protocol andrewBan(I,R)
 	role I
 	{
 		const ni: Nonce;
-		var nr: Nonce;
+		var nr,nr2: Nonce;
 		var kir: SessionKey;
 
-		send_1(I,R, I,ni );
-		read_2(R,I, {ni,kir,I}k(I,R) );
-		send_3(I,R, {ni}kir );
-		read_4(R,I, nr );
+		send_1(I,R, I,{ni}k(I,R) );
+		read_2(R,I, {ni,nr}k(I,R) );
+		send_3(I,R, {nr}k(I,R) );
+		read_4(R,I, {kir,nr2,ni}k(I,R) );
 		claim_5(I,Nisynch);
 		claim_6(I,Secret, kir);
 		claim_7(I,Secret, k(I,R));
@@ -21,13 +21,13 @@ protocol andrewBan(I,R)
 	role R
 	{
 		var ni: Nonce;
-		const nr: Nonce;
+		const nr,nr2: Nonce;
 		const kir: SessionKey;
 
-		read_1(I,R, I,ni );
-		send_2(R,I, {ni,kir,I}k(I,R) );
-		read_3(I,R, {ni}kir );
-		send_4(R,I, nr );
+		read_1(I,R, I,{ni}k(I,R) );
+		send_2(R,I, {ni,nr}k(I,R) );
+		read_3(I,R, {nr}k(I,R) );
+		send_4(R,I, {kir,nr2,ni}k(I,R) );
 		claim_8(R,Nisynch);
 		claim_9(R,Secret, kir);
 		claim_10(R,Secret, k(I,R));
diff --git a/spdl/andrew-lowe-ban.spdl b/spdl/andrew-lowe-ban.spdl
new file mode 100644
index 0000000..09abd85
--- /dev/null
+++ b/spdl/andrew-lowe-ban.spdl
@@ -0,0 +1,51 @@
+usertype SessionKey;
+secret k: Function;
+
+protocol andrewLoweBan(I,R)
+{
+	role I
+	{
+		const ni: Nonce;
+		var nr: Nonce;
+		var kir: SessionKey;
+
+		send_1(I,R, I,ni );
+		read_2(R,I, {ni,kir,I}k(I,R) );
+		send_3(I,R, {ni}kir );
+		read_4(R,I, nr );
+		claim_5(I,Nisynch);
+		claim_6(I,Secret, kir);
+		claim_7(I,Secret, k(I,R));
+	}	
+	
+	role R
+	{
+		var ni: Nonce;
+		const nr: Nonce;
+		const kir: SessionKey;
+
+		read_1(I,R, I,ni );
+		send_2(R,I, {ni,kir,I}k(I,R) );
+		read_3(I,R, {ni}kir );
+		send_4(R,I, nr );
+		claim_8(R,Nisynch);
+		claim_9(R,Secret, kir);
+		claim_10(R,Secret, k(I,R));
+	}
+}
+
+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 andrewLoweBan.I(Agent,Agent);
+run andrewLoweBan.R(Agent,Agent);
+run andrewLoweBan.I(Agent,Agent);
+run andrewLoweBan.R(Agent,Agent);