diff --git a/protocols/misc/README.txt b/protocols/misc/README.txt new file mode 100644 index 0000000..386d6cc --- /dev/null +++ b/protocols/misc/README.txt @@ -0,0 +1,7 @@ + +The protocols in this directory are experimental and are not considered +to be stable in any way. Therefore, they should not be used as reference +models for experimenting with Scyther. Rather, use the protocols in +../SPORE or ../Demo. + + diff --git a/protocols/misc/trondheim/th-1.spdl b/protocols/misc/compositionality-examples/th-1.spdl similarity index 100% rename from protocols/misc/trondheim/th-1.spdl rename to protocols/misc/compositionality-examples/th-1.spdl diff --git a/protocols/misc/trondheim/th-1par2.spdl b/protocols/misc/compositionality-examples/th-1par2.spdl similarity index 100% rename from protocols/misc/trondheim/th-1par2.spdl rename to protocols/misc/compositionality-examples/th-1par2.spdl diff --git a/protocols/misc/trondheim/th-1seq2-rename-ni.spdl b/protocols/misc/compositionality-examples/th-1seq2-rename-ni.spdl similarity index 100% rename from protocols/misc/trondheim/th-1seq2-rename-ni.spdl rename to protocols/misc/compositionality-examples/th-1seq2-rename-ni.spdl diff --git a/protocols/misc/trondheim/th-1seq2-rename-nr.spdl b/protocols/misc/compositionality-examples/th-1seq2-rename-nr.spdl similarity index 100% rename from protocols/misc/trondheim/th-1seq2-rename-nr.spdl rename to protocols/misc/compositionality-examples/th-1seq2-rename-nr.spdl diff --git a/protocols/misc/trondheim/th-1seq2.spdl b/protocols/misc/compositionality-examples/th-1seq2.spdl similarity index 100% rename from protocols/misc/trondheim/th-1seq2.spdl rename to protocols/misc/compositionality-examples/th-1seq2.spdl diff --git a/protocols/misc/trondheim/th-2.spdl b/protocols/misc/compositionality-examples/th-2.spdl similarity index 100% rename from protocols/misc/trondheim/th-2.spdl rename to protocols/misc/compositionality-examples/th-2.spdl diff --git a/protocols/misc/problems-johanselst.spdl b/protocols/misc/problems-johanselst.spdl deleted file mode 100644 index 20e23ac..0000000 --- a/protocols/misc/problems-johanselst.spdl +++ /dev/null @@ -1,83 +0,0 @@ -/* - * Some authentication protocol - * - * Version by Johan Selst. Seems to segfault at a simple -r4 execution - * with the modelchecker. - * - * Reported on 2005-05-11. - */ - -// PKI infrastructure - -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); - -// The protocol description - -protocol as3a(X, I, Y) -{ - role X - { - var nix: Nonce; - - read_1(I, X, nix); - send_2(X, I, {I,nix}sk(X)); - } - - role I - { - const nix, niy: Nonce; - - send_1(I, X, nix); - read_2(X, I, {I,nix}sk(X)); - send_3(I, Y, niy); - read_4(Y, I, {niy,I}sk(Y)); - claim_i1(I, Nisynch); - } - - role Y - { - var niy: Nonce; - - read_3(I, Y, niy); - send_4(Y, I, {niy,I}sk(Y)); - } -} - -// The trusted agents in the system - -const Alice,Bob,Carol: Agent; - -// An untrusted agent, with leaked information - -const Eve: Agent; -untrusted Eve; -compromised sk(Eve); - -// The runs (only needed for the modelchecker algorithm) - -run as3a.X(Agent,Agent,Agent); -run as3a.I(Agent,Agent,Agent); -run as3a.Y(Agent,Agent,Agent); - -run as3a.X(Agent,Agent,Agent); -run as3a.I(Agent,Agent,Agent); -run as3a.Y(Agent,Agent,Agent); - -run as3a.X(Agent,Agent,Agent); -run as3a.I(Agent,Agent,Agent); -run as3a.Y(Agent,Agent,Agent); - -run as3a.X(Agent,Agent,Agent); -run as3a.I(Agent,Agent,Agent); -run as3a.Y(Agent,Agent,Agent); - -run as3a.X(Agent,Agent,Agent); -run as3a.I(Agent,Agent,Agent); -run as3a.Y(Agent,Agent,Agent); - -run as3a.X(Agent,Agent,Agent); -run as3a.I(Agent,Agent,Agent); -run as3a.Y(Agent,Agent,Agent); - diff --git a/protocols/spdl-defaults.inc b/protocols/spdl-defaults.inc deleted file mode 100644 index 9a0b77c..0000000 --- a/protocols/spdl-defaults.inc +++ /dev/null @@ -1,34 +0,0 @@ -/* default includes */ - -/* asymmetric */ - -const pk,hash: Function; -secret sk,unhash: Function; -inversekeys (pk,sk); -inversekeys (hash,unhash); - - -/* symmetric */ - -usertype SessionKey; -secret k: Function; - -/* agents */ - -const a,b,e: Agent; - - -/* untrusted e */ - -untrusted e; -compromised sk(e); -const ne: Nonce; -const kee: SessionKey; - -compromised k(e,e); -compromised k(e,a); -compromised k(e,b); -compromised k(a,e); -compromised k(b,e); - -