diff --git a/spdl/bunava-2-4.spdl b/spdl/bunava-2-4.spdl
new file mode 100644
index 0000000..68e5fe4
--- /dev/null
+++ b/spdl/bunava-2-4.spdl
@@ -0,0 +1,138 @@
+# Buttyan Nagy Vajda protocol 2 (4-party)
+#
+# Modelled after the description in the paper
+# "Efficient multi-party challenge-response protocols for entity
+# authentication"
+#
+# Note:
+# Does not seem to reach the claim. I don't know why yet. TODO
+# investigate.
+#
+
+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 bunava24(A,B,C,D)
+{
+    role A
+    {
+        const ra: Nonce;
+	var rb,rc,rd: Nonce;
+        var Tacd, Tabd: Ticket;
+
+	send_1(A,B, ra);
+	read_4(D,A, rd,
+	    Tacd,
+	    Tabd,
+	    { D, { C, { B,ra }k(A,B) }k(A,C) }k(A,D)
+	    );
+#	send_5(A,B,
+#	    { A, rd }k(A,D),
+#	    { A, Tacd }k(A,C),
+#	    { A, Tabd }k(A,B)
+#	    );
+
+	claim_A1(A, Niagree);
+	claim_A2(A, Nisynch);
+    }
+
+    role B
+    {
+        const rb: Nonce;
+	var ra,rc,rd: Nonce;
+        var Tbad, Tbac: Ticket;
+
+	read_1(A,B, ra);
+	send_2(B,C, rb,
+	    { B,ra }k(A,B)
+	    );
+#	read_5(A,B,
+#	    Tbad,
+#	    Tbac,
+#	    { A, { D, { C,rb }k(B,C) }k(B,D) }k(A,B)
+#	    );
+#	send_6(B,C,
+#	    { B, Tbad }k(B,D),
+#	    { B, Tbac }k(B,C)
+#	    );
+#
+#	claim_B1(B, Niagree);
+#	claim_B2(B, Nisynch);
+    }
+
+    role C
+    {
+        const rc: Nonce;
+	var ra,rb,rd: Nonce;
+        var Tcab,Tcbd: Ticket;
+
+	read_2(B,C, rb, Tcab );
+	send_3(C,D, rc,
+	    { C, rb }k(B,C),
+	    { C, Tcab }k(A,C)
+	    );
+#	read_6(B,C,
+#	    Tcbd,
+#	    { B, { A,{ D,rc }k(C,D) }k(A,C) }k(B,C)
+#	    );
+#	send_7(C,D,
+#	    { C, Tcbd }k(C,D)
+#	    );
+#
+#	claim_C1(C, Niagree);
+#	claim_C2(C, Nisynch);
+    }
+
+    role D
+    {
+        const rd: Nonce;
+	var ra,rb,rc: Nonce;
+        var Tdbc,Tdac: Ticket;
+
+	read_3(C,D, rc, Tdbc, Tdac );
+	send_4(D,A, rd,
+	    { D, rc }k(C,D),
+	    { D, Tdbc }k(B,D),
+	    { D, Tdac }k(A,D)
+	    );
+#	read_7(C,D,
+#	    { C, { B,{ A,rd }k(A,D) }k(B,D) }k(C,D)
+#	    );
+#
+#	claim_D1(D, Niagree);
+#	claim_D2(D, 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
+ 
+run bunava24.A(Agent,Agent,Agent,Agent);
+run bunava24.B(Agent,Agent,Agent,Agent);
+run bunava24.C(Agent,Agent,Agent,Agent);
+run bunava24.D(Agent,Agent,Agent,Agent);
+run bunava24.A(Agent,Agent,Agent,Agent);
+run bunava24.B(Agent,Agent,Agent,Agent);
+run bunava24.C(Agent,Agent,Agent,Agent);
+run bunava24.D(Agent,Agent,Agent,Agent);