From 0de515fd7d45caa5e7abe48a60972f2152cee5b1 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Sun, 21 Mar 2004 16:26:31 +0000
Subject: [PATCH] - Broken protocol for article.

---
 spdl/bke-broken.spdl | 61 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 61 insertions(+)
 create mode 100644 spdl/bke-broken.spdl

diff --git a/spdl/bke-broken.spdl b/spdl/bke-broken.spdl
new file mode 100644
index 0000000..66a76cc
--- /dev/null
+++ b/spdl/bke-broken.spdl
@@ -0,0 +1,61 @@
+/* 
+	Bilateral Key Exchange with Public Key protocol (BKEPK)
+
+	CMV version with explicit secrecy claims.
+*/
+
+usertype Key;
+
+const pk,hash: Function;
+secret sk,unhash: Function;
+
+inversekeys (pk,sk);
+inversekeys (hash,unhash);
+
+protocol bkepk(Initiator,Responder)
+{
+	role Initiator
+	{
+		const NI: Nonce;
+		var NR: Nonce;
+		var kab: Key;
+
+		send_1 (Initiator,Responder, { NI,Responder }pk(Responder) );
+		read_2 (Responder,Initiator, { hash(NI),NR,Responder,kab }pk(Initiator) );
+		send_3 (Initiator,Responder, { hash(NR) }kab );
+		claim_4 (Initiator, Secret, kab );
+	}
+
+	role Responder
+	{
+		var NI: Nonce;
+		const NR: Nonce;
+		const kab: Key;
+
+		read_1 (Initiator,Responder, { NI,Responder }pk(Responder) );
+		send_2 (Responder,Initiator, { hash(NI),NR,Responder,kab }pk(Initiator) );
+		read_3 (Initiator,Responder, { hash(NR) }kab );
+		claim_5 (Responder, Secret, kab );
+	}
+}
+
+const Alice,Bob,Eve: Agent;
+
+untrusted Eve;
+compromised sk(Eve);
+const ne: Nonce;
+
+run bkepk.Initiator(Alice,Agent);
+run bkepk.Responder(Agent,Bob);
+run bkepk.Initiator(Alice,Agent);
+run bkepk.Responder(Agent,Bob);
+
+run bkepk.Initiator(Alice,Agent);
+run bkepk.Responder(Agent,Bob);
+run bkepk.Initiator(Alice,Agent);
+run bkepk.Responder(Agent,Bob);
+
+run bkepk.Initiator(Alice,Agent);
+run bkepk.Responder(Agent,Bob);
+
+