From 64f041e176ac752861c47e4274d884d5ebe8dfdc Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 22 Dec 2005 10:38:00 +0000 Subject: [PATCH] - Moved many old protocols to the misc directory. --- spdl/2r890-ex3-a.spdl | 52 -------------- spdl/2r890-ex3-b.spdl | 51 ------------- spdl/{ => misc}/andrew-ban.spdl | 0 spdl/{ => misc}/andrew-lowe-ban.spdl | 0 spdl/{ => misc}/bke-broken.spdl | 0 spdl/{ => misc}/bke-generalized-4.spdl | 0 spdl/{ => misc}/bke-one.spdl | 0 spdl/{ => misc}/bke-variation.spdl | 0 spdl/{ => misc}/bke.spdl | 0 spdl/{ => misc}/bkepk-ce.spdl | 0 spdl/{ => misc}/bkepk-ce2.spdl | 0 spdl/{ => misc}/boyd-nsl-fix.spdl | 0 spdl/{ => misc}/boyd.spdl | 0 spdl/{ => misc}/broken1.spdl | 0 spdl/{ => misc}/bunava-1-3.spdl | 0 spdl/{ => misc}/bunava-1-4.spdl | 0 spdl/{ => misc}/bunava-2-3.spdl | 0 spdl/{ => misc}/bunava-2-4.spdl | 0 spdl/{ => misc}/carkey-broken-limited.spdl | 0 spdl/{ => misc}/carkey-broken.spdl | 0 spdl/{ => misc}/carkey-ni.spdl | 0 spdl/{ => misc}/carkey-ni2.spdl | 0 spdl/{ => misc}/ccitt509-ban.spdl | 0 spdl/{ => misc}/denning-sacco-shared.spdl | 0 spdl/{ => misc}/f4.spdl | 0 spdl/{ => misc}/f5.spdl | 0 spdl/{ => misc}/five-run-bound.spdl | 0 spdl/{ => misc}/gong-nonce-b.spdl | 0 spdl/{ => misc}/gong-nonce.spdl | 0 spdl/{ => misc}/helloworld.spdl | 0 spdl/{ => misc}/isoiec11770-2-13.spdl | 0 spdl/{ => misc}/kaochow-palm.spdl | 0 spdl/{ => misc}/kaochow-v2.spdl | 0 spdl/{ => misc}/kaochow-v3.spdl | 0 spdl/{ => misc}/kaochow.spdl | 0 spdl/{ => misc}/ksl.spdl | 0 spdl/{ => misc}/ns-symmetric-amended.spdl | 0 spdl/{ => misc}/ns-symmetric.spdl | 0 spdl/{ => misc}/ns3-brutus.spdl | 0 spdl/{ => misc}/ns3.spdl | 0 spdl/{ => misc}/nsl-generalized-4.spdl | 0 spdl/{ => misc}/nsl3-nisynch-rep.spdl | 0 spdl/{ => misc}/nsl7.spdl | 0 spdl/{ => misc}/onetrace.spdl | 0 spdl/{ => misc}/otwayrees.spdl | 0 spdl/{ => misc}/samasc-broken.spdl | 0 spdl/{ => misc}/simplest.spdl | 0 spdl/{ => misc}/soph-keyexch.spdl | 0 spdl/{ => misc}/soph.spdl | 0 spdl/{ => misc}/splice-as-hc-cj.spdl | 0 spdl/{ => misc}/splice-as-hc.spdl | 0 spdl/{ => misc}/splice-as.spdl | 0 spdl/{ => misc}/tls-paulson.cpp | 13 ++++ spdl/{ => misc}/tmn-Gijs.spdl | 0 spdl/{ => misc}/tmn.spdl | 0 spdl/{ => misc}/unknown2.spdl | 0 spdl/{ => misc}/wmf-brutus.spdl | 0 spdl/{ => misc}/woolam-ce.spdl | 0 spdl/{ => misc}/woolam-cmv.spdl | 0 spdl/{ => misc}/woolam-pi-f.spdl | 0 spdl/{ => misc}/yahalom-ban.spdl | 0 spdl/{ => misc}/yahalom-lowe.spdl | 0 spdl/{ => misc}/yahalom-paulson.spdl | 0 spdl/{ => misc}/yahalom.spdl | 0 spdl/nsl3.spdl | 6 +- spdl/problems-johanselst.spdl | 83 ---------------------- spdl/speedtest.spdl | 49 ------------- 67 files changed, 16 insertions(+), 238 deletions(-) delete mode 100644 spdl/2r890-ex3-a.spdl delete mode 100644 spdl/2r890-ex3-b.spdl rename spdl/{ => misc}/andrew-ban.spdl (100%) rename spdl/{ => misc}/andrew-lowe-ban.spdl (100%) rename spdl/{ => misc}/bke-broken.spdl (100%) rename spdl/{ => misc}/bke-generalized-4.spdl (100%) rename spdl/{ => misc}/bke-one.spdl (100%) rename spdl/{ => misc}/bke-variation.spdl (100%) rename spdl/{ => misc}/bke.spdl (100%) rename spdl/{ => misc}/bkepk-ce.spdl (100%) rename spdl/{ => misc}/bkepk-ce2.spdl (100%) rename spdl/{ => misc}/boyd-nsl-fix.spdl (100%) rename spdl/{ => misc}/boyd.spdl (100%) rename spdl/{ => misc}/broken1.spdl (100%) rename spdl/{ => misc}/bunava-1-3.spdl (100%) rename spdl/{ => misc}/bunava-1-4.spdl (100%) rename spdl/{ => misc}/bunava-2-3.spdl (100%) rename spdl/{ => misc}/bunava-2-4.spdl (100%) rename spdl/{ => misc}/carkey-broken-limited.spdl (100%) rename spdl/{ => misc}/carkey-broken.spdl (100%) rename spdl/{ => misc}/carkey-ni.spdl (100%) rename spdl/{ => misc}/carkey-ni2.spdl (100%) rename spdl/{ => misc}/ccitt509-ban.spdl (100%) rename spdl/{ => misc}/denning-sacco-shared.spdl (100%) rename spdl/{ => misc}/f4.spdl (100%) rename spdl/{ => misc}/f5.spdl (100%) rename spdl/{ => misc}/five-run-bound.spdl (100%) rename spdl/{ => misc}/gong-nonce-b.spdl (100%) rename spdl/{ => misc}/gong-nonce.spdl (100%) rename spdl/{ => misc}/helloworld.spdl (100%) rename spdl/{ => misc}/isoiec11770-2-13.spdl (100%) rename spdl/{ => misc}/kaochow-palm.spdl (100%) rename spdl/{ => misc}/kaochow-v2.spdl (100%) rename spdl/{ => misc}/kaochow-v3.spdl (100%) rename spdl/{ => misc}/kaochow.spdl (100%) rename spdl/{ => misc}/ksl.spdl (100%) rename spdl/{ => misc}/ns-symmetric-amended.spdl (100%) rename spdl/{ => misc}/ns-symmetric.spdl (100%) rename spdl/{ => misc}/ns3-brutus.spdl (100%) rename spdl/{ => misc}/ns3.spdl (100%) rename spdl/{ => misc}/nsl-generalized-4.spdl (100%) rename spdl/{ => misc}/nsl3-nisynch-rep.spdl (100%) rename spdl/{ => misc}/nsl7.spdl (100%) rename spdl/{ => misc}/onetrace.spdl (100%) rename spdl/{ => misc}/otwayrees.spdl (100%) rename spdl/{ => misc}/samasc-broken.spdl (100%) rename spdl/{ => misc}/simplest.spdl (100%) rename spdl/{ => misc}/soph-keyexch.spdl (100%) rename spdl/{ => misc}/soph.spdl (100%) rename spdl/{ => misc}/splice-as-hc-cj.spdl (100%) rename spdl/{ => misc}/splice-as-hc.spdl (100%) rename spdl/{ => misc}/splice-as.spdl (100%) rename spdl/{ => misc}/tls-paulson.cpp (84%) rename spdl/{ => misc}/tmn-Gijs.spdl (100%) rename spdl/{ => misc}/tmn.spdl (100%) rename spdl/{ => misc}/unknown2.spdl (100%) rename spdl/{ => misc}/wmf-brutus.spdl (100%) rename spdl/{ => misc}/woolam-ce.spdl (100%) rename spdl/{ => misc}/woolam-cmv.spdl (100%) rename spdl/{ => misc}/woolam-pi-f.spdl (100%) rename spdl/{ => misc}/yahalom-ban.spdl (100%) rename spdl/{ => misc}/yahalom-lowe.spdl (100%) rename spdl/{ => misc}/yahalom-paulson.spdl (100%) rename spdl/{ => misc}/yahalom.spdl (100%) delete mode 100644 spdl/problems-johanselst.spdl delete mode 100644 spdl/speedtest.spdl diff --git a/spdl/2r890-ex3-a.spdl b/spdl/2r890-ex3-a.spdl deleted file mode 100644 index bd124d0..0000000 --- a/spdl/2r890-ex3-a.spdl +++ /dev/null @@ -1,52 +0,0 @@ -/* - * Course 2r890 - * - * Assignment 0405-3 - * - * Protocol a - * - * nisynch, niagree - */ -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); - -protocol course2r890year0405ex3(X,Y,I) -{ - role I - { - const nx: Nonce; - const ny: Nonce; - - send_1(I,X, nx ); - read_2(X,I, { I,nx }sk(X) ); - send_3(I,Y, ny ); - read_4(Y,I, { ny,I }sk(Y) ); - - claim_i1(I,Niagree); - claim_i2(I,Nisynch); - } - - role X - { - var nx: Nonce; - - read_1(I,X, nx ); - send_2(X,I, { I,nx }sk(X) ); - } - - role Y - { - var ny: Nonce; - - read_3(I,Y, ny ); - send_4(Y,I, { ny,I }sk(Y) ); - } -} - -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - diff --git a/spdl/2r890-ex3-b.spdl b/spdl/2r890-ex3-b.spdl deleted file mode 100644 index 8620998..0000000 --- a/spdl/2r890-ex3-b.spdl +++ /dev/null @@ -1,51 +0,0 @@ -/* - * Course 2r890 - * - * Assignment 0405-3 - * - * Protocol b - * - * not nisynch, but still niagree - */ -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); - -protocol course2r890year0405ex3(X,Y,I) -{ - role I - { - const ni: Nonce; - - send_1(I,X, ni ); - read_2(X,I, { I,ni }sk(X) ); - send_3(I,Y, ni ); - read_4(Y,I, { ni,I }sk(Y) ); - - claim_i1(I,Niagree); - claim_i2(I,Nisynch); - } - - role X - { - var nx: Nonce; - - read_1(I,X, nx ); - send_2(X,I, { I,nx }sk(X) ); - } - - role Y - { - var ny: Nonce; - - read_3(I,Y, ny ); - send_4(Y,I, { ny,I }sk(Y) ); - } -} - -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - diff --git a/spdl/andrew-ban.spdl b/spdl/misc/andrew-ban.spdl similarity index 100% rename from spdl/andrew-ban.spdl rename to spdl/misc/andrew-ban.spdl diff --git a/spdl/andrew-lowe-ban.spdl b/spdl/misc/andrew-lowe-ban.spdl similarity index 100% rename from spdl/andrew-lowe-ban.spdl rename to spdl/misc/andrew-lowe-ban.spdl diff --git a/spdl/bke-broken.spdl b/spdl/misc/bke-broken.spdl similarity index 100% rename from spdl/bke-broken.spdl rename to spdl/misc/bke-broken.spdl diff --git a/spdl/bke-generalized-4.spdl b/spdl/misc/bke-generalized-4.spdl similarity index 100% rename from spdl/bke-generalized-4.spdl rename to spdl/misc/bke-generalized-4.spdl diff --git a/spdl/bke-one.spdl b/spdl/misc/bke-one.spdl similarity index 100% rename from spdl/bke-one.spdl rename to spdl/misc/bke-one.spdl diff --git a/spdl/bke-variation.spdl b/spdl/misc/bke-variation.spdl similarity index 100% rename from spdl/bke-variation.spdl rename to spdl/misc/bke-variation.spdl diff --git a/spdl/bke.spdl b/spdl/misc/bke.spdl similarity index 100% rename from spdl/bke.spdl rename to spdl/misc/bke.spdl diff --git a/spdl/bkepk-ce.spdl b/spdl/misc/bkepk-ce.spdl similarity index 100% rename from spdl/bkepk-ce.spdl rename to spdl/misc/bkepk-ce.spdl diff --git a/spdl/bkepk-ce2.spdl b/spdl/misc/bkepk-ce2.spdl similarity index 100% rename from spdl/bkepk-ce2.spdl rename to spdl/misc/bkepk-ce2.spdl diff --git a/spdl/boyd-nsl-fix.spdl b/spdl/misc/boyd-nsl-fix.spdl similarity index 100% rename from spdl/boyd-nsl-fix.spdl rename to spdl/misc/boyd-nsl-fix.spdl diff --git a/spdl/boyd.spdl b/spdl/misc/boyd.spdl similarity index 100% rename from spdl/boyd.spdl rename to spdl/misc/boyd.spdl diff --git a/spdl/broken1.spdl b/spdl/misc/broken1.spdl similarity index 100% rename from spdl/broken1.spdl rename to spdl/misc/broken1.spdl diff --git a/spdl/bunava-1-3.spdl b/spdl/misc/bunava-1-3.spdl similarity index 100% rename from spdl/bunava-1-3.spdl rename to spdl/misc/bunava-1-3.spdl diff --git a/spdl/bunava-1-4.spdl b/spdl/misc/bunava-1-4.spdl similarity index 100% rename from spdl/bunava-1-4.spdl rename to spdl/misc/bunava-1-4.spdl diff --git a/spdl/bunava-2-3.spdl b/spdl/misc/bunava-2-3.spdl similarity index 100% rename from spdl/bunava-2-3.spdl rename to spdl/misc/bunava-2-3.spdl diff --git a/spdl/bunava-2-4.spdl b/spdl/misc/bunava-2-4.spdl similarity index 100% rename from spdl/bunava-2-4.spdl rename to spdl/misc/bunava-2-4.spdl diff --git a/spdl/carkey-broken-limited.spdl b/spdl/misc/carkey-broken-limited.spdl similarity index 100% rename from spdl/carkey-broken-limited.spdl rename to spdl/misc/carkey-broken-limited.spdl diff --git a/spdl/carkey-broken.spdl b/spdl/misc/carkey-broken.spdl similarity index 100% rename from spdl/carkey-broken.spdl rename to spdl/misc/carkey-broken.spdl diff --git a/spdl/carkey-ni.spdl b/spdl/misc/carkey-ni.spdl similarity index 100% rename from spdl/carkey-ni.spdl rename to spdl/misc/carkey-ni.spdl diff --git a/spdl/carkey-ni2.spdl b/spdl/misc/carkey-ni2.spdl similarity index 100% rename from spdl/carkey-ni2.spdl rename to spdl/misc/carkey-ni2.spdl diff --git a/spdl/ccitt509-ban.spdl b/spdl/misc/ccitt509-ban.spdl similarity index 100% rename from spdl/ccitt509-ban.spdl rename to spdl/misc/ccitt509-ban.spdl diff --git a/spdl/denning-sacco-shared.spdl b/spdl/misc/denning-sacco-shared.spdl similarity index 100% rename from spdl/denning-sacco-shared.spdl rename to spdl/misc/denning-sacco-shared.spdl diff --git a/spdl/f4.spdl b/spdl/misc/f4.spdl similarity index 100% rename from spdl/f4.spdl rename to spdl/misc/f4.spdl diff --git a/spdl/f5.spdl b/spdl/misc/f5.spdl similarity index 100% rename from spdl/f5.spdl rename to spdl/misc/f5.spdl diff --git a/spdl/five-run-bound.spdl b/spdl/misc/five-run-bound.spdl similarity index 100% rename from spdl/five-run-bound.spdl rename to spdl/misc/five-run-bound.spdl diff --git a/spdl/gong-nonce-b.spdl b/spdl/misc/gong-nonce-b.spdl similarity index 100% rename from spdl/gong-nonce-b.spdl rename to spdl/misc/gong-nonce-b.spdl diff --git a/spdl/gong-nonce.spdl b/spdl/misc/gong-nonce.spdl similarity index 100% rename from spdl/gong-nonce.spdl rename to spdl/misc/gong-nonce.spdl diff --git a/spdl/helloworld.spdl b/spdl/misc/helloworld.spdl similarity index 100% rename from spdl/helloworld.spdl rename to spdl/misc/helloworld.spdl diff --git a/spdl/isoiec11770-2-13.spdl b/spdl/misc/isoiec11770-2-13.spdl similarity index 100% rename from spdl/isoiec11770-2-13.spdl rename to spdl/misc/isoiec11770-2-13.spdl diff --git a/spdl/kaochow-palm.spdl b/spdl/misc/kaochow-palm.spdl similarity index 100% rename from spdl/kaochow-palm.spdl rename to spdl/misc/kaochow-palm.spdl diff --git a/spdl/kaochow-v2.spdl b/spdl/misc/kaochow-v2.spdl similarity index 100% rename from spdl/kaochow-v2.spdl rename to spdl/misc/kaochow-v2.spdl diff --git a/spdl/kaochow-v3.spdl b/spdl/misc/kaochow-v3.spdl similarity index 100% rename from spdl/kaochow-v3.spdl rename to spdl/misc/kaochow-v3.spdl diff --git a/spdl/kaochow.spdl b/spdl/misc/kaochow.spdl similarity index 100% rename from spdl/kaochow.spdl rename to spdl/misc/kaochow.spdl diff --git a/spdl/ksl.spdl b/spdl/misc/ksl.spdl similarity index 100% rename from spdl/ksl.spdl rename to spdl/misc/ksl.spdl diff --git a/spdl/ns-symmetric-amended.spdl b/spdl/misc/ns-symmetric-amended.spdl similarity index 100% rename from spdl/ns-symmetric-amended.spdl rename to spdl/misc/ns-symmetric-amended.spdl diff --git a/spdl/ns-symmetric.spdl b/spdl/misc/ns-symmetric.spdl similarity index 100% rename from spdl/ns-symmetric.spdl rename to spdl/misc/ns-symmetric.spdl diff --git a/spdl/ns3-brutus.spdl b/spdl/misc/ns3-brutus.spdl similarity index 100% rename from spdl/ns3-brutus.spdl rename to spdl/misc/ns3-brutus.spdl diff --git a/spdl/ns3.spdl b/spdl/misc/ns3.spdl similarity index 100% rename from spdl/ns3.spdl rename to spdl/misc/ns3.spdl diff --git a/spdl/nsl-generalized-4.spdl b/spdl/misc/nsl-generalized-4.spdl similarity index 100% rename from spdl/nsl-generalized-4.spdl rename to spdl/misc/nsl-generalized-4.spdl diff --git a/spdl/nsl3-nisynch-rep.spdl b/spdl/misc/nsl3-nisynch-rep.spdl similarity index 100% rename from spdl/nsl3-nisynch-rep.spdl rename to spdl/misc/nsl3-nisynch-rep.spdl diff --git a/spdl/nsl7.spdl b/spdl/misc/nsl7.spdl similarity index 100% rename from spdl/nsl7.spdl rename to spdl/misc/nsl7.spdl diff --git a/spdl/onetrace.spdl b/spdl/misc/onetrace.spdl similarity index 100% rename from spdl/onetrace.spdl rename to spdl/misc/onetrace.spdl diff --git a/spdl/otwayrees.spdl b/spdl/misc/otwayrees.spdl similarity index 100% rename from spdl/otwayrees.spdl rename to spdl/misc/otwayrees.spdl diff --git a/spdl/samasc-broken.spdl b/spdl/misc/samasc-broken.spdl similarity index 100% rename from spdl/samasc-broken.spdl rename to spdl/misc/samasc-broken.spdl diff --git a/spdl/simplest.spdl b/spdl/misc/simplest.spdl similarity index 100% rename from spdl/simplest.spdl rename to spdl/misc/simplest.spdl diff --git a/spdl/soph-keyexch.spdl b/spdl/misc/soph-keyexch.spdl similarity index 100% rename from spdl/soph-keyexch.spdl rename to spdl/misc/soph-keyexch.spdl diff --git a/spdl/soph.spdl b/spdl/misc/soph.spdl similarity index 100% rename from spdl/soph.spdl rename to spdl/misc/soph.spdl diff --git a/spdl/splice-as-hc-cj.spdl b/spdl/misc/splice-as-hc-cj.spdl similarity index 100% rename from spdl/splice-as-hc-cj.spdl rename to spdl/misc/splice-as-hc-cj.spdl diff --git a/spdl/splice-as-hc.spdl b/spdl/misc/splice-as-hc.spdl similarity index 100% rename from spdl/splice-as-hc.spdl rename to spdl/misc/splice-as-hc.spdl diff --git a/spdl/splice-as.spdl b/spdl/misc/splice-as.spdl similarity index 100% rename from spdl/splice-as.spdl rename to spdl/misc/splice-as.spdl diff --git a/spdl/tls-paulson.cpp b/spdl/misc/tls-paulson.cpp similarity index 84% rename from spdl/tls-paulson.cpp rename to spdl/misc/tls-paulson.cpp index 87ffd6a..5d0369e 100644 --- a/spdl/tls-paulson.cpp +++ b/spdl/misc/tls-paulson.cpp @@ -1,3 +1,16 @@ +/* + * This is a model of the TLS version as modeled by Paulson + * + * The .cpp file cannot be fed into scyther directly; rather, one needs + * to type: + * + * cpp tls-paulson.cpp >tls-paulson.spdl + * + * in order to generate a valid spdl file for scyther. + * + * This allows for macro expansion, as seen in the next part. + * + */ #define CERT(a) { a,pk(a) }sk(Terence) #define MSG a,na,sid,pa,pb,nb,sid,pb,CERT(a),CERT(b),{pms}pk(b) #define M hash(pms,na,nb) diff --git a/spdl/tmn-Gijs.spdl b/spdl/misc/tmn-Gijs.spdl similarity index 100% rename from spdl/tmn-Gijs.spdl rename to spdl/misc/tmn-Gijs.spdl diff --git a/spdl/tmn.spdl b/spdl/misc/tmn.spdl similarity index 100% rename from spdl/tmn.spdl rename to spdl/misc/tmn.spdl diff --git a/spdl/unknown2.spdl b/spdl/misc/unknown2.spdl similarity index 100% rename from spdl/unknown2.spdl rename to spdl/misc/unknown2.spdl diff --git a/spdl/wmf-brutus.spdl b/spdl/misc/wmf-brutus.spdl similarity index 100% rename from spdl/wmf-brutus.spdl rename to spdl/misc/wmf-brutus.spdl diff --git a/spdl/woolam-ce.spdl b/spdl/misc/woolam-ce.spdl similarity index 100% rename from spdl/woolam-ce.spdl rename to spdl/misc/woolam-ce.spdl diff --git a/spdl/woolam-cmv.spdl b/spdl/misc/woolam-cmv.spdl similarity index 100% rename from spdl/woolam-cmv.spdl rename to spdl/misc/woolam-cmv.spdl diff --git a/spdl/woolam-pi-f.spdl b/spdl/misc/woolam-pi-f.spdl similarity index 100% rename from spdl/woolam-pi-f.spdl rename to spdl/misc/woolam-pi-f.spdl diff --git a/spdl/yahalom-ban.spdl b/spdl/misc/yahalom-ban.spdl similarity index 100% rename from spdl/yahalom-ban.spdl rename to spdl/misc/yahalom-ban.spdl diff --git a/spdl/yahalom-lowe.spdl b/spdl/misc/yahalom-lowe.spdl similarity index 100% rename from spdl/yahalom-lowe.spdl rename to spdl/misc/yahalom-lowe.spdl diff --git a/spdl/yahalom-paulson.spdl b/spdl/misc/yahalom-paulson.spdl similarity index 100% rename from spdl/yahalom-paulson.spdl rename to spdl/misc/yahalom-paulson.spdl diff --git a/spdl/yahalom.spdl b/spdl/misc/yahalom.spdl similarity index 100% rename from spdl/yahalom.spdl rename to spdl/misc/yahalom.spdl diff --git a/spdl/nsl3.spdl b/spdl/nsl3.spdl index 8ccecde..874a439 100644 --- a/spdl/nsl3.spdl +++ b/spdl/nsl3.spdl @@ -12,6 +12,7 @@ protocol nsl3(I,R) send_1(I,R, {I,ni}pk(R) ); read_2(R,I, {ni,nr,R}pk(I) ); send_3(I,R, {nr}pk(R) ); + claim_i1(I,Secret,ni); claim_i2(I,Secret,nr); claim_i3(I,Niagree); @@ -26,6 +27,7 @@ protocol nsl3(I,R) read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); read_3(I,R, {nr}pk(R) ); + claim_r1(R,Secret,ni); claim_r2(R,Secret,nr); claim_r3(R,Niagree); @@ -33,11 +35,9 @@ protocol nsl3(I,R) } } -const Alice,Bob,Eve: Agent; +const Eve: Agent; untrusted Eve; const ne: Nonce; compromised sk(Eve); -run nsl3.I(Agent,Agent); -run nsl3.R(Agent,Agent); diff --git a/spdl/problems-johanselst.spdl b/spdl/problems-johanselst.spdl deleted file mode 100644 index 20e23ac..0000000 --- a/spdl/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/spdl/speedtest.spdl b/spdl/speedtest.spdl deleted file mode 100644 index 3b9b72e..0000000 --- a/spdl/speedtest.spdl +++ /dev/null @@ -1,49 +0,0 @@ -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); - -protocol ns3speedtest(I,R) -{ - role I - { - const ni: Nonce; - var nr: Nonce; - - send_1(I,R, {I,ni}pk(R) ); - read_2(R,I, {ni,nr}pk(I) ); - send_3(I,R, {nr}pk(R) ); - claim_4(I,Secret,nr); - } - - role R - { - var ni: Nonce; - const nr: Nonce; - - read_1(I,R, {I,ni}pk(R) ); - send_2(R,I, {ni,nr}pk(I) ); - read_3(I,R, {nr}pk(R) ); - claim_5(R,Secret,ni); - } -} - -const Alice,Bob,Eve : Agent; - -/* something like this will later on all be implied by 'untrusted Eve' */ - -untrusted Eve; -const nc: Nonce; -compromised sk(Eve); - -/* pre-defined 10 runs, limit using --max-runs parameters */ - -run ns3speedtest.I(Alice,Bob); - run ns3speedtest.R(Alice,Bob); -run ns3speedtest.I(Alice,Eve); - run ns3speedtest.R(Eve,Bob); -run ns3speedtest.I(Bob,Alice); - run ns3speedtest.R(Bob,Alice); -run ns3speedtest.I(Bob,Eve); - run ns3speedtest.R(Eve,Alice); -run ns3speedtest.I(Alice,Alice); - run ns3speedtest.R(Bob,Bob);