From b86c60240ccf42731d483f851d4006fe0bb68b98 Mon Sep 17 00:00:00 2001 From: gijs Date: Mon, 23 May 2005 12:00:33 +0000 Subject: [PATCH] - Adding more Woo Lam variants --- spdl/SPORE/woo-lam-pi-1.spdl | 63 ++++++++++++++++++++++++++++++++++++ spdl/SPORE/woo-lam-pi-2.spdl | 63 ++++++++++++++++++++++++++++++++++++ spdl/SPORE/woo-lam-pi-3.spdl | 63 ++++++++++++++++++++++++++++++++++++ spdl/SPORE/woo-lam-pi-f.spdl | 61 ++++++++++++++++++++++++++++++++++ 4 files changed, 250 insertions(+) create mode 100644 spdl/SPORE/woo-lam-pi-1.spdl create mode 100644 spdl/SPORE/woo-lam-pi-2.spdl create mode 100644 spdl/SPORE/woo-lam-pi-3.spdl create mode 100644 spdl/SPORE/woo-lam-pi-f.spdl diff --git a/spdl/SPORE/woo-lam-pi-1.spdl b/spdl/SPORE/woo-lam-pi-1.spdl new file mode 100644 index 0000000..21dee6d --- /dev/null +++ b/spdl/SPORE/woo-lam-pi-1.spdl @@ -0,0 +1,63 @@ +# Woo and Lam Pi 1 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamPi1.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2) +# + +usertype Ticket; + +secret k: Function; + +protocol woolamPi1(I,R,S) +{ + role I + { + var Nr: Nonce; + + send_1(I,R, I); + read_2(R,I, Nr); + send_3(I,R, {I,R,Nr}k(I,S)); + + } + + role R + { + const Nr: Nonce; + var T: Ticket; + + read_1(I,R, I); + send_2(R,I, Nr); + read_3(I,R, T); + send_4(R,S, {I,R, T}k(R,S)); + read_5(S,R, {I,R, Nr}k(R,S)); + + claim_R1(R,Nisynch); + } + + role S + { + var Nr: Nonce; + + read_4(R,S, {I,R, {I,R,Nr}k(I,S)}k(R,S)); + send_5(S,R, {I,R,Nr}k(R,S)); + } +} + +const Alice,Bob,Eve,Simon: Agent; +const Te: Ticket; +const Ne: Nonce; + + +untrusted Eve; +compromised k(Eve,Simon); + +run woolamPi1.I (Agent,Agent,Simon); +run woolamPi1.R (Agent,Agent,Simon); +run woolamPi1.S (Agent,Agent,Simon); + + + diff --git a/spdl/SPORE/woo-lam-pi-2.spdl b/spdl/SPORE/woo-lam-pi-2.spdl new file mode 100644 index 0000000..f885ec9 --- /dev/null +++ b/spdl/SPORE/woo-lam-pi-2.spdl @@ -0,0 +1,63 @@ +# Woo and Lam Pi 2 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamPi2.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2) +# + +usertype Ticket; + +secret k: Function; + +protocol woolamPi2(I,R,S) +{ + role I + { + var Nr: Nonce; + + send_1(I,R, I); + read_2(R,I, Nr); + send_3(I,R, {I,Nr}k(I,S)); + + } + + role R + { + const Nr: Nonce; + var T: Ticket; + + read_1(I,R, I); + send_2(R,I, Nr); + read_3(I,R, T); + send_4(R,S, {I, T}k(R,S)); + read_5(S,R, {I, Nr}k(R,S)); + + claim_R1(R,Nisynch); + } + + role S + { + var Nr: Nonce; + + read_4(R,S, {I, {I,Nr}k(I,S)}k(R,S)); + send_5(S,R, {I,Nr}k(R,S)); + } +} + +const Alice,Bob,Eve,Simon: Agent; +const Te: Ticket; +const Ne: Nonce; + + +untrusted Eve; +compromised k(Eve,Simon); + +run woolamPi2.I (Agent,Agent,Simon); +run woolamPi2.R (Agent,Agent,Simon); +run woolamPi2.S (Agent,Agent,Simon); + + + diff --git a/spdl/SPORE/woo-lam-pi-3.spdl b/spdl/SPORE/woo-lam-pi-3.spdl new file mode 100644 index 0000000..932afbf --- /dev/null +++ b/spdl/SPORE/woo-lam-pi-3.spdl @@ -0,0 +1,63 @@ +# Woo and Lam Pi 2 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamPi3.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2) +# + +usertype Ticket; + +secret k: Function; + +protocol woolamPi3(I,R,S) +{ + role I + { + var Nr: Nonce; + + send_1(I,R, I); + read_2(R,I, Nr); + send_3(I,R, {Nr}k(I,S)); + + } + + role R + { + const Nr: Nonce; + var T: Ticket; + + read_1(I,R, I); + send_2(R,I, Nr); + read_3(I,R, T); + send_4(R,S, {I, T}k(R,S)); + read_5(S,R, {I, Nr}k(R,S)); + + claim_R1(R,Nisynch); + } + + role S + { + var Nr: Nonce; + + read_4(R,S, {I, {Nr}k(I,S)}k(R,S)); + send_5(S,R, {I,Nr}k(R,S)); + } +} + +const Alice,Bob,Eve,Simon: Agent; +const Te: Ticket; +const Ne: Nonce; + + +untrusted Eve; +compromised k(Eve,Simon); + +run woolamPi3.I (Agent,Agent,Simon); +run woolamPi3.R (Agent,Agent,Simon); +run woolamPi3.S (Agent,Agent,Simon); + + + diff --git a/spdl/SPORE/woo-lam-pi-f.spdl b/spdl/SPORE/woo-lam-pi-f.spdl new file mode 100644 index 0000000..edbecfb --- /dev/null +++ b/spdl/SPORE/woo-lam-pi-f.spdl @@ -0,0 +1,61 @@ +# Woo and Lam Pi f +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamPif.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) and type 2 matching (-m2) +# + +usertype Ticket; + +secret k: Function; + +protocol woolamPif(I,R,S) +{ + role I + { + var Nr: Nonce; + + send_1(I,R, I); + read_2(R,I, Nr); + send_3(I,R, {I,R,Nr}k(I,S)); + + } + + role R + { + const Nr: Nonce; + var T: Ticket; + + read_1(I,R, I); + send_2(R,I, Nr); + read_3(I,R, T); + send_4(R,S, {I, R, Nr, T}k(R,S)); + read_5(S,R, {I, R, Nr}k(R,S)); + + claim_R1(R,Nisynch); + } + + role S + { + var Nr: Nonce; + + read_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S)); + send_5(S,R, {I, R, Nr}k(R,S)); + } +} + +const Alice,Bob,Eve,Simon: Agent; +const Te: Ticket; +const Ne: Nonce; + + +untrusted Eve; +compromised k(Eve,Simon); + +run woolamPif.I (Agent,Agent,Simon); +run woolamPif.R (Agent,Agent,Simon); +run woolamPif.S (Agent,Agent,Simon); +