diff --git a/spdl/woolam-pi-f.spdl b/spdl/woolam-pi-f.spdl new file mode 100644 index 0000000..cd67d0f --- /dev/null +++ b/spdl/woolam-pi-f.spdl @@ -0,0 +1,55 @@ +/* + * Woo-lam version from Spore, Pi f + * + * Only one-way verification + */ + +usertype Server, SessionKey, Ticket; +secret k: Function; + +const Alice, Bob, Charlie, Eve: Agent; +const Simon: Server; + +const ne: Nonce; +const ke: SessionKey; +untrusted Eve; +compromised k(Eve,Simon); + +protocol woolampif(A,B,S) +{ + role A + { + var Nb: Nonce; + + send_1(A,B, A); + read_2(B,A, Nb); + send_3(A,B, { A,B,Nb }k(A,S) ); + } + + role B + { + const Nb: Nonce; + var T: Ticket; + + read_1(A,B, A); + send_2(B,A, Nb); + read_3(A,B, T); + send_4(B,S, { A,B,Nb, T }k(B,S) ); + read_5(S,B, { A,B,Nb }k(B,S) ); + + claim_6(B,Niagree); + claim_7(B,Nisynch); + } + + role S + { + var Nb: Nonce; + + read_4(B,S, { A,B,Nb, { A,B,Nb }k(A,S) }k(B,S) ); + send_5(S,B, { A,B,Nb }k(B,S) ); + } +} + +run woolampif.B(Alice,Bob,Simon); +run woolampif.B(Alice,Bob,Simon); + diff --git a/test/protocollist.py b/test/protocollist.py index 8b11013..674e563 100644 --- a/test/protocollist.py +++ b/test/protocollist.py @@ -40,6 +40,7 @@ def from_literature(): "wmf-brutus.spdl", "woolam-ce.spdl", "woolam-cmv.spdl", + "woolam-pi-f.spdl", "yahalom-ban.spdl", "yahalom-lowe.spdl", "yahalom-paulson.spdl",