diff --git a/spdl/bunava-2-3.spdl b/spdl/bunava-2-3.spdl new file mode 100644 index 0000000..2b36df5 --- /dev/null +++ b/spdl/bunava-2-3.spdl @@ -0,0 +1,88 @@ +# Buttyan Nagy Vajda protocol 2 (3-party) +# +# Modelled after the description in the paper +# "Efficient multi-party challenge-response protocols for entity +# authentication" +# +# Attacks: +# + +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 bunava23(A,B,C) +{ + role A + { + const ra: Nonce; + var rb,rc: Nonce; + var Ta: Ticket; + + send_1(A,B, ra); + read_3(C,A, rc, Ta, { C,{ B,ra }k(A,B) }k(A,C) ); + send_4(A,B, { A,rc }k(A,C), { A, Ta }k(A,B) ); + + claim_A1(A, Niagree); + claim_A2(A, Nisynch); + } + + role B + { + const rb: Nonce; + var ra,rc: Nonce; + var Tb: Ticket; + + read_1(A,B, ra); + send_2(B,C, rb,{B,ra}k(B,C) ); + read_4(A,B, Tb, { A, { C,rb }k(B,C) }k(A,B) ); + send_5(B,C, { B, Tb }k(B,C) ); + + claim_B1(B, Niagree); + claim_B2(B, Nisynch); + } + + role C + { + const rc: Nonce; + var ra,rb: Nonce; + var Tc: Ticket; + + read_2(B,C, rb, Tc ); + send_3(C,A, rc,{ C,rb }k(B,C), { C, Tc }k(A,C) ); + read_5(B,C, { B, { A,rc }k(A,C) }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 + +run bunava23.A(Agent,Agent,Agent); +run bunava23.B(Agent,Agent,Agent); +run bunava23.C(Agent,Agent,Agent); +run bunava23.A(Agent,Agent,Agent); +run bunava23.B(Agent,Agent,Agent); +run bunava23.C(Agent,Agent,Agent);