diff --git a/protocols/SPORE/NotModelled.txt b/gui/Protocols/NotModelled.txt similarity index 100% rename from protocols/SPORE/NotModelled.txt rename to gui/Protocols/NotModelled.txt diff --git a/protocols/SPORE/andrew-ban-concrete.spdl b/gui/Protocols/andrew-ban-concrete.spdl similarity index 100% rename from protocols/SPORE/andrew-ban-concrete.spdl rename to gui/Protocols/andrew-ban-concrete.spdl diff --git a/protocols/SPORE/andrew-ban.spdl b/gui/Protocols/andrew-ban.spdl similarity index 100% rename from protocols/SPORE/andrew-ban.spdl rename to gui/Protocols/andrew-ban.spdl diff --git a/protocols/SPORE/andrew-lowe-ban.spdl b/gui/Protocols/andrew-lowe-ban.spdl similarity index 100% rename from protocols/SPORE/andrew-lowe-ban.spdl rename to gui/Protocols/andrew-lowe-ban.spdl diff --git a/protocols/SPORE/andrew.spdl b/gui/Protocols/andrew.spdl similarity index 100% rename from protocols/SPORE/andrew.spdl rename to gui/Protocols/andrew.spdl diff --git a/protocols/SPORE/ccitt509-1.spdl b/gui/Protocols/ccitt509-1.spdl similarity index 100% rename from protocols/SPORE/ccitt509-1.spdl rename to gui/Protocols/ccitt509-1.spdl diff --git a/protocols/SPORE/ccitt509-1c.spdl b/gui/Protocols/ccitt509-1c.spdl similarity index 100% rename from protocols/SPORE/ccitt509-1c.spdl rename to gui/Protocols/ccitt509-1c.spdl diff --git a/protocols/SPORE/ccitt509-3.spdl b/gui/Protocols/ccitt509-3.spdl similarity index 100% rename from protocols/SPORE/ccitt509-3.spdl rename to gui/Protocols/ccitt509-3.spdl diff --git a/protocols/SPORE/ccitt509-ban3.spdl b/gui/Protocols/ccitt509-ban3.spdl similarity index 100% rename from protocols/SPORE/ccitt509-ban3.spdl rename to gui/Protocols/ccitt509-ban3.spdl diff --git a/protocols/SPORE/denning-sacco-lowe.spdl b/gui/Protocols/denning-sacco-lowe.spdl similarity index 100% rename from protocols/SPORE/denning-sacco-lowe.spdl rename to gui/Protocols/denning-sacco-lowe.spdl diff --git a/protocols/SPORE/denning-sacco.spdl b/gui/Protocols/denning-sacco.spdl similarity index 100% rename from protocols/SPORE/denning-sacco.spdl rename to gui/Protocols/denning-sacco.spdl diff --git a/protocols/SPORE/kaochow-v2.spdl b/gui/Protocols/kaochow-v2.spdl similarity index 100% rename from protocols/SPORE/kaochow-v2.spdl rename to gui/Protocols/kaochow-v2.spdl diff --git a/protocols/SPORE/kaochow-v3.spdl b/gui/Protocols/kaochow-v3.spdl similarity index 100% rename from protocols/SPORE/kaochow-v3.spdl rename to gui/Protocols/kaochow-v3.spdl diff --git a/protocols/SPORE/kaochow.spdl b/gui/Protocols/kaochow.spdl similarity index 100% rename from protocols/SPORE/kaochow.spdl rename to gui/Protocols/kaochow.spdl diff --git a/protocols/SPORE/ksl-lowe.spdl b/gui/Protocols/ksl-lowe.spdl similarity index 100% rename from protocols/SPORE/ksl-lowe.spdl rename to gui/Protocols/ksl-lowe.spdl diff --git a/protocols/SPORE/ksl.spdl b/gui/Protocols/ksl.spdl similarity index 100% rename from protocols/SPORE/ksl.spdl rename to gui/Protocols/ksl.spdl diff --git a/protocols/SPORE/needham-schroeder-lowe.spdl b/gui/Protocols/needham-schroeder-lowe.spdl similarity index 100% rename from protocols/SPORE/needham-schroeder-lowe.spdl rename to gui/Protocols/needham-schroeder-lowe.spdl diff --git a/protocols/SPORE/needham-schroeder-sk-amend.spdl b/gui/Protocols/needham-schroeder-sk-amend.spdl similarity index 100% rename from protocols/SPORE/needham-schroeder-sk-amend.spdl rename to gui/Protocols/needham-schroeder-sk-amend.spdl diff --git a/protocols/SPORE/needham-schroeder-sk.spdl b/gui/Protocols/needham-schroeder-sk.spdl similarity index 100% rename from protocols/SPORE/needham-schroeder-sk.spdl rename to gui/Protocols/needham-schroeder-sk.spdl diff --git a/protocols/SPORE/needham-schroeder.spdl b/gui/Protocols/needham-schroeder.spdl similarity index 100% rename from protocols/SPORE/needham-schroeder.spdl rename to gui/Protocols/needham-schroeder.spdl diff --git a/protocols/SPORE/neumannstub-guttman-hwang.spdl b/gui/Protocols/neumannstub-guttman-hwang.spdl similarity index 100% rename from protocols/SPORE/neumannstub-guttman-hwang.spdl rename to gui/Protocols/neumannstub-guttman-hwang.spdl diff --git a/protocols/SPORE/neumannstub-guttman.spdl b/gui/Protocols/neumannstub-guttman.spdl similarity index 100% rename from protocols/SPORE/neumannstub-guttman.spdl rename to gui/Protocols/neumannstub-guttman.spdl diff --git a/protocols/SPORE/neumannstub-hwang.spdl b/gui/Protocols/neumannstub-hwang.spdl similarity index 100% rename from protocols/SPORE/neumannstub-hwang.spdl rename to gui/Protocols/neumannstub-hwang.spdl diff --git a/protocols/SPORE/neumannstub-keycompromise.spdl b/gui/Protocols/neumannstub-keycompromise.spdl similarity index 100% rename from protocols/SPORE/neumannstub-keycompromise.spdl rename to gui/Protocols/neumannstub-keycompromise.spdl diff --git a/protocols/SPORE/neumannstub.spdl b/gui/Protocols/neumannstub.spdl similarity index 100% rename from protocols/SPORE/neumannstub.spdl rename to gui/Protocols/neumannstub.spdl diff --git a/protocols/SPORE/otwayrees.spdl b/gui/Protocols/otwayrees.spdl similarity index 100% rename from protocols/SPORE/otwayrees.spdl rename to gui/Protocols/otwayrees.spdl diff --git a/protocols/SPORE/smartright.spdl b/gui/Protocols/smartright.spdl similarity index 100% rename from protocols/SPORE/smartright.spdl rename to gui/Protocols/smartright.spdl diff --git a/protocols/SPORE/splice-as-cj.spdl b/gui/Protocols/splice-as-cj.spdl similarity index 100% rename from protocols/SPORE/splice-as-cj.spdl rename to gui/Protocols/splice-as-cj.spdl diff --git a/protocols/SPORE/splice-as-hc.spdl b/gui/Protocols/splice-as-hc.spdl similarity index 100% rename from protocols/SPORE/splice-as-hc.spdl rename to gui/Protocols/splice-as-hc.spdl diff --git a/protocols/SPORE/splice-as.spdl b/gui/Protocols/splice-as.spdl similarity index 100% rename from protocols/SPORE/splice-as.spdl rename to gui/Protocols/splice-as.spdl diff --git a/protocols/SPORE/tmn.spdl b/gui/Protocols/tmn.spdl similarity index 100% rename from protocols/SPORE/tmn.spdl rename to gui/Protocols/tmn.spdl diff --git a/protocols/SPORE/wmf-lowe.spdl b/gui/Protocols/wmf-lowe.spdl similarity index 100% rename from protocols/SPORE/wmf-lowe.spdl rename to gui/Protocols/wmf-lowe.spdl diff --git a/protocols/SPORE/wmf.spdl b/gui/Protocols/wmf.spdl similarity index 100% rename from protocols/SPORE/wmf.spdl rename to gui/Protocols/wmf.spdl diff --git a/protocols/SPORE/woo-lam-pi-1.spdl b/gui/Protocols/woo-lam-pi-1.spdl similarity index 100% rename from protocols/SPORE/woo-lam-pi-1.spdl rename to gui/Protocols/woo-lam-pi-1.spdl diff --git a/protocols/SPORE/woo-lam-pi-2.spdl b/gui/Protocols/woo-lam-pi-2.spdl similarity index 100% rename from protocols/SPORE/woo-lam-pi-2.spdl rename to gui/Protocols/woo-lam-pi-2.spdl diff --git a/protocols/SPORE/woo-lam-pi-3.spdl b/gui/Protocols/woo-lam-pi-3.spdl similarity index 100% rename from protocols/SPORE/woo-lam-pi-3.spdl rename to gui/Protocols/woo-lam-pi-3.spdl diff --git a/protocols/SPORE/woo-lam-pi-f.spdl b/gui/Protocols/woo-lam-pi-f.spdl similarity index 100% rename from protocols/SPORE/woo-lam-pi-f.spdl rename to gui/Protocols/woo-lam-pi-f.spdl diff --git a/protocols/SPORE/woo-lam-pi.spdl b/gui/Protocols/woo-lam-pi.spdl similarity index 100% rename from protocols/SPORE/woo-lam-pi.spdl rename to gui/Protocols/woo-lam-pi.spdl diff --git a/protocols/SPORE/woo-lam.spdl b/gui/Protocols/woo-lam.spdl similarity index 100% rename from protocols/SPORE/woo-lam.spdl rename to gui/Protocols/woo-lam.spdl diff --git a/protocols/SPORE/yahalom-ban.spdl b/gui/Protocols/yahalom-ban.spdl similarity index 100% rename from protocols/SPORE/yahalom-ban.spdl rename to gui/Protocols/yahalom-ban.spdl diff --git a/protocols/SPORE/yahalom-lowe.spdl b/gui/Protocols/yahalom-lowe.spdl similarity index 100% rename from protocols/SPORE/yahalom-lowe.spdl rename to gui/Protocols/yahalom-lowe.spdl diff --git a/protocols/SPORE/yahalom-paulson.spdl b/gui/Protocols/yahalom-paulson.spdl similarity index 100% rename from protocols/SPORE/yahalom-paulson.spdl rename to gui/Protocols/yahalom-paulson.spdl diff --git a/protocols/SPORE/yahalom.spdl b/gui/Protocols/yahalom.spdl similarity index 100% rename from protocols/SPORE/yahalom.spdl rename to gui/Protocols/yahalom.spdl diff --git a/protocols/SPORE/key-compromise/needham-schroeder-sk.spdl b/protocols/SPORE/key-compromise/needham-schroeder-sk.spdl deleted file mode 100644 index c461405..0000000 --- a/protocols/SPORE/key-compromise/needham-schroeder-sk.spdl +++ /dev/null @@ -1,88 +0,0 @@ -# Needham Schroeder Symmetric Key -# -# Modelled after the description in the SPORE library -# http://www.lsv.ens-cachan.fr/spore/nssk.html -# -# -# Note: -# This protocol uses a ticket so scyther will only be able to verify -# the protocol using the ARACHNE engine (-a) -# - - -secret k: Function; -# Model dec that is invertible by inc -const dec,inc: Function; -inversekeys(dec,inc); -usertype SessionKey; -const Fresh: Function; -const Compromised: Function; - -protocol needhamschroederSessionKeyCompromise(C) -{ - // Read the names of 3 agents and disclose a session between them including - // corresponding session key to simulate key compromise - role C { - const Ni,Nr: Nonce; - const Kir: SessionKey; - var I,R,S: Agent; - - read_!C1(C,C, I,R,S); - send_!C2(C,C, (I,R,Ni), - {Ni,R,Kir,{Kir,I}k(R,S)}k(I,S), - {Kir,I}k(R,S), - {Nr}Kir, - {{Nr}dec}Kir, - Kir - ); - claim_C3(C,Empty, (Compromised,Kir)); - } -} - -protocol needhamschroedersk(I,R,S) -{ - role I - { - const Ni: Nonce; - var Nr: Nonce; - var Kir: SessionKey; - var T: Ticket; - - send_1(I,S,(I,R,Ni)); - read_2(S,I, {Ni,R,Kir,T}k(I,S)); - send_3(I,R,T); - read_4(R,I,{Nr}Kir); - send_5(I,R,{{Nr}dec}Kir); - claim_I2(I,Secret,Kir); - claim_I3(I,Nisynch); - claim_I4(I,Empty,(Fresh,Kir)); - } - - role R - { - const Nr: Nonce; - var Kir: SessionKey; - - read_3(I,R,{Kir,I}k(R,S)); - send_4(R,I,{Nr}Kir); - read_5(I,R,{{Nr}dec}Kir); - claim_R1(R,Secret,Kir); - claim_R3(R,Nisynch); - claim_R4(R,Empty,(Fresh,Kir)); - } - - role S - { - var Ni: Nonce; - const Kir: SessionKey; - read_1(I,S,(I,R,Ni)); - send_2(S,I,{Ni,R,Kir,{Kir,I}k(R,S)}k(I,S)); - } -} - -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised k(Eve,Simon); -