- Added the BuNaVa protocol 1.

spdl/bunava-1-3.spdl

@@ -0,0 +1,89 @@
+# Buttyan Nagy Vajda protocol 1 (3-party)
+#
+# Modelled after the description in the paper
+# "Efficient multi-party challenge-response protocols for entity
+# authentication"
+#
+# Attacks:
+# Does not satisfy ni-agree, because when Alice in the A role terminates
+# it cannot be sure that the agent in role B is aware of having sent a
+# reply for Alice.
+# A type flaw attack exists in which there are only two agents active.
+#
+
+secret k: Function;
+
+protocol intruderhelp(Swap)
+{
+    role Swap
+    {
+        var T: Ticket;
+	var A,B: Agent;
+
+	read_1(Swap,Swap, { T }k(A,B) );
+	send_2(Swap,Swap, { T }k(B,A) );
+    }
+}
+
+protocol bunava1(A,B,C)
+{
+    role A
+    {
+        const ra: Nonce;
+	var rb,rc: Nonce;
+
+	send_1(A,B, ra);
+	read_3(C,A, rc,{C,rb,B,ra}k(A,C) );
+	send_4(A,B, {A,rc,C,rb}k(A,B) );
+
+	claim_A1(A, Niagree);
+	claim_A2(A, Nisynch);
+    }
+
+    role B
+    {
+        const rb: Nonce;
+	var ra,rc: Nonce;
+
+	read_1(A,B, ra);
+	send_2(B,C, rb,{B,ra}k(B,C) );
+	read_4(A,B, {A,rc,C,rb}k(A,B) );
+	send_5(B,C, {B,A,rc}k(B,C) );
+
+	claim_B1(B, Niagree);
+	claim_B2(B, Nisynch);
+    }
+
+    role C
+    {
+        const rc: Nonce;
+	var ra,rb: Nonce;
+
+	read_2(B,C, rb,{B,ra}k(B,C) );
+	send_3(C,A, rc,{C,rb,B,ra}k(A,C) );
+	read_5(B,C, {B,A,rc}k(B,C) );
+
+	claim_C1(C, Niagree);
+	claim_C2(C, Nisynch);
+    }
+}
+
+const Alice,Bob,Charlie,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+compromised k(Alice,Eve);
+compromised k(Bob,Eve);
+compromised k(Charlie,Eve);
+compromised k(Eve,Alice);
+compromised k(Eve,Bob);
+compromised k(Eve,Charlie);
+
+# General scenario, 2 parallel runs of the protocol
+ 
+run bunava1.A(Agent,Agent,Agent);
+run bunava1.B(Agent,Agent,Agent);
+run bunava1.C(Agent,Agent,Agent);
+run bunava1.A(Agent,Agent,Agent);
+run bunava1.B(Agent,Agent,Agent);
+run bunava1.C(Agent,Agent,Agent);