From 727e813c7791919ebf9d4769e6a5e61b441dd28c Mon Sep 17 00:00:00 2001 From: Cas Cremers Date: Wed, 2 May 2012 23:01:08 +0200 Subject: [PATCH] Fixed obsolete notation in protocol specification files. Not everything is fixed yet. However, we fixed: - 'const' -> 'fresh' - Removed lines specifying 'runs' - Removed some specifications of compromised Eve and its long-term keys being compromised. --- gui/Protocols/ccitt509-1c.spdl | 4 +-- gui/Protocols/ccitt509-ban3.spdl | 4 +-- protocols/Demo/ns3.spdl | 4 +-- protocols/Demo/nsl3-broken.spdl | 4 +-- protocols/Demo/nsl3-updated-both.spdl | 8 +++--- protocols/Demo/nsl3.spdl | 4 +-- protocols/misc/2r890-ex3-a.spdl | 8 ++---- protocols/misc/2r890-ex3-b.spdl | 6 +---- protocols/misc/andrew-ban.spdl | 18 +++---------- protocols/misc/andrew-lowe-ban.spdl | 18 +++---------- protocols/misc/athena-breaker.spdl | 7 +----- protocols/misc/bke-broken.spdl | 10 +++----- protocols/misc/bke-one.spdl | 18 +++---------- protocols/misc/bke-variation.spdl | 12 +++------ protocols/misc/bke.spdl | 24 +++--------------- protocols/misc/bkepk-ce.spdl | 8 +++--- protocols/misc/bkepk-ce2.spdl | 17 +++---------- protocols/misc/boyd-nsl-fix.spdl | 10 ++------ protocols/misc/boyd.spdl | 6 ++--- protocols/misc/bunava-1-3.spdl | 21 +++------------- protocols/misc/bunava-1-4.spdl | 25 +++---------------- protocols/misc/bunava-2-3.spdl | 21 +++------------- protocols/misc/bunava-2-4.spdl | 25 +++---------------- protocols/misc/carkey-broken-limited.spdl | 10 +------- protocols/misc/carkey-broken.spdl | 10 +------- protocols/misc/carkey-ni.spdl | 10 +------- protocols/misc/carkey-ni2.spdl | 10 +------- protocols/misc/ccitt509-ban.spdl | 16 +++--------- .../misc/compositionality-examples/th-1.spdl | 8 ++---- .../compositionality-examples/th-1par2.spdl | 16 +++--------- .../th-1seq2-rename-ni.spdl | 8 ++---- .../th-1seq2-rename-nr.spdl | 8 ++---- .../compositionality-examples/th-1seq2.spdl | 8 ++---- .../misc/compositionality-examples/th-2.spdl | 8 ++---- protocols/misc/denning-sacco-shared.spdl | 6 ++--- protocols/misc/f4.spdl | 6 +---- protocols/misc/f5.spdl | 6 +---- protocols/misc/five-run-bound.spdl | 4 +-- protocols/misc/fourway-HSDDM05.cpp | 9 ++----- protocols/misc/fourway-HSDDM05.spdl | 9 ++----- protocols/misc/gong-nonce-b.spdl | 24 +++--------------- protocols/misc/gong-nonce.spdl | 24 +++--------------- protocols/misc/ibe-ns.spdl | 12 ++------- protocols/misc/ibe.spdl | 6 +---- protocols/misc/isoiec11770-2-13.spdl | 22 +++------------- protocols/misc/kaochow-palm.spdl | 22 +++------------- protocols/misc/kaochow-v2.spdl | 22 +++------------- protocols/misc/kaochow-v3.spdl | 24 +++--------------- protocols/misc/kaochow.spdl | 22 +++------------- protocols/misc/kerberos-rddm.spdl | 23 ++++------------- protocols/misc/ksl.spdl | 15 ++++------- protocols/misc/localclaims-breaker.spdl | 10 +++----- protocols/misc/localclaims-seq1.spdl | 12 +++------ protocols/misc/localclaims.spdl | 7 +----- protocols/misc/ns-symmetric-amended.spdl | 8 +++--- protocols/misc/ns-symmetric.spdl | 8 +++--- protocols/misc/ns3-brutus.spdl | 13 +++------- protocols/misc/ns3.spdl | 19 ++------------ protocols/misc/nsl3-nisynch-rep.spdl | 12 ++------- protocols/misc/nsl3.spdl | 8 ++---- protocols/misc/nst1.spdl | 14 ++++------- protocols/misc/nst2.spdl | 14 ++++------- protocols/misc/otwayrees.spdl | 18 ++++--------- protocols/misc/samasc-broken.spdl | 4 +-- protocols/misc/simplest.spdl | 4 +-- protocols/misc/soph-keyexch.spdl | 13 +++------- protocols/misc/soph.spdl | 10 +------- protocols/misc/speedtest.spdl | 13 ++-------- protocols/misc/splice-as-hc-cj.spdl | 21 ++++++---------- protocols/misc/splice-as-hc.spdl | 21 ++++++---------- protocols/misc/splice-as.spdl | 21 ++++++---------- protocols/misc/tls/tls-BM-1.m4 | 8 +++--- protocols/misc/tls/tls-BM-1.spdl | 8 +++--- protocols/misc/tls/tls-HSDDM05-2.cpp | 12 ++++----- protocols/misc/tls/tls-HSDDM05-2.spdl | 12 ++++----- protocols/misc/tls/tls-HSDDM05-fix.cpp | 12 ++++----- protocols/misc/tls/tls-HSDDM05-fix.m4 | 12 ++++----- protocols/misc/tls/tls-HSDDM05-fix.spdl | 12 ++++----- protocols/misc/tls/tls-HSDDM05.cpp | 12 ++++----- protocols/misc/tls/tls-HSDDM05.spdl | 12 ++++----- protocols/misc/tls/tls-paulson-avispa.cpp | 15 ++++------- protocols/misc/tls/tls-paulson-avispa.spdl | 17 ++++--------- protocols/misc/tls/tls-paulson.cpp | 23 ++++------------- protocols/misc/tls/tls-paulson.spdl | 23 ++++------------- protocols/misc/tmn-Gijs.spdl | 8 ++---- protocols/misc/tmn.spdl | 14 +++-------- protocols/misc/unknown2.spdl | 20 +++------------ protocols/misc/wmf-brutus.spdl | 13 ++-------- protocols/misc/woolam-cmv.spdl | 12 +++------ protocols/misc/woolam-pi-f.spdl | 8 +----- protocols/misc/yahalom-ban.spdl | 6 ++--- protocols/misc/yahalom-lowe.spdl | 15 +++-------- protocols/misc/yahalom-paulson.spdl | 15 +++-------- 93 files changed, 281 insertions(+), 908 deletions(-) diff --git a/gui/Protocols/ccitt509-1c.spdl b/gui/Protocols/ccitt509-1c.spdl index 6ae4088..b75e069 100644 --- a/gui/Protocols/ccitt509-1c.spdl +++ b/gui/Protocols/ccitt509-1c.spdl @@ -14,8 +14,8 @@ protocol ccitt509-1c(I,R) { role I { - const Ta: Timestamp; - const Na,Xa,Ya: Nonce; + fresh Ta: Timestamp; + fresh Na,Xa,Ya: Nonce; send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); # claim_2(I,Nisynch); # This claim is useless as there are no preceding receive events diff --git a/gui/Protocols/ccitt509-ban3.spdl b/gui/Protocols/ccitt509-ban3.spdl index 0cbc198..bdf146d 100644 --- a/gui/Protocols/ccitt509-ban3.spdl +++ b/gui/Protocols/ccitt509-ban3.spdl @@ -15,7 +15,7 @@ protocol ccitt509-ban3(I,R) { role I { - const Na,Xa,Ya: Nonce; + fresh Na,Xa,Ya: Nonce; var Xb,Nb,Yb: Nonce; send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); @@ -27,7 +27,7 @@ protocol ccitt509-ban3(I,R) role R { var Na,Xa,Ya: Nonce; - const Xb,Yb,Nb: Nonce; + fresh Xb,Yb,Nb: Nonce; recv_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); send_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); diff --git a/protocols/Demo/ns3.spdl b/protocols/Demo/ns3.spdl index 7b3e6ba..7954e31 100644 --- a/protocols/Demo/ns3.spdl +++ b/protocols/Demo/ns3.spdl @@ -8,7 +8,7 @@ protocol ns3(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {I,ni}pk(R) ); @@ -24,7 +24,7 @@ protocol ns3(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr}pk(I) ); diff --git a/protocols/Demo/nsl3-broken.spdl b/protocols/Demo/nsl3-broken.spdl index 458e306..b06cb69 100644 --- a/protocols/Demo/nsl3-broken.spdl +++ b/protocols/Demo/nsl3-broken.spdl @@ -9,7 +9,7 @@ protocol nsl3-broken(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {R,ni}pk(R) ); @@ -25,7 +25,7 @@ protocol nsl3-broken(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {R,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); diff --git a/protocols/Demo/nsl3-updated-both.spdl b/protocols/Demo/nsl3-updated-both.spdl index e8c6bf0..4e706c2 100644 --- a/protocols/Demo/nsl3-updated-both.spdl +++ b/protocols/Demo/nsl3-updated-both.spdl @@ -9,7 +9,7 @@ protocol nsl3-broken(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {R,ni}pk(R) ); @@ -25,7 +25,7 @@ protocol nsl3-broken(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {R,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); @@ -48,7 +48,7 @@ protocol nsl3(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {I,ni}pk(R) ); @@ -64,7 +64,7 @@ protocol nsl3(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); diff --git a/protocols/Demo/nsl3.spdl b/protocols/Demo/nsl3.spdl index e448499..6d367cb 100644 --- a/protocols/Demo/nsl3.spdl +++ b/protocols/Demo/nsl3.spdl @@ -8,7 +8,7 @@ protocol nsl3(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {I,ni}pk(R) ); @@ -24,7 +24,7 @@ protocol nsl3(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); diff --git a/protocols/misc/2r890-ex3-a.spdl b/protocols/misc/2r890-ex3-a.spdl index bd124d0..32c55ab 100644 --- a/protocols/misc/2r890-ex3-a.spdl +++ b/protocols/misc/2r890-ex3-a.spdl @@ -15,8 +15,8 @@ protocol course2r890year0405ex3(X,Y,I) { role I { - const nx: Nonce; - const ny: Nonce; + fresh nx: Nonce; + fresh ny: Nonce; send_1(I,X, nx ); read_2(X,I, { I,nx }sk(X) ); @@ -44,9 +44,5 @@ protocol course2r890year0405ex3(X,Y,I) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/2r890-ex3-b.spdl b/protocols/misc/2r890-ex3-b.spdl index 8620998..4b9c8cd 100644 --- a/protocols/misc/2r890-ex3-b.spdl +++ b/protocols/misc/2r890-ex3-b.spdl @@ -15,7 +15,7 @@ protocol course2r890year0405ex3(X,Y,I) { role I { - const ni: Nonce; + fresh ni: Nonce; send_1(I,X, ni ); read_2(X,I, { I,ni }sk(X) ); @@ -43,9 +43,5 @@ protocol course2r890year0405ex3(X,Y,I) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/andrew-ban.spdl b/protocols/misc/andrew-ban.spdl index 3524f75..580e108 100644 --- a/protocols/misc/andrew-ban.spdl +++ b/protocols/misc/andrew-ban.spdl @@ -5,7 +5,7 @@ protocol andrewBan(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr,nr2: Nonce; var kir: SessionKey; @@ -22,8 +22,8 @@ protocol andrewBan(I,R) role R { var ni: Nonce; - const nr,nr2: Nonce; - const kir: SessionKey; + fresh nr,nr2: Nonce; + fresh kir: SessionKey; read_1(I,R, I,{ni}k(I,R) ); send_2(R,I, {ni,nr}k(I,R) ); @@ -36,18 +36,6 @@ protocol andrewBan(I,R) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const ne: Nonce; const kee: SessionKey; -compromised k(Eve,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Alice,Eve); -compromised k(Bob,Eve); -run andrewBan.I(Agent,Agent); -run andrewBan.R(Agent,Agent); -run andrewBan.I(Agent,Agent); -run andrewBan.R(Agent,Agent); diff --git a/protocols/misc/andrew-lowe-ban.spdl b/protocols/misc/andrew-lowe-ban.spdl index 8c292bd..778fac1 100644 --- a/protocols/misc/andrew-lowe-ban.spdl +++ b/protocols/misc/andrew-lowe-ban.spdl @@ -5,7 +5,7 @@ protocol andrewLoweBan(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: SessionKey; @@ -22,8 +22,8 @@ protocol andrewLoweBan(I,R) role R { var ni: Nonce; - const nr: Nonce; - const kir: SessionKey; + fresh nr: Nonce; + fresh kir: SessionKey; read_1(I,R, I,ni ); send_2(R,I, {ni,kir,I}k(I,R) ); @@ -36,18 +36,6 @@ protocol andrewLoweBan(I,R) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const ne: Nonce; const kee: SessionKey; -compromised k(Eve,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Alice,Eve); -compromised k(Bob,Eve); -run andrewLoweBan.I(Agent,Agent); -run andrewLoweBan.R(Agent,Agent); -run andrewLoweBan.I(Agent,Agent); -run andrewLoweBan.R(Agent,Agent); diff --git a/protocols/misc/athena-breaker.spdl b/protocols/misc/athena-breaker.spdl index 7d31f73..75d15a0 100644 --- a/protocols/misc/athena-breaker.spdl +++ b/protocols/misc/athena-breaker.spdl @@ -14,7 +14,7 @@ protocol abreaker(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; send_!1(I,R, {{I,ni}pk(R)}pk(R) ); @@ -33,12 +33,7 @@ protocol abreaker(I,R) // The agents in the system -const Alice,Bob: Agent; // An untrusted agent, with leaked information -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/bke-broken.spdl b/protocols/misc/bke-broken.spdl index 4d2321e..e05e1bd 100644 --- a/protocols/misc/bke-broken.spdl +++ b/protocols/misc/bke-broken.spdl @@ -15,7 +15,7 @@ protocol bkebroken(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: Key; @@ -28,8 +28,8 @@ protocol bkebroken(I,R) role R { var ni: Nonce; - const nr: Nonce; - const kir: Key; + fresh nr: Nonce; + fresh kir: Key; read_1 (I,R, { ni,I }pk(R) ); send_2 (R,I, { h(ni),nr,kir }pk(I) ); @@ -38,11 +38,7 @@ protocol bkebroken(I,R) } } -const a,b,e: Agent; untrusted e; compromised sk(e); -const ne: Nonce; -run bkebroken.I(a,Agent); -run bkebroken.R(Agent,b); diff --git a/protocols/misc/bke-one.spdl b/protocols/misc/bke-one.spdl index a5e8325..f21b775 100644 --- a/protocols/misc/bke-one.spdl +++ b/protocols/misc/bke-one.spdl @@ -14,7 +14,7 @@ protocol bkeONE(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: Key; @@ -27,8 +27,8 @@ protocol bkeONE(I,R) role R { var ni: Nonce; - const nr: Nonce; - const kir: Key; + fresh nr: Nonce; + fresh kir: Key; read_1 (I,R, { ni,I }pk(R) ); send_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); @@ -37,22 +37,10 @@ protocol bkeONE(I,R) } } -const a,e: Agent; untrusted e; compromised sk(e); -const ne: Nonce; -run bkeONE.I(a,Agent); -run bkeONE.R(Agent,a); -run bkeONE.I(a,Agent); -run bkeONE.R(Agent,a); -run bkeONE.I(a,Agent); -run bkeONE.R(Agent,a); -run bkeONE.I(a,Agent); -run bkeONE.R(Agent,a); -run bkeONE.I(a,Agent); -run bkeONE.R(Agent,a); diff --git a/protocols/misc/bke-variation.spdl b/protocols/misc/bke-variation.spdl index 6f7e91f..f7e8b30 100644 --- a/protocols/misc/bke-variation.spdl +++ b/protocols/misc/bke-variation.spdl @@ -15,7 +15,7 @@ protocol bkevariation(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: Key; @@ -30,8 +30,8 @@ protocol bkevariation(I,R) role R { var ni: Nonce; - const nr: Nonce; - const kir: Key; + fresh nr: Nonce; + fresh kir: Key; read_1 (I,R, { ni,I }pk(R) ); send_2 (R,I, { hash(ni),nr,kir }pk(I) ); @@ -42,14 +42,8 @@ protocol bkevariation(I,R) } } -const a,b,e: Agent; untrusted e; compromised sk(e); -const ne: Nonce; -run bkevariation.I(a,Agent); -run bkevariation.R(Agent,b); -run bkevariation.I(a,Agent); -run bkevariation.R(Agent,b); diff --git a/protocols/misc/bke.spdl b/protocols/misc/bke.spdl index 73d9ac5..3962db2 100644 --- a/protocols/misc/bke.spdl +++ b/protocols/misc/bke.spdl @@ -4,17 +4,13 @@ usertype Key; -const pk,hash: Function; -secret sk,unhash: Function; - -inversekeys (pk,sk); -inversekeys (hash,unhash); +hashfunction hash; protocol bke(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: Key; @@ -29,8 +25,8 @@ protocol bke(I,R) role R { var ni: Nonce; - const nr: Nonce; - const kir: Key; + fresh nr: Nonce; + fresh kir: Key; read_1 (I,R, { ni,I }pk(R) ); send_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); @@ -41,22 +37,10 @@ protocol bke(I,R) } } -const a,b,e: Agent; untrusted e; compromised sk(e); -const ne: Nonce; -run bke.I(a,Agent); -run bke.R(Agent,b); -run bke.I(a,Agent); -run bke.R(Agent,b); -run bke.I(a,Agent); -run bke.R(Agent,b); -run bke.I(a,Agent); -run bke.R(Agent,b); -run bke.I(a,Agent); -run bke.R(Agent,b); diff --git a/protocols/misc/bkepk-ce.spdl b/protocols/misc/bkepk-ce.spdl index cb5cedb..91bb7f9 100644 --- a/protocols/misc/bkepk-ce.spdl +++ b/protocols/misc/bkepk-ce.spdl @@ -18,8 +18,8 @@ protocol bkeCE(A,B) role A { var nb: Nonce; - const na: Nonce; - const kab: Key; + fresh na: Nonce; + fresh kab: Key; read_1 (B,A, B,{ nb,B }pk(A) ); send_2 (A,B, { hash(nb),na,A,kab }pk(B) ); @@ -31,7 +31,7 @@ protocol bkeCE(A,B) role B { - const nb: Nonce; + fresh nb: Nonce; var na: Nonce; var kab: Key; @@ -47,7 +47,5 @@ protocol bkeCE(A,B) const Alice,Bob,Eve; -compromised sk(Eve); -untrusted Eve; diff --git a/protocols/misc/bkepk-ce2.spdl b/protocols/misc/bkepk-ce2.spdl index 09879bf..f596453 100644 --- a/protocols/misc/bkepk-ce2.spdl +++ b/protocols/misc/bkepk-ce2.spdl @@ -16,7 +16,7 @@ protocol bkepkCE2(A,B,testnonce) { role B { - const nb: Nonce; + fresh nb: Nonce; var na: Nonce; var kab: Key; @@ -28,8 +28,8 @@ protocol bkepkCE2(A,B,testnonce) role A { var nb: Nonce; - const na: Nonce; - const kab: Key; + fresh na: Nonce; + fresh kab: Key; read_1 (B,A, B,{ nb,B }pk(A) ); send_2 (A,B, { hash(nb),na,A,kab }pk(B) ); @@ -46,17 +46,6 @@ protocol bkepkCE2(A,B,testnonce) const Alice,Bob,Eve; -compromised sk(Eve); -untrusted Eve; -run bkepkCE2.A(Alice,Bob,Alice); -run bkepkCE2.A(Alice,Bob,Alice); -run bkepkCE2.A(Alice,Bob,Alice); -run bkepkCE2.B(Alice,Bob,Alice); -run bkepkCE2.B(Alice,Bob,Alice); -run bkepkCE2.B(Alice,Bob,Alice); -run bkepkCE2.testnonce(Alice,Bob,Alice); -run bkepkCE2.testnonce(Alice,Bob,Alice); -run bkepkCE2.testnonce(Alice,Bob,Alice); diff --git a/protocols/misc/boyd-nsl-fix.spdl b/protocols/misc/boyd-nsl-fix.spdl index 3413026..02adf67 100644 --- a/protocols/misc/boyd-nsl-fix.spdl +++ b/protocols/misc/boyd-nsl-fix.spdl @@ -18,7 +18,7 @@ protocol boydNS(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {ni}pk(R),I ); @@ -33,7 +33,7 @@ protocol boydNS(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {ni}pk(R),I ); send_2(R,I, {nr}pk(I),hash(ni,R) ); @@ -45,11 +45,5 @@ protocol boydNS(I,R) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); -run boydNS.I(Agent,Agent); -run boydNS.R(Agent,Agent); diff --git a/protocols/misc/boyd.spdl b/protocols/misc/boyd.spdl index ace3bd7..1ce9516 100644 --- a/protocols/misc/boyd.spdl +++ b/protocols/misc/boyd.spdl @@ -20,7 +20,7 @@ protocol boyd(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var ks: Macseed; @@ -36,7 +36,7 @@ protocol boyd(I,R,S) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; var ks: Macseed; read_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni ); @@ -51,7 +51,7 @@ protocol boyd(I,R,S) role S { var ni,nr: Nonce; - const ks: Macseed; + fresh ks: Macseed; read_1 (I,S, I,R, ni ); send_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni ); diff --git a/protocols/misc/bunava-1-3.spdl b/protocols/misc/bunava-1-3.spdl index 17858d1..5b5803a 100644 --- a/protocols/misc/bunava-1-3.spdl +++ b/protocols/misc/bunava-1-3.spdl @@ -29,7 +29,7 @@ protocol bunava13(R0,R1,R2) { role R0 { - const n0: Nonce; + fresh n0: Nonce; var n1,n2: Nonce; send_1(R0,R1, n0); @@ -42,7 +42,7 @@ protocol bunava13(R0,R1,R2) role R1 { - const n1: Nonce; + fresh n1: Nonce; var n0,n2: Nonce; read_1(R0,R1, n0); @@ -56,7 +56,7 @@ protocol bunava13(R0,R1,R2) role R2 { - const n2: Nonce; + fresh n2: Nonce; var n0,n1: Nonce; read_2(R1,R2, n1,{R1,n0}k(R1,R2) ); @@ -68,22 +68,7 @@ protocol bunava13(R0,R1,R2) } } -const Alice,Bob,Charlie,David,Frodo,Gerard,Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Charlie,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Charlie); # General scenario, 2 parallel runs of the protocol -run bunava13.R0(Agent,Agent,Agent); -run bunava13.R1(Agent,Agent,Agent); -run bunava13.R2(Agent,Agent,Agent); -run bunava13.R0(Agent,Agent,Agent); -run bunava13.R1(Agent,Agent,Agent); -run bunava13.R2(Agent,Agent,Agent); diff --git a/protocols/misc/bunava-1-4.spdl b/protocols/misc/bunava-1-4.spdl index b858e5a..a5be500 100644 --- a/protocols/misc/bunava-1-4.spdl +++ b/protocols/misc/bunava-1-4.spdl @@ -30,7 +30,7 @@ protocol bunava14(A,B,C,D) { role A { - const ra: Nonce; + fresh ra: Nonce; var rb,rc,rd: Nonce; send_1(A,B, ra); @@ -43,7 +43,7 @@ protocol bunava14(A,B,C,D) role B { - const rb: Nonce; + fresh rb: Nonce; var ra,rc,rd: Nonce; read_1(A,B, ra); @@ -57,7 +57,7 @@ protocol bunava14(A,B,C,D) role C { - const rc: Nonce; + fresh rc: Nonce; var ra,rb,rd: Nonce; read_2(B,C, rb,{B,ra}k(B,C) ); @@ -71,7 +71,7 @@ protocol bunava14(A,B,C,D) role D { - const rd: Nonce; + fresh rd: Nonce; var ra,rb,rc: Nonce; read_3(C,D, rc,{C,rb,B,ra}k(C,D) ); @@ -83,24 +83,7 @@ protocol bunava14(A,B,C,D) } } -const Alice,Bob,Charlie,Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Charlie,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Charlie); # General scenario, 2 parallel runs of the protocol -run bunava14.A(Agent,Agent,Agent,Agent); -run bunava14.B(Agent,Agent,Agent,Agent); -run bunava14.C(Agent,Agent,Agent,Agent); -run bunava14.D(Agent,Agent,Agent,Agent); -run bunava14.A(Agent,Agent,Agent,Agent); -run bunava14.B(Agent,Agent,Agent,Agent); -run bunava14.C(Agent,Agent,Agent,Agent); -run bunava14.D(Agent,Agent,Agent,Agent); diff --git a/protocols/misc/bunava-2-3.spdl b/protocols/misc/bunava-2-3.spdl index 2ecf955..af100ae 100644 --- a/protocols/misc/bunava-2-3.spdl +++ b/protocols/misc/bunava-2-3.spdl @@ -25,7 +25,7 @@ protocol bunava23(R0,R1,R2) { role R0 { - const n0: Nonce; + fresh n0: Nonce; var n1,n2: Nonce; var T0: Ticket; @@ -39,7 +39,7 @@ protocol bunava23(R0,R1,R2) role R1 { - const n1: Nonce; + fresh n1: Nonce; var n0,n2: Nonce; var T1: Ticket; @@ -54,7 +54,7 @@ protocol bunava23(R0,R1,R2) role R2 { - const n2: Nonce; + fresh n2: Nonce; var n0,n1: Nonce; var T2: Ticket; @@ -67,22 +67,7 @@ protocol bunava23(R0,R1,R2) } } -const Alice,Bob,Charlie,David,Frodo,Gerard,Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Charlie,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Charlie); # General scenario -run bunava23.R0(Agent,Agent,Agent); -run bunava23.R1(Agent,Agent,Agent); -run bunava23.R2(Agent,Agent,Agent); -run bunava23.R0(Agent,Agent,Agent); -run bunava23.R1(Agent,Agent,Agent); -run bunava23.R2(Agent,Agent,Agent); diff --git a/protocols/misc/bunava-2-4.spdl b/protocols/misc/bunava-2-4.spdl index 68e5fe4..3311d62 100644 --- a/protocols/misc/bunava-2-4.spdl +++ b/protocols/misc/bunava-2-4.spdl @@ -27,7 +27,7 @@ protocol bunava24(A,B,C,D) { role A { - const ra: Nonce; + fresh ra: Nonce; var rb,rc,rd: Nonce; var Tacd, Tabd: Ticket; @@ -49,7 +49,7 @@ protocol bunava24(A,B,C,D) role B { - const rb: Nonce; + fresh rb: Nonce; var ra,rc,rd: Nonce; var Tbad, Tbac: Ticket; @@ -73,7 +73,7 @@ protocol bunava24(A,B,C,D) role C { - const rc: Nonce; + fresh rc: Nonce; var ra,rb,rd: Nonce; var Tcab,Tcbd: Ticket; @@ -96,7 +96,7 @@ protocol bunava24(A,B,C,D) role D { - const rd: Nonce; + fresh rd: Nonce; var ra,rb,rc: Nonce; var Tdbc,Tdac: Ticket; @@ -115,24 +115,7 @@ protocol bunava24(A,B,C,D) } } -const Alice,Bob,Charlie,Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Charlie,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Charlie); # General scenario -run bunava24.A(Agent,Agent,Agent,Agent); -run bunava24.B(Agent,Agent,Agent,Agent); -run bunava24.C(Agent,Agent,Agent,Agent); -run bunava24.D(Agent,Agent,Agent,Agent); -run bunava24.A(Agent,Agent,Agent,Agent); -run bunava24.B(Agent,Agent,Agent,Agent); -run bunava24.C(Agent,Agent,Agent,Agent); -run bunava24.D(Agent,Agent,Agent,Agent); diff --git a/protocols/misc/carkey-broken-limited.spdl b/protocols/misc/carkey-broken-limited.spdl index 346beaa..91a75a4 100644 --- a/protocols/misc/carkey-broken-limited.spdl +++ b/protocols/misc/carkey-broken-limited.spdl @@ -6,7 +6,7 @@ protocol carkeybrokenlim(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; send_1(I,R, I,R ); } @@ -20,13 +20,5 @@ protocol carkeybrokenlim(I,R) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const nc: Nonce; -compromised sk(Eve); -run carkeybrokenlim.I(Alice,Bob); -run carkeybrokenlim.R(Alice,Bob); -run carkeybrokenlim.I(Alice,Bob); -run carkeybrokenlim.R(Alice,Bob); diff --git a/protocols/misc/carkey-broken.spdl b/protocols/misc/carkey-broken.spdl index a0e0ba5..8ad0198 100644 --- a/protocols/misc/carkey-broken.spdl +++ b/protocols/misc/carkey-broken.spdl @@ -6,7 +6,7 @@ protocol carkeybroken(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; send_1(I,R, {ni}sk(I) ); } @@ -20,13 +20,5 @@ protocol carkeybroken(I,R) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const nc: Nonce; -compromised sk(Eve); -run carkeybroken.I(Agent,Agent); -run carkeybroken.R(Agent,Agent); -run carkeybroken.I(Agent,Agent); -run carkeybroken.R(Agent,Agent); diff --git a/protocols/misc/carkey-ni.spdl b/protocols/misc/carkey-ni.spdl index ed189b4..ec809fc 100644 --- a/protocols/misc/carkey-ni.spdl +++ b/protocols/misc/carkey-ni.spdl @@ -6,7 +6,7 @@ protocol carkeyni(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; send_1(I,R, {R,ni}sk(I) ); } @@ -20,13 +20,5 @@ protocol carkeyni(I,R) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const nc: Nonce; -compromised sk(Eve); -run carkeyni.I(Agent,Agent); -run carkeyni.R(Agent,Agent); -run carkeyni.I(Agent,Agent); -run carkeyni.R(Agent,Agent); diff --git a/protocols/misc/carkey-ni2.spdl b/protocols/misc/carkey-ni2.spdl index 49bbe95..e6e5551 100644 --- a/protocols/misc/carkey-ni2.spdl +++ b/protocols/misc/carkey-ni2.spdl @@ -6,7 +6,7 @@ protocol carkeyni2(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; send_1(I,R, {R,ni}sk(I) ); send_2(I,R, {R,ni}sk(I) ); @@ -22,13 +22,5 @@ protocol carkeyni2(I,R) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const nc: Nonce; -compromised sk(Eve); -run carkeyni2.I(Agent,Agent); -run carkeyni2.R(Agent,Agent); -run carkeyni2.I(Agent,Agent); -run carkeyni2.R(Agent,Agent); diff --git a/protocols/misc/ccitt509-ban.spdl b/protocols/misc/ccitt509-ban.spdl index c4c15d5..23e26b6 100644 --- a/protocols/misc/ccitt509-ban.spdl +++ b/protocols/misc/ccitt509-ban.spdl @@ -7,8 +7,8 @@ protocol ccitt509(I,R) { role I { - const xi,yi: Data; - const ni: Nonce; + fresh xi,yi: Data; + fresh ni: Nonce; var nr: Nonce; var yr,xr: Data; @@ -26,8 +26,8 @@ protocol ccitt509(I,R) { var xi,yi: Data; var ni: Nonce; - const nr: Nonce; - const yr,xr: Data; + fresh nr: Nonce; + fresh yr,xr: Data; read_1(I,R, I,{ni, R, xi, {yi}pk(R) }sk(I) ); send_2(R,I, R,{nr, I, ni, xr, {yr}pk(I) }sk(R) ); @@ -40,14 +40,6 @@ protocol ccitt509(I,R) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const ne: Nonce; const de: Data; -compromised sk(Eve); -run ccitt509.I(Agent,Agent); -run ccitt509.R(Agent,Agent); -run ccitt509.I(Agent,Agent); -run ccitt509.R(Agent,Agent); diff --git a/protocols/misc/compositionality-examples/th-1.spdl b/protocols/misc/compositionality-examples/th-1.spdl index f1dd1d5..a69cf2d 100644 --- a/protocols/misc/compositionality-examples/th-1.spdl +++ b/protocols/misc/compositionality-examples/th-1.spdl @@ -7,7 +7,7 @@ protocol nsl3th1(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {P1,I,ni}pk(R) ); @@ -21,7 +21,7 @@ protocol nsl3th1(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {P1,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); @@ -32,9 +32,5 @@ protocol nsl3th1(I,R) } } -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/compositionality-examples/th-1par2.spdl b/protocols/misc/compositionality-examples/th-1par2.spdl index f1f910e..82451a1 100644 --- a/protocols/misc/compositionality-examples/th-1par2.spdl +++ b/protocols/misc/compositionality-examples/th-1par2.spdl @@ -9,7 +9,7 @@ protocol nsl3th1(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {P1,I,ni}pk(R) ); @@ -23,7 +23,7 @@ protocol nsl3th1(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {P1,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); @@ -34,18 +34,14 @@ protocol nsl3th1(I,R) } } -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); protocol nsl3th2(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {P2,I,ni}pk(R) ); @@ -59,7 +55,7 @@ protocol nsl3th2(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {P2,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); @@ -70,9 +66,5 @@ protocol nsl3th2(I,R) } } -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/compositionality-examples/th-1seq2-rename-ni.spdl b/protocols/misc/compositionality-examples/th-1seq2-rename-ni.spdl index 0a6cc5d..082db56 100644 --- a/protocols/misc/compositionality-examples/th-1seq2-rename-ni.spdl +++ b/protocols/misc/compositionality-examples/th-1seq2-rename-ni.spdl @@ -8,7 +8,7 @@ protocol nsl3th3ni(I,R) { role I { - const ni,ni: Nonce; + fresh ni,ni: Nonce; var nr,nr2: Nonce; send_1(I,R, {P1,I,ni}pk(R) ); @@ -29,7 +29,7 @@ protocol nsl3th3ni(I,R) role R { var ni,ni: Nonce; - const nr,nr2: Nonce; + fresh nr,nr2: Nonce; read_1(I,R, {P1,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); @@ -48,9 +48,5 @@ protocol nsl3th3ni(I,R) } -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/compositionality-examples/th-1seq2-rename-nr.spdl b/protocols/misc/compositionality-examples/th-1seq2-rename-nr.spdl index fb899f2..3e016f9 100644 --- a/protocols/misc/compositionality-examples/th-1seq2-rename-nr.spdl +++ b/protocols/misc/compositionality-examples/th-1seq2-rename-nr.spdl @@ -8,7 +8,7 @@ protocol nsl3th3nr(I,R) { role I { - const ni,ni2: Nonce; + fresh ni,ni2: Nonce; var nr,nr: Nonce; send_1(I,R, {P1,I,ni}pk(R) ); @@ -29,7 +29,7 @@ protocol nsl3th3nr(I,R) role R { var ni,ni2: Nonce; - const nr,nr: Nonce; + fresh nr,nr: Nonce; read_1(I,R, {P1,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); @@ -48,9 +48,5 @@ protocol nsl3th3nr(I,R) } -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/compositionality-examples/th-1seq2.spdl b/protocols/misc/compositionality-examples/th-1seq2.spdl index 1301599..6e50f3c 100644 --- a/protocols/misc/compositionality-examples/th-1seq2.spdl +++ b/protocols/misc/compositionality-examples/th-1seq2.spdl @@ -8,7 +8,7 @@ protocol nsl3th3(I,R) { role I { - const ni,ni2: Nonce; + fresh ni,ni2: Nonce; var nr,nr2: Nonce; send_1(I,R, {P1,I,ni}pk(R) ); @@ -29,7 +29,7 @@ protocol nsl3th3(I,R) role R { var ni,ni2: Nonce; - const nr,nr2: Nonce; + fresh nr,nr2: Nonce; read_1(I,R, {P1,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); @@ -48,9 +48,5 @@ protocol nsl3th3(I,R) } -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/compositionality-examples/th-2.spdl b/protocols/misc/compositionality-examples/th-2.spdl index dbb6ee9..3332085 100644 --- a/protocols/misc/compositionality-examples/th-2.spdl +++ b/protocols/misc/compositionality-examples/th-2.spdl @@ -7,7 +7,7 @@ protocol nsl3th2(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {P2,I,ni}pk(R) ); @@ -21,7 +21,7 @@ protocol nsl3th2(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {P2,I,ni}pk(R) ); send_1b(R,I, {nr}pk(I) ); @@ -32,9 +32,5 @@ protocol nsl3th2(I,R) } } -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/denning-sacco-shared.spdl b/protocols/misc/denning-sacco-shared.spdl index 4ace1c8..0756c3b 100644 --- a/protocols/misc/denning-sacco-shared.spdl +++ b/protocols/misc/denning-sacco-shared.spdl @@ -17,13 +17,11 @@ secret k: Function; /* agents */ -const a,b,e: Agent; /* untrusted e */ untrusted e; -const ne: Nonce; const kee: SessionKey; compromised k(e,e); @@ -51,8 +49,8 @@ protocol denningsaccosh(A,S,B) role S { - const t: Time; - const kab: SessionKey; + fresh t: Time; + fresh kab: SessionKey; read_1 (A,S, A,S ); send_2 (S,A, {B, kab, t, { kab, A,t }k(B,S) }k(A,S) ); diff --git a/protocols/misc/f4.spdl b/protocols/misc/f4.spdl index eb1d54f..5b43bbb 100644 --- a/protocols/misc/f4.spdl +++ b/protocols/misc/f4.spdl @@ -28,15 +28,11 @@ protocol f4(I,R) role R { - const nr: Nonce; + fresh nr: Nonce; send_!1(R,I, nr ); } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/f5.spdl b/protocols/misc/f5.spdl index a0b8f7e..860c165 100644 --- a/protocols/misc/f5.spdl +++ b/protocols/misc/f5.spdl @@ -28,15 +28,11 @@ protocol f5(I,R) role R { - const nr: Nonce; + fresh nr: Nonce; send_!1(R,I, nr ); } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/five-run-bound.spdl b/protocols/misc/five-run-bound.spdl index c60735c..ee8d4c3 100644 --- a/protocols/misc/five-run-bound.spdl +++ b/protocols/misc/five-run-bound.spdl @@ -8,7 +8,7 @@ protocol r5bound(I,R) { var k1: Nonce; var ni: Nonce; - const k2: Nonce; + fresh k2: Nonce; read_!1 (I,R, ni ); send_!2 (R,I, { ni }sk(R) ); @@ -19,6 +19,4 @@ protocol r5bound(I,R) } } -const Alice, Bob: Agent; -const ne: Nonce; diff --git a/protocols/misc/fourway-HSDDM05.cpp b/protocols/misc/fourway-HSDDM05.cpp index dacd54f..5992e13 100644 --- a/protocols/misc/fourway-HSDDM05.cpp +++ b/protocols/misc/fourway-HSDDM05.cpp @@ -22,7 +22,7 @@ protocol fourway(X,Y) { role X { - const x: Nonce; + fresh x: Nonce; var y: Nonce; send_1( X,Y, x,msg1 ); @@ -37,7 +37,7 @@ protocol fourway(X,Y) role Y { var x: Nonce; - const y: Nonce; + fresh y: Nonce; read_1( X,Y, x,msg1 ); send_2( Y,X, y,msg2,hash( ptk,y,msg2 ) ); @@ -50,9 +50,4 @@ protocol fourway(X,Y) } -untrusted Eve; -compromised pmk(Eve,Alice); -compromised pmk(Eve,Bob); -compromised pmk(Alice,Eve); -compromised pmk(Bob,Eve); diff --git a/protocols/misc/fourway-HSDDM05.spdl b/protocols/misc/fourway-HSDDM05.spdl index 1edaf8e..4a91a9e 100644 --- a/protocols/misc/fourway-HSDDM05.spdl +++ b/protocols/misc/fourway-HSDDM05.spdl @@ -18,7 +18,7 @@ protocol fourway(X,Y) { role X { - const x: Nonce; + fresh x: Nonce; var y: Nonce; send_1( X,Y, x,msg1 ); @@ -33,7 +33,7 @@ protocol fourway(X,Y) role Y { var x: Nonce; - const y: Nonce; + fresh y: Nonce; read_1( X,Y, x,msg1 ); send_2( Y,X, y,msg2,hash( hash( pmk(X,Y),x,y ),y,msg2 ) ); @@ -46,8 +46,3 @@ protocol fourway(X,Y) } -untrusted Eve; -compromised pmk(Eve,Alice); -compromised pmk(Eve,Bob); -compromised pmk(Alice,Eve); -compromised pmk(Bob,Eve); diff --git a/protocols/misc/gong-nonce-b.spdl b/protocols/misc/gong-nonce-b.spdl index e9bb6d2..c9e85c0 100644 --- a/protocols/misc/gong-nonce-b.spdl +++ b/protocols/misc/gong-nonce-b.spdl @@ -14,9 +14,9 @@ protocol gongnonceb(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; - const ki: Keypart; + fresh ki: Keypart; var kr: Keypart; send_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni ); @@ -32,8 +32,8 @@ protocol gongnonceb(I,R,S) role R { var ni: Nonce; - const nr: Nonce; - const kr: Keypart; + fresh nr: Nonce; + fresh kr: Keypart; var ki: Keypart; read_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni ); @@ -59,23 +59,7 @@ protocol gongnonceb(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; -untrusted Eve; -const ne: Nonce; const kpe: Keypart; const ke: Sessionkey; -compromised k(Eve,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Simon); -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Simon,Eve); -run gongnonceb.I(Agent,Agent,Simon); -run gongnonceb.R(Agent,Agent,Simon); -run gongnonceb.S(Agent,Agent,Simon); -run gongnonceb.I(Agent,Agent,Simon); -run gongnonceb.R(Agent,Agent,Simon); -run gongnonceb.S(Agent,Agent,Simon); diff --git a/protocols/misc/gong-nonce.spdl b/protocols/misc/gong-nonce.spdl index 3670288..6cfb50c 100644 --- a/protocols/misc/gong-nonce.spdl +++ b/protocols/misc/gong-nonce.spdl @@ -6,9 +6,9 @@ protocol gongnonce(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; - const ki: Keypart; + fresh ki: Keypart; var kr: Keypart; send_1 (I,R, I,R,ni ); @@ -24,8 +24,8 @@ protocol gongnonce(I,R,S) role R { var ni: Nonce; - const nr: Nonce; - const kr: Keypart; + fresh nr: Nonce; + fresh kr: Keypart; var ki: Keypart; read_1 (I,R, I,R,ni ); @@ -50,23 +50,7 @@ protocol gongnonce(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; -untrusted Eve; -const ne: Nonce; const kpe: Keypart; const ke: Sessionkey; -compromised k(Eve,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Simon); -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Simon,Eve); -run gongnonce.I(Agent,Agent,Simon); -run gongnonce.R(Agent,Agent,Simon); -run gongnonce.S(Agent,Agent,Simon); -run gongnonce.I(Agent,Agent,Simon); -run gongnonce.R(Agent,Agent,Simon); -run gongnonce.S(Agent,Agent,Simon); diff --git a/protocols/misc/ibe-ns.spdl b/protocols/misc/ibe-ns.spdl index 5874e2e..f96db64 100644 --- a/protocols/misc/ibe-ns.spdl +++ b/protocols/misc/ibe-ns.spdl @@ -4,20 +4,17 @@ // The only requirement on the server communications is that the // sending of the private key is secret. -const pk: Function; //public-private keys are used to model a secure channel -secret sk: Function; //from the keyserver to the parties const ibepublic: Function; //publicly known key construction from server //parameters and recipient name secret ibesecret: Function;//secret key determined by server for recipient const param: Function; //public security parameter of server -inversekeys (pk,sk); inversekeys (ibepublic,ibesecret); protocol ibe(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; //Note that we are not interested in the order of server messages. @@ -36,7 +33,7 @@ protocol ibe(I,R,S) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_!2(S,R, {ibesecret(param(S),R)}pk(R) ); read_3(I,R, {I,ni}ibepublic(param(S),R) ); @@ -59,11 +56,6 @@ protocol ibe(I,R,S) } } -const Alice, Bob, Carol, Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); compromised ibesecret(param(Eve),Alice); compromised ibesecret(param(Eve),Bob); compromised ibesecret(param(Eve),Carol); diff --git a/protocols/misc/ibe.spdl b/protocols/misc/ibe.spdl index dc33589..d1b23d6 100644 --- a/protocols/misc/ibe.spdl +++ b/protocols/misc/ibe.spdl @@ -14,7 +14,7 @@ protocol ibe(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; read_1(S,I, param(S) ); send_3(I,R, {ni}ibepublic(param(S),R) ); @@ -40,11 +40,7 @@ protocol ibe(I,R,S) } } -const Alice, Bob, Carol, Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); compromised ibesecret(param(Eve),Alice); compromised ibesecret(param(Eve),Bob); compromised ibesecret(param(Eve),Carol); diff --git a/protocols/misc/isoiec11770-2-13.spdl b/protocols/misc/isoiec11770-2-13.spdl index 2be4d3d..4790421 100644 --- a/protocols/misc/isoiec11770-2-13.spdl +++ b/protocols/misc/isoiec11770-2-13.spdl @@ -6,7 +6,7 @@ protocol isoiec11770213(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: Sessionkey; @@ -19,8 +19,8 @@ protocol isoiec11770213(I,R,S) role R { var ni: Nonce; - const nr: Nonce; - const kir: Sessionkey; + fresh nr: Nonce; + fresh kir: Sessionkey; var T; read_1 (I,R, ni); @@ -41,23 +41,7 @@ protocol isoiec11770213(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; -untrusted Eve; -const ne: Nonce; const te: Ticket; const ke: Sessionkey; -compromised k(Eve,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Simon); -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Simon,Eve); -run isoiec11770213.I(Agent,Agent,Simon); -run isoiec11770213.R(Agent,Agent,Simon); -run isoiec11770213.S(Agent,Agent,Simon); -run isoiec11770213.I(Agent,Agent,Simon); -run isoiec11770213.R(Agent,Agent,Simon); -run isoiec11770213.S(Agent,Agent,Simon); diff --git a/protocols/misc/kaochow-palm.spdl b/protocols/misc/kaochow-palm.spdl index 559a5e1..9401811 100644 --- a/protocols/misc/kaochow-palm.spdl +++ b/protocols/misc/kaochow-palm.spdl @@ -6,7 +6,7 @@ protocol kaochowPalm(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: Sessionkey; @@ -22,7 +22,7 @@ protocol kaochowPalm(I,R,S) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; var kir: Sessionkey; var T; @@ -38,30 +38,14 @@ protocol kaochowPalm(I,R,S) role S { var ni: Nonce; - const kir: Sessionkey; + fresh kir: Sessionkey; read_1 (I,S, I,R,ni); send_2 (S,R, { {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) }k(R,S) ); } } -const Alice,Bob,Simon,Eve: Agent; -untrusted Eve; -const ne: Nonce; const te: Ticket; const ke: Sessionkey; -compromised k(Eve,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Simon); -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Simon,Eve); -run kaochowPalm.I(Agent,Agent,Simon); -run kaochowPalm.R(Agent,Agent,Simon); -run kaochowPalm.S(Agent,Agent,Simon); -run kaochowPalm.I(Agent,Agent,Simon); -run kaochowPalm.R(Agent,Agent,Simon); -run kaochowPalm.S(Agent,Agent,Simon); diff --git a/protocols/misc/kaochow-v2.spdl b/protocols/misc/kaochow-v2.spdl index edd8eb4..0265f3c 100644 --- a/protocols/misc/kaochow-v2.spdl +++ b/protocols/misc/kaochow-v2.spdl @@ -6,7 +6,7 @@ protocol kaochow2(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir,kt: Sessionkey; @@ -22,7 +22,7 @@ protocol kaochow2(I,R,S) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; var kir,kt: Sessionkey; var T: Ticket; @@ -38,30 +38,14 @@ protocol kaochow2(I,R,S) role S { var ni: Nonce; - const kir, kt: Sessionkey; + fresh kir, kt: Sessionkey; read_1 (I,S, I,R,ni); send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); } } -const Alice,Bob,Simon,Eve: Agent; -untrusted Eve; -const ne: Nonce; const te: Ticket; const ke: Sessionkey; -compromised k(Eve,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Simon); -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Simon,Eve); -run kaochow2.I(Agent,Agent,Simon); -run kaochow2.R(Agent,Agent,Simon); -run kaochow2.S(Agent,Agent,Simon); -run kaochow2.I(Agent,Agent,Simon); -run kaochow2.R(Agent,Agent,Simon); -run kaochow2.S(Agent,Agent,Simon); diff --git a/protocols/misc/kaochow-v3.spdl b/protocols/misc/kaochow-v3.spdl index 93669fd..61f6a7a 100644 --- a/protocols/misc/kaochow-v3.spdl +++ b/protocols/misc/kaochow-v3.spdl @@ -7,7 +7,7 @@ protocol kaochow3(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir,kt: Sessionkey; var T2: Ticket; @@ -24,10 +24,10 @@ protocol kaochow3(I,R,S) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; var kir,kt: Sessionkey; var T: Ticket; - const tr: Timestamp; + fresh tr: Timestamp; read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); @@ -41,30 +41,14 @@ protocol kaochow3(I,R,S) role S { var ni: Nonce; - const kir, kt: Sessionkey; + fresh kir, kt: Sessionkey; read_1 (I,S, I,R,ni); send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S) ); } } -const Alice,Bob,Simon,Eve: Agent; -untrusted Eve; -const ne: Nonce; const te: Ticket; const ke: Sessionkey; -compromised k(Eve,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Simon); -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Simon,Eve); -run kaochow3.I(Agent,Agent,Simon); -run kaochow3.R(Agent,Agent,Simon); -run kaochow3.S(Agent,Agent,Simon); -run kaochow3.I(Agent,Agent,Simon); -run kaochow3.R(Agent,Agent,Simon); -run kaochow3.S(Agent,Agent,Simon); diff --git a/protocols/misc/kaochow.spdl b/protocols/misc/kaochow.spdl index 5b17ef5..198d737 100644 --- a/protocols/misc/kaochow.spdl +++ b/protocols/misc/kaochow.spdl @@ -6,7 +6,7 @@ protocol kaochow(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: Sessionkey; @@ -22,7 +22,7 @@ protocol kaochow(I,R,S) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; var kir: Sessionkey; var T; @@ -38,30 +38,14 @@ protocol kaochow(I,R,S) role S { var ni: Nonce; - const kir: Sessionkey; + fresh kir: Sessionkey; read_1 (I,S, I,R,ni); send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S) ); } } -const Alice,Bob,Simon,Eve: Agent; -untrusted Eve; -const ne: Nonce; const te: Ticket; const ke: Sessionkey; -compromised k(Eve,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Eve,Simon); -compromised k(Alice,Eve); -compromised k(Bob,Eve); -compromised k(Simon,Eve); -run kaochow.I(Agent,Agent,Simon); -run kaochow.R(Agent,Agent,Simon); -run kaochow.S(Agent,Agent,Simon); -run kaochow.I(Agent,Agent,Simon); -run kaochow.R(Agent,Agent,Simon); -run kaochow.S(Agent,Agent,Simon); diff --git a/protocols/misc/kerberos-rddm.spdl b/protocols/misc/kerberos-rddm.spdl index fbcbda8..95c0598 100644 --- a/protocols/misc/kerberos-rddm.spdl +++ b/protocols/misc/kerberos-rddm.spdl @@ -58,13 +58,13 @@ protocol @swapkey-kst(I,R) protocol kerberos(C,K,T,S) { role C { - const n1: Nonce; - const n2: Nonce; + fresh n1: Nonce; + fresh n2: Nonce; var tgt: Ticket; var st: Ticket; var AKey: Sessionkey; var SKey: Sessionkey; - const t: Text; + fresh t: Text; send_1(C,K, C,T,n1); read_2(K,C, tgt, { AKey,n1,T }kck(C,K) ); @@ -94,7 +94,7 @@ protocol kerberos(C,K,T,S) { } role K { var n1: Nonce; - const AKey: Sessionkey; + fresh AKey: Sessionkey; read_1(C,K, C,T,n1); send_2(K,C, { AKey, C }ktk(T,K), { AKey,n1,T }kck(C,K) ); @@ -106,7 +106,7 @@ protocol kerberos(C,K,T,S) { role T { var AKey: Sessionkey; var n2: Nonce; - const SKey: Sessionkey; + fresh SKey: Sessionkey; read_3(C,T, { AKey, C }ktk(T,K), { C }AKey,C,S,n2 ); send_4(T,C, C,{ SKey, C }kst(S,T), { SKey, n2, S }AKey ); @@ -138,27 +138,14 @@ protocol kerberos(C,K,T,S) { } const Alice,Bob,Charlie,Eve: Agent; -untrusted Eve; // C untrusted -compromised kck(Eve,Alice); -compromised kck(Alice,Eve); // K untrusted -compromised kck(Eve,Alice); -compromised kck(Alice,Eve); -compromised ktk(Eve,Alice); -compromised ktk(Alice,Eve); // T untrusted -compromised kst(Alice,Eve); -compromised kst(Eve,Alice); -compromised ktk(Eve,Alice); -compromised ktk(Alice,Eve); // S untrusted -compromised kst(Alice,Eve); -compromised kst(Eve,Alice); diff --git a/protocols/misc/ksl.spdl b/protocols/misc/ksl.spdl index 635b311..a0b2eda 100644 --- a/protocols/misc/ksl.spdl +++ b/protocols/misc/ksl.spdl @@ -11,12 +11,10 @@ usertype Server, SessionKey, GeneralizedTimestamp, Ticket, TicketKey; secret k: Function; -const a, b, e: Agent; const s: Server; /* give the intruder something to work with */ -const ne: Nonce; const kee: SessionKey; untrusted e; compromised k(e,s); @@ -25,7 +23,7 @@ protocol ksl(A,B,S) { role A { - const Na, Ma: Nonce; + fresh Na, Ma: Nonce; var Nc, Mb: Nonce; var T: Ticket; var Kab: SessionKey; @@ -46,10 +44,10 @@ protocol ksl(A,B,S) role B { var Na,Ma: Nonce; - const Nb,Nc,Mb: Nonce; + fresh Nb,Nc,Mb: Nonce; var Kab: SessionKey; - const Kbb: TicketKey; - const Tb: GeneralizedTimestamp; + fresh Kbb: TicketKey; + fresh Tb: GeneralizedTimestamp; var T: Ticket; read_1(A,B, Na, A); @@ -70,14 +68,11 @@ protocol ksl(A,B,S) role S { var Na, Nb: Nonce; - const Kab: SessionKey; + fresh Kab: SessionKey; read_2(B,S, Na, A, Nb, B ); send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) ); } } -run ksl.A(a,b,s); -run ksl.B(a,b,s); -run ksl.S(a,b,s); diff --git a/protocols/misc/localclaims-breaker.spdl b/protocols/misc/localclaims-breaker.spdl index b54b315..3abbb42 100644 --- a/protocols/misc/localclaims-breaker.spdl +++ b/protocols/misc/localclaims-breaker.spdl @@ -15,7 +15,7 @@ protocol lcbreaker(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var x: Nonce; @@ -33,8 +33,8 @@ protocol lcbreaker(I,R) role R { var ni: Nonce; - const nr: Nonce; - const x: Nonce; + fresh nr: Nonce; + fresh x: Nonce; read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); @@ -48,9 +48,5 @@ protocol lcbreaker(I,R) } } -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/localclaims-seq1.spdl b/protocols/misc/localclaims-seq1.spdl index 16e5892..059159b 100644 --- a/protocols/misc/localclaims-seq1.spdl +++ b/protocols/misc/localclaims-seq1.spdl @@ -15,7 +15,7 @@ protocol lcbreakerS1(I,R) { role I { - const ni,ni2: Nonce; + fresh ni,ni2: Nonce; var nr: Nonce; var x: Nonce; @@ -36,8 +36,8 @@ protocol lcbreakerS1(I,R) role R { var ni,ni2: Nonce; - const nr: Nonce; - const x: Nonce; + fresh nr: Nonce; + fresh x: Nonce; read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); @@ -54,10 +54,6 @@ protocol lcbreakerS1(I,R) } } -const Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); + diff --git a/protocols/misc/localclaims.spdl b/protocols/misc/localclaims.spdl index 8a27b30..1623b5f 100644 --- a/protocols/misc/localclaims.spdl +++ b/protocols/misc/localclaims.spdl @@ -14,7 +14,7 @@ protocol localclaims(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; send_1(I,R, {ni}pk(R) ); @@ -33,13 +33,8 @@ protocol localclaims(I,R) // The agents in the system -const Alice,Bob: Agent; // An untrusted agent, with leaked information -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/ns-symmetric-amended.spdl b/protocols/misc/ns-symmetric-amended.spdl index 9231c85..d000f1b 100644 --- a/protocols/misc/ns-symmetric-amended.spdl +++ b/protocols/misc/ns-symmetric-amended.spdl @@ -10,13 +10,11 @@ secret k: Function; /* agents */ -const a,b,e: Agent; /* untrusted e */ untrusted e; -const ne: Nonce; const kee: SessionKey; compromised k(e,e); @@ -36,7 +34,7 @@ protocol nssymmetricamended(A,S,B) { role A { - const na: Nonce; + fresh na: Nonce; var T1: Ticket; var T2: Ticket; var kab: SessionKey; @@ -57,7 +55,7 @@ protocol nssymmetricamended(A,S,B) role S { - const kab: SessionKey; + fresh kab: SessionKey; var na: Nonce; var nb: Nonce; @@ -68,7 +66,7 @@ protocol nssymmetricamended(A,S,B) role B { var kab: SessionKey; - const nb: Nonce; + fresh nb: Nonce; read_1(A,B, A ); send_2(B,A, { A,nb }k(B,S) ); diff --git a/protocols/misc/ns-symmetric.spdl b/protocols/misc/ns-symmetric.spdl index 0eb0793..22c2366 100644 --- a/protocols/misc/ns-symmetric.spdl +++ b/protocols/misc/ns-symmetric.spdl @@ -9,13 +9,11 @@ secret k: Function; /* agents */ -const a,b,e: Agent; /* untrusted e */ untrusted e; -const ne: Nonce; const kee: SessionKey; compromised k(e,e); @@ -35,7 +33,7 @@ protocol nssymmetric(A,S,B) { role A { - const na: Nonce; + fresh na: Nonce; var T: Ticket; var kab: SessionKey; var nb: Nonce; @@ -51,7 +49,7 @@ protocol nssymmetric(A,S,B) role S { - const kab: SessionKey; + fresh kab: SessionKey; var na: Nonce; read_1(A,S, A,B,na ); @@ -61,7 +59,7 @@ protocol nssymmetric(A,S,B) role B { var kab: SessionKey; - const nb: Nonce; + fresh nb: Nonce; read_3(A,B, { kab,A }k(B,S) ); send_4(B,A, { nb }kab ); diff --git a/protocols/misc/ns3-brutus.spdl b/protocols/misc/ns3-brutus.spdl index b915956..1fd51b0 100644 --- a/protocols/misc/ns3-brutus.spdl +++ b/protocols/misc/ns3-brutus.spdl @@ -6,7 +6,7 @@ protocol ns3brutus(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {I,ni}pk(R) ); @@ -18,7 +18,7 @@ protocol ns3brutus(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr}pk(I) ); @@ -31,20 +31,13 @@ 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); +/* fresh nc: Nonce; */ /* pre-defined 10 runs, limit using --max-runs parameters */ /* to be nice to brutus, stupid scenario :( */ -run ns3brutus.R(Agent,Bob); run ns3brutus.I(Alice,Agent); -run ns3brutus.R(Agent,Bob); run ns3brutus.I(Alice,Agent); -run ns3brutus.R(Agent,Bob); run ns3brutus.I(Alice,Agent); -run ns3brutus.R(Agent,Bob); run ns3brutus.I(Alice,Agent); -run ns3brutus.R(Agent,Bob); run ns3brutus.I(Alice,Agent); diff --git a/protocols/misc/ns3.spdl b/protocols/misc/ns3.spdl index 44cb490..d0017c0 100644 --- a/protocols/misc/ns3.spdl +++ b/protocols/misc/ns3.spdl @@ -14,7 +14,7 @@ protocol ns3(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {I,ni}pk(R) ); @@ -29,7 +29,7 @@ protocol ns3(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr}pk(I) ); @@ -43,25 +43,10 @@ protocol ns3(I,R) // The agents in the system -const Alice,Bob: Agent; // An untrusted agent, with leaked information -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); // The runs (only needed for the modelchecker algorithm) -run ns3.I(Agent,Agent); -run ns3.R(Agent,Agent); -run ns3.I(Agent,Agent); -run ns3.R(Agent,Agent); -run ns3.I(Agent,Agent); -run ns3.R(Agent,Agent); -run ns3.I(Agent,Agent); -run ns3.R(Agent,Agent); -run ns3.I(Agent,Agent); -run ns3.R(Agent,Agent); diff --git a/protocols/misc/nsl3-nisynch-rep.spdl b/protocols/misc/nsl3-nisynch-rep.spdl index 104c8b8..991bf13 100644 --- a/protocols/misc/nsl3-nisynch-rep.spdl +++ b/protocols/misc/nsl3-nisynch-rep.spdl @@ -6,7 +6,7 @@ protocol nsl3rep(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {I,ni}pk(R) ); @@ -20,7 +20,7 @@ protocol nsl3rep(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {I,ni}pk(R) ); read_6(I,R, {I,ni}pk(R) ); @@ -31,13 +31,5 @@ protocol nsl3rep(I,R) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const nc: Nonce; -compromised sk(Eve); -run nsl3rep.I(Agent,Agent); -run nsl3rep.R(Agent,Agent); -run nsl3rep.I(Agent,Agent); -run nsl3rep.R(Agent,Agent); diff --git a/protocols/misc/nsl3.spdl b/protocols/misc/nsl3.spdl index 874a439..1028bf5 100644 --- a/protocols/misc/nsl3.spdl +++ b/protocols/misc/nsl3.spdl @@ -6,7 +6,7 @@ protocol nsl3(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {I,ni}pk(R) ); @@ -22,7 +22,7 @@ protocol nsl3(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); @@ -35,9 +35,5 @@ protocol nsl3(I,R) } } -const Eve: Agent; -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); diff --git a/protocols/misc/nst1.spdl b/protocols/misc/nst1.spdl index c915f61..85c21fb 100644 --- a/protocols/misc/nst1.spdl +++ b/protocols/misc/nst1.spdl @@ -12,20 +12,16 @@ usertype Server, SessionKey, TimeStamp, TicketKey; usertype ExpiredTimeStamp; secret k: Function; -const Alice, Bob, Simon, Eve: Agent; const Fresh: Function; const Compromised: Function; -const ne: Nonce; const kee: SessionKey; -untrusted Eve; -compromised k(Eve,Simon); protocol neustub(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var T: Ticket; var Tb: TimeStamp; @@ -46,12 +42,12 @@ protocol neustub(I,R,S) role R { var Ni,Mi: Nonce; - const Nr,Mr: Nonce; + fresh Nr,Mr: Nonce; var Kir: SessionKey; - const Tb: TimeStamp; + fresh Tb: TimeStamp; var T: Ticket; - const g: Ticket; + fresh g: Ticket; read_1(I,R, I, Ni); send_!2(R,S, R, {I, Ni, Tb, g}k(R,S),Nr); @@ -67,7 +63,7 @@ protocol neustub(I,R,S) role S { var Ni, Nr: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; var Tb: TimeStamp; var g: Ticket; diff --git a/protocols/misc/nst2.spdl b/protocols/misc/nst2.spdl index 431c36d..85b6cab 100644 --- a/protocols/misc/nst2.spdl +++ b/protocols/misc/nst2.spdl @@ -12,28 +12,24 @@ usertype Server, SessionKey, TimeStamp, TicketKey; usertype ExpiredTimeStamp; secret k: Function; -const Alice, Bob, Simon, Eve: Agent; const Fresh: Function; const Compromised: Function; -const ne: Nonce; const kee: SessionKey; -untrusted Eve; -compromised k(Eve,Simon); protocol neustub^Repeat(I,R,S) { - const Kir: SessionKey; + fresh Kir: SessionKey; role I { - const Mi: Nonce; + fresh Mi: Nonce; var Mr: Nonce; var Kir: SessionKey; var Tr: TimeStamp; var Tb: Ticket; - const g: Ticket; + fresh g: Ticket; var h: Ticket; read_!chain(R,I, { R,Tr,Kir }k(I,S), Tb); @@ -52,13 +48,13 @@ protocol neustub^Repeat(I,R,S) role R { - const Mr: Nonce; + fresh Mr: Nonce; var Tr: TimeStamp; var Kir: SessionKey; var Mi: Nonce; var g: Ticket; - const h: Ticket; + fresh h: Ticket; read_5(I,R,Mi,{I,Kir,Tr}k(R,S),g); send_6(R,I,{Mi,Mr,g,h}Kir); diff --git a/protocols/misc/otwayrees.spdl b/protocols/misc/otwayrees.spdl index b26552a..fea9d6d 100644 --- a/protocols/misc/otwayrees.spdl +++ b/protocols/misc/otwayrees.spdl @@ -1,4 +1,4 @@ -secret const k : Function; +secret fresh k : Function; /* Version from the Spore Librairy http://www.lsv.ens-cachan.fr/spore/otwayRees.html @@ -10,8 +10,8 @@ protocol otwayrees(A,B,S) { role A { - const na : Nonce; - const M : String; + fresh na : Nonce; + fresh M : String; var kab : SesKey; send_1(A,B, M,A,B, { na,M,A,B }k(A,S) ); @@ -25,7 +25,7 @@ protocol otwayrees(A,B,S) role B { var M : String; - const nb : Nonce; + fresh nb : Nonce; var kab : SesKey; var t1,t2; @@ -43,7 +43,7 @@ protocol otwayrees(A,B,S) { var na,nb : Nonce; var M : String; - const kab : SesKey; + fresh kab : SesKey; read_2(B,S, M,A,B, { na,M,A,B }k(A,S), { nb,M,A,B }k(B,S) ); send_3(S,B, M, { na,kab }k(A,S) , { nb,kab }k(B,S) ); @@ -53,14 +53,6 @@ protocol otwayrees(A,B,S) const Alice, Bob, Eve: Agent; const Simon: Server; -untrusted Eve; -compromised k(Eve,Simon); -run otwayrees.A(Alice, Agent, Simon); -run otwayrees.B(Agent, Bob, Simon); -run otwayrees.S(Agent, Agent, Simon); -run otwayrees.A(Agent, Agent, Simon); -run otwayrees.B(Agent, Agent, Simon); -run otwayrees.S(Agent, Agent, Simon); diff --git a/protocols/misc/samasc-broken.spdl b/protocols/misc/samasc-broken.spdl index ae7f2b3..765d190 100644 --- a/protocols/misc/samasc-broken.spdl +++ b/protocols/misc/samasc-broken.spdl @@ -13,7 +13,7 @@ protocol samascbroken(I,R) { role R { - const nr: Nonce; + fresh nr: Nonce; var kir: Key; read_!1a (I,R, { kir,I }pk(R) ); @@ -29,8 +29,6 @@ protocol samascbroken(I,R) } } -const a,b,e: Agent; untrusted e; compromised sk(e); -const ne: Nonce; diff --git a/protocols/misc/simplest.spdl b/protocols/misc/simplest.spdl index 53bf29f..c800620 100644 --- a/protocols/misc/simplest.spdl +++ b/protocols/misc/simplest.spdl @@ -1,14 +1,12 @@ secret k: Nonce; -const Alice,Bob,Charlie: Agent; -const ne: Nonce; protocol simplest(I) { role I { var x: Nonce; - const n: Nonce; + fresh n: Nonce; read_!1(I,I, x); send_!2(I,I, n, {n, x}k ); diff --git a/protocols/misc/soph-keyexch.spdl b/protocols/misc/soph-keyexch.spdl index 611ba09..75ccaa1 100644 --- a/protocols/misc/soph-keyexch.spdl +++ b/protocols/misc/soph-keyexch.spdl @@ -7,8 +7,8 @@ protocol sophkx(I,R) { role I { - const ni: Nonce; - const kir: Sessionkey; + fresh ni: Nonce; + fresh kir: Sessionkey; var nr: Nonce; send_1(I,R, ni, {I,kir}pk(R) ); @@ -20,20 +20,13 @@ protocol sophkx(I,R) { var ni: Nonce; var kir: Sessionkey; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, ni, {I,kir}pk(R) ); send_2(R,I, {ni}kir ); } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const nc: Nonce; const ke: Sessionkey; -compromised sk(Eve); -run sophkx.I(Agent,Agent); -run sophkx.R(Agent,Agent); -run sophkx.I(Agent,Agent); diff --git a/protocols/misc/soph.spdl b/protocols/misc/soph.spdl index 174f9e1..13f5946 100644 --- a/protocols/misc/soph.spdl +++ b/protocols/misc/soph.spdl @@ -6,7 +6,7 @@ protocol soph(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; send_1(I,R, {I,ni}pk(R) ); read_2(R,I, ni ); @@ -22,13 +22,5 @@ protocol soph(I,R) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const nc: Nonce; -compromised sk(Eve); -run soph.I(Agent,Agent); -run soph.R(Agent,Agent); -run soph.I(Agent,Agent); -run soph.R(Agent,Agent); diff --git a/protocols/misc/speedtest.spdl b/protocols/misc/speedtest.spdl index 3b9b72e..4a311fe 100644 --- a/protocols/misc/speedtest.spdl +++ b/protocols/misc/speedtest.spdl @@ -6,7 +6,7 @@ protocol ns3speedtest(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {I,ni}pk(R) ); @@ -18,7 +18,7 @@ protocol ns3speedtest(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {I,ni}pk(R) ); send_2(R,I, {ni,nr}pk(I) ); @@ -27,23 +27,14 @@ protocol ns3speedtest(I,R) } } -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); diff --git a/protocols/misc/splice-as-hc-cj.spdl b/protocols/misc/splice-as-hc-cj.spdl index 1463e61..635c35f 100644 --- a/protocols/misc/splice-as-hc-cj.spdl +++ b/protocols/misc/splice-as-hc-cj.spdl @@ -8,9 +8,9 @@ protocol spliceAShcCJ(C,AS,S) { role C { - const N1,N2: Nonce; - const T: TimeStamp; - const L: LifeTime; + fresh N1,N2: Nonce; + fresh T: TimeStamp; + fresh L: LifeTime; send_1(C,AS, C, S, N1 ); read_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); @@ -34,13 +34,13 @@ protocol spliceAShcCJ(C,AS,S) role S { - const N3: Nonce; + fresh N3: Nonce; var N2: Nonce; var T: TimeStamp; var L: LifeTime; var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_3(C,S, C, S, {T, L, {C, N2}pk(S)}sk(C) ); send_4(S,AS, S, C, N3 ); @@ -53,14 +53,7 @@ protocol spliceAShcCJ(C,AS,S) } } -const Al,Bo,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - -run spliceAShcCJ.C(Agent,Agent,Agent); -run spliceAShcCJ.AS(Agent,Agent,Agent); -run spliceAShcCJ.S(Agent,Agent,Agent); + + diff --git a/protocols/misc/splice-as-hc.spdl b/protocols/misc/splice-as-hc.spdl index d2bf6d5..ff773dc 100644 --- a/protocols/misc/splice-as-hc.spdl +++ b/protocols/misc/splice-as-hc.spdl @@ -8,9 +8,9 @@ protocol spliceAShc(C,AS,S) { role C { - const N1,N2: Nonce; - const T: TimeStamp; - const L: LifeTime; + fresh N1,N2: Nonce; + fresh T: TimeStamp; + fresh L: LifeTime; send_1(C,AS, C, S, N1 ); read_2(AS,C, AS, {AS, C, N1, S, pk(S)}sk(AS) ); @@ -34,13 +34,13 @@ protocol spliceAShc(C,AS,S) role S { - const N3: Nonce; + fresh N3: Nonce; var N2: Nonce; var T: TimeStamp; var L: LifeTime; var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); send_4(S,AS, S, C, N3 ); @@ -53,14 +53,7 @@ protocol spliceAShc(C,AS,S) } } -const Al,Bo,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - -run spliceAShc.C(Agent,Agent,Agent); -run spliceAShc.AS(Agent,Agent,Agent); -run spliceAShc.S(Agent,Agent,Agent); + + diff --git a/protocols/misc/splice-as.spdl b/protocols/misc/splice-as.spdl index 788cdca..abaca41 100644 --- a/protocols/misc/splice-as.spdl +++ b/protocols/misc/splice-as.spdl @@ -8,9 +8,9 @@ protocol spliceAS(C,AS,S) { role C { - const N1,N2: Nonce; - const T: TimeStamp; - const L: LifeTime; + fresh N1,N2: Nonce; + fresh T: TimeStamp; + fresh L: LifeTime; send_1(C,AS, C, S, N1 ); read_2(AS,C, AS, {AS, C, N1, pk(S)}sk(AS) ); @@ -34,13 +34,13 @@ protocol spliceAS(C,AS,S) role S { - const N3: Nonce; + fresh N3: Nonce; var N2: Nonce; var T: TimeStamp; var L: LifeTime; var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_3(C,S, C, S, {C, T, L, {N2}pk(S)}sk(C) ); send_4(S,AS, S, C, N3 ); @@ -53,14 +53,7 @@ protocol spliceAS(C,AS,S) } } -const Al,Bo,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - -run spliceAS.C(Agent,Agent,Agent); -run spliceAS.AS(Agent,Agent,Agent); -run spliceAS.S(Agent,Agent,Agent); + + diff --git a/protocols/misc/tls/tls-BM-1.m4 b/protocols/misc/tls/tls-BM-1.m4 index 2ccada2..bc48e10 100644 --- a/protocols/misc/tls/tls-BM-1.m4 +++ b/protocols/misc/tls/tls-BM-1.m4 @@ -30,8 +30,8 @@ protocol tls-bm-1(A,B) { role A { - const na: Nonce; - const pmk: Nonce; + fresh na: Nonce; + fresh pmk: Nonce; var nb: Nonce; send_1( A,B, msg1 ); @@ -47,7 +47,7 @@ protocol tls-bm-1(A,B) { var na: Nonce; var pmk: Nonce; - const nb: Nonce; + fresh nb: Nonce; read_1( A,B, msg1 ); send_2( B,A, msg2 ); @@ -60,6 +60,4 @@ protocol tls-bm-1(A,B) } -untrusted Eve; -compromised sk(Eve); diff --git a/protocols/misc/tls/tls-BM-1.spdl b/protocols/misc/tls/tls-BM-1.spdl index bd9287a..1adf816 100644 --- a/protocols/misc/tls/tls-BM-1.spdl +++ b/protocols/misc/tls/tls-BM-1.spdl @@ -30,8 +30,8 @@ protocol tls-bm-1(A,B) { role A { - const na: Nonce; - const pmk: Nonce; + fresh na: Nonce; + fresh pmk: Nonce; var nb: Nonce; send_1( A,B, na ); @@ -47,7 +47,7 @@ protocol tls-bm-1(A,B) { var na: Nonce; var pmk: Nonce; - const nb: Nonce; + fresh nb: Nonce; read_1( A,B, na ); send_2( B,A, nb ); @@ -60,6 +60,4 @@ protocol tls-bm-1(A,B) } -untrusted Eve; -compromised sk(Eve); diff --git a/protocols/misc/tls/tls-HSDDM05-2.cpp b/protocols/misc/tls/tls-HSDDM05-2.cpp index 9d21a41..fa40d5f 100644 --- a/protocols/misc/tls/tls-HSDDM05-2.cpp +++ b/protocols/misc/tls/tls-HSDDM05-2.cpp @@ -47,9 +47,9 @@ protocol tls-HSDDM05(X,Y) { role X { - const Nx: Nonce; - const msecret: Nonce; - const pa: Params; + fresh Nx: Nonce; + fresh msecret: Nonce; + fresh pa: Params; var Ny: Nonce; var pb: Params; @@ -66,8 +66,8 @@ protocol tls-HSDDM05(X,Y) var Nx: Nonce; var msecret: Nonce; var pa: Params; - const Ny: Nonce; - const pb: Params; + fresh Ny: Nonce; + fresh pb: Params; read_1( X,Y, msg1 ); send_2( Y,X, msg2 ); @@ -79,6 +79,4 @@ protocol tls-HSDDM05(X,Y) } -untrusted Eve; -compromised sk(Eve); diff --git a/protocols/misc/tls/tls-HSDDM05-2.spdl b/protocols/misc/tls/tls-HSDDM05-2.spdl index c1ab0e9..8ed52cc 100644 --- a/protocols/misc/tls/tls-HSDDM05-2.spdl +++ b/protocols/misc/tls/tls-HSDDM05-2.spdl @@ -19,9 +19,9 @@ protocol tls-HSDDM05(X,Y) { role X { - const Nx: Nonce; - const msecret: Nonce; - const pa: Params; + fresh Nx: Nonce; + fresh msecret: Nonce; + fresh pa: Params; var Ny: Nonce; var pb: Params; @@ -38,8 +38,8 @@ protocol tls-HSDDM05(X,Y) var Nx: Nonce; var msecret: Nonce; var pa: Params; - const Ny: Nonce; - const pb: Params; + fresh Ny: Nonce; + fresh pb: Params; read_1( X,Y, X,Nx,pa ); send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); @@ -51,5 +51,3 @@ protocol tls-HSDDM05(X,Y) } -untrusted Eve; -compromised sk(Eve); diff --git a/protocols/misc/tls/tls-HSDDM05-fix.cpp b/protocols/misc/tls/tls-HSDDM05-fix.cpp index 3b94979..82cbc0a 100644 --- a/protocols/misc/tls/tls-HSDDM05-fix.cpp +++ b/protocols/misc/tls/tls-HSDDM05-fix.cpp @@ -37,9 +37,9 @@ protocol tls-HSDDM05(X,Y) { role X { - const Nx: Nonce; - const msecret: Nonce; - const pa: Params; + fresh Nx: Nonce; + fresh msecret: Nonce; + fresh pa: Params; var Ny: Nonce; var pb: Params; @@ -56,8 +56,8 @@ protocol tls-HSDDM05(X,Y) var Nx: Nonce; var msecret: Nonce; var pa: Params; - const Ny: Nonce; - const pb: Params; + fresh Ny: Nonce; + fresh pb: Params; read_1( X,Y, msg1 ); send_2( Y,X, msg2 ); @@ -69,6 +69,4 @@ protocol tls-HSDDM05(X,Y) } -untrusted Eve; -compromised sk(Eve); diff --git a/protocols/misc/tls/tls-HSDDM05-fix.m4 b/protocols/misc/tls/tls-HSDDM05-fix.m4 index 5a96b3b..9abe9c7 100644 --- a/protocols/misc/tls/tls-HSDDM05-fix.m4 +++ b/protocols/misc/tls/tls-HSDDM05-fix.m4 @@ -38,9 +38,9 @@ protocol tls-HSDDM05(X,Y) { role X { - const Nx: Nonce; - const msecret: Nonce; - const pa: Params; + fresh Nx: Nonce; + fresh msecret: Nonce; + fresh pa: Params; var Ny: Nonce; var pb: Params; @@ -57,8 +57,8 @@ protocol tls-HSDDM05(X,Y) var Nx: Nonce; var msecret: Nonce; var pa: Params; - const Ny: Nonce; - const pb: Params; + fresh Ny: Nonce; + fresh pb: Params; read_1( X,Y, msg1 ); send_2( Y,X, msg2 ); @@ -70,6 +70,4 @@ protocol tls-HSDDM05(X,Y) } -untrusted Eve; -compromised sk(Eve); diff --git a/protocols/misc/tls/tls-HSDDM05-fix.spdl b/protocols/misc/tls/tls-HSDDM05-fix.spdl index 7bfdf81..c3820fc 100644 --- a/protocols/misc/tls/tls-HSDDM05-fix.spdl +++ b/protocols/misc/tls/tls-HSDDM05-fix.spdl @@ -38,9 +38,9 @@ protocol tls-HSDDM05(X,Y) { role X { - const Nx: Nonce; - const msecret: Nonce; - const pa: Params; + fresh Nx: Nonce; + fresh msecret: Nonce; + fresh pa: Params; var Ny: Nonce; var pb: Params; @@ -57,8 +57,8 @@ protocol tls-HSDDM05(X,Y) var Nx: Nonce; var msecret: Nonce; var pa: Params; - const Ny: Nonce; - const pb: Params; + fresh Ny: Nonce; + fresh pb: Params; read_1( X,Y, X,Nx,pa ); send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); @@ -70,6 +70,4 @@ protocol tls-HSDDM05(X,Y) } -untrusted Eve; -compromised sk(Eve); diff --git a/protocols/misc/tls/tls-HSDDM05.cpp b/protocols/misc/tls/tls-HSDDM05.cpp index afe1fc7..182f171 100644 --- a/protocols/misc/tls/tls-HSDDM05.cpp +++ b/protocols/misc/tls/tls-HSDDM05.cpp @@ -41,9 +41,9 @@ protocol tls-HSDDM05(X,Y) { role X { - const Nx: Nonce; - const msecret: Nonce; - const pa: Params; + fresh Nx: Nonce; + fresh msecret: Nonce; + fresh pa: Params; var Ny: Nonce; var pb: Params; @@ -60,8 +60,8 @@ protocol tls-HSDDM05(X,Y) var Nx: Nonce; var msecret: Nonce; var pa: Params; - const Ny: Nonce; - const pb: Params; + fresh Ny: Nonce; + fresh pb: Params; read_1( X,Y, msg1 ); send_2( Y,X, msg2 ); @@ -73,6 +73,4 @@ protocol tls-HSDDM05(X,Y) } -untrusted Eve; -compromised sk(Eve); diff --git a/protocols/misc/tls/tls-HSDDM05.spdl b/protocols/misc/tls/tls-HSDDM05.spdl index 9908063..cb9b1e9 100644 --- a/protocols/misc/tls/tls-HSDDM05.spdl +++ b/protocols/misc/tls/tls-HSDDM05.spdl @@ -19,9 +19,9 @@ protocol tls-HSDDM05(X,Y) { role X { - const Nx: Nonce; - const msecret: Nonce; - const pa: Params; + fresh Nx: Nonce; + fresh msecret: Nonce; + fresh pa: Params; var Ny: Nonce; var pb: Params; @@ -38,8 +38,8 @@ protocol tls-HSDDM05(X,Y) var Nx: Nonce; var msecret: Nonce; var pa: Params; - const Ny: Nonce; - const pb: Params; + fresh Ny: Nonce; + fresh pb: Params; read_1( X,Y, X,Nx,pa ); send_2( Y,X, Ny,pb,{ Y,pk(Y) }sk(Terence) ); @@ -51,5 +51,3 @@ protocol tls-HSDDM05(X,Y) } -untrusted Eve; -compromised sk(Eve); diff --git a/protocols/misc/tls/tls-paulson-avispa.cpp b/protocols/misc/tls/tls-paulson-avispa.cpp index 0fa2389..aef2211 100644 --- a/protocols/misc/tls/tls-paulson-avispa.cpp +++ b/protocols/misc/tls/tls-paulson-avispa.cpp @@ -34,7 +34,6 @@ secret unkeygen: Function; inversekeys(keygen, unkeygen); const pa,pb: Params; -const Terence: Agent; const false,true: Bool; @@ -42,9 +41,9 @@ protocol tlspaulson-avispa(a,b) { role a { - const na: Nonce; - const sid: SessionID; - const pms: Nonce; + fresh na: Nonce; + fresh sid: SessionID; + fresh pms: Nonce; var nb: Nonce; var pb: Params; @@ -68,8 +67,8 @@ protocol tlspaulson-avispa(a,b) var na: Nonce; var sid: SessionID; var pms: Nonce; - const nb: Nonce; - const pb: Params; + fresh nb: Nonce; + fresh pb: Params; read_1( a,b, a,na,sid,pa ); send_2( b,a, nb,sid,pb ); @@ -86,11 +85,7 @@ protocol tlspaulson-avispa(a,b) } } -const Alice, Bob, Eve: Agent; -untrusted Eve; -compromised sk(Eve); -const ne: Nonce; const side: SessionID; const pe: Params; diff --git a/protocols/misc/tls/tls-paulson-avispa.spdl b/protocols/misc/tls/tls-paulson-avispa.spdl index 19c11cc..9f67636 100644 --- a/protocols/misc/tls/tls-paulson-avispa.spdl +++ b/protocols/misc/tls/tls-paulson-avispa.spdl @@ -15,9 +15,6 @@ secret unkeygen: Function; inversekeys(keygen, unkeygen); const pa,pb: Params; -const Alice,Bob: Agent; -const Terence: Agent; -const Sally: Agent; const false,true: Bool; @@ -25,9 +22,9 @@ protocol tlspaulson-avispa(a,b) { role a { - const na: Nonce; - const sid: SessionID; - const pms: Nonce; + fresh na: Nonce; + fresh sid: SessionID; + fresh pms: Nonce; var nb: Nonce; var pb: Params; @@ -51,8 +48,8 @@ protocol tlspaulson-avispa(a,b) var na: Nonce; var sid: SessionID; var pms: Nonce; - const nb: Nonce; - const pb: Params; + fresh nb: Nonce; + fresh pb: Params; read_1( a,b, a,na,sid,pa ); send_2( b,a, nb,sid,pb ); @@ -69,10 +66,6 @@ protocol tlspaulson-avispa(a,b) } } -const Alice, Bob, Eve: Agent; -untrusted Eve; -compromised sk(Eve); -const ne: Nonce; const side: SessionID; const pe: Params; diff --git a/protocols/misc/tls/tls-paulson.cpp b/protocols/misc/tls/tls-paulson.cpp index 5d0369e..7147024 100644 --- a/protocols/misc/tls/tls-paulson.cpp +++ b/protocols/misc/tls/tls-paulson.cpp @@ -26,7 +26,6 @@ inversekeys(pk,sk); inversekeys(hash,unhash); const pa,pb: Params; -const Terence: Agent; const false,true: Bool; @@ -34,9 +33,9 @@ protocol tlspaulson(a,b) { role a { - const na: Nonce; - const sid: SessionID; - const pms: Nonce; + fresh na: Nonce; + fresh sid: SessionID; + fresh pms: Nonce; var nb: Nonce; var pb: Params; @@ -59,8 +58,8 @@ protocol tlspaulson(a,b) var na: Nonce; var sid: SessionID; var pms: Nonce; - const nb: Nonce; - const pb: Params; + fresh nb: Nonce; + fresh pb: Params; read_1( a,b, a,na,sid,pa ); send_2( b,a, nb,sid,pb ); @@ -76,20 +75,8 @@ protocol tlspaulson(a,b) } } -const Alice, Bob, Eve: Agent; -untrusted Eve; -compromised sk(Eve); -const ne: Nonce; const side: SessionID; const pe: Params; -run tlspaulson.a(Agent,Agent); -run tlspaulson.b(Agent,Agent); -run tlspaulson.a(Agent,Agent); -run tlspaulson.b(Agent,Agent); -run tlspaulson.a(Agent,Agent); -run tlspaulson.b(Agent,Agent); -run tlspaulson.a(Agent,Agent); -run tlspaulson.b(Agent,Agent); diff --git a/protocols/misc/tls/tls-paulson.spdl b/protocols/misc/tls/tls-paulson.spdl index d750c36..c385cd3 100644 --- a/protocols/misc/tls/tls-paulson.spdl +++ b/protocols/misc/tls/tls-paulson.spdl @@ -11,7 +11,6 @@ inversekeys(pk,sk); inversekeys(hash,unhash); const pa,pb: Params; -const Terence: Agent; const false,true: Bool; @@ -19,9 +18,9 @@ protocol tlspaulson(a,b) { role a { - const na: Nonce; - const sid: SessionID; - const pms: Nonce; + fresh na: Nonce; + fresh sid: SessionID; + fresh pms: Nonce; var nb: Nonce; var pb: Params; @@ -44,8 +43,8 @@ protocol tlspaulson(a,b) var na: Nonce; var sid: SessionID; var pms: Nonce; - const nb: Nonce; - const pb: Params; + fresh nb: Nonce; + fresh pb: Params; read_1( a,b, a,na,sid,pa ); send_2( b,a, nb,sid,pb ); @@ -61,19 +60,7 @@ protocol tlspaulson(a,b) } } -const Alice, Bob, Eve: Agent; -untrusted Eve; -compromised sk(Eve); -const ne: Nonce; const side: SessionID; const pe: Params; -run tlspaulson.a(Agent,Agent); -run tlspaulson.b(Agent,Agent); -run tlspaulson.a(Agent,Agent); -run tlspaulson.b(Agent,Agent); -run tlspaulson.a(Agent,Agent); -run tlspaulson.b(Agent,Agent); -run tlspaulson.a(Agent,Agent); -run tlspaulson.b(Agent,Agent); diff --git a/protocols/misc/tmn-Gijs.spdl b/protocols/misc/tmn-Gijs.spdl index b9179cf..55893cf 100644 --- a/protocols/misc/tmn-Gijs.spdl +++ b/protocols/misc/tmn-Gijs.spdl @@ -9,7 +9,7 @@ protocol tmn(A,B,S) { role A { - const Ka: Key; + fresh Ka: Key; var Kb: Key; send_1(A,S, B,{Ka}pk(S) ); @@ -21,7 +21,7 @@ protocol tmn(A,B,S) role B { - const Kb: Key; + fresh Kb: Key; read_2(S,B, A ); send_3(B,S, A, { Kb }pk(S) ); @@ -46,11 +46,7 @@ const Alice,Bob,Eve,Simon: Agent; const Ke: Key; -untrusted Eve; -compromised sk(Eve); # Scenario to recreate an attack in SPORE -run tmn.B (Alice,Bob,Simon); -run tmn.S (Alice,Bob,Simon); diff --git a/protocols/misc/tmn.spdl b/protocols/misc/tmn.spdl index bdd0dab..d1baab3 100644 --- a/protocols/misc/tmn.spdl +++ b/protocols/misc/tmn.spdl @@ -8,7 +8,7 @@ protocol tmn(A,B,S) { role A { - const Ka: Key; + fresh Ka: Key; var Kb: Key; send_1(A,S, B,{Ka}pk(S) ); @@ -20,7 +20,7 @@ protocol tmn(A,B,S) role B { - const Kb: Key; + fresh Kb: Key; read_2(S,B, A ); send_3(B,S, A, { Kb }pk(S) ); @@ -43,14 +43,6 @@ protocol tmn(A,B,S) const Alice,Bob,Eve,Simon: Agent; -untrusted Eve; -compromised sk(Eve); - -run tmn.A (Agent,Agent,Simon); -run tmn.A (Agent,Agent,Simon); -run tmn.B (Agent,Agent,Simon); -run tmn.B (Agent,Agent,Simon); -run tmn.S (Agent,Agent,Simon); -run tmn.S (Agent,Agent,Simon); + diff --git a/protocols/misc/unknown2.spdl b/protocols/misc/unknown2.spdl index acfefcb..1ce13fb 100644 --- a/protocols/misc/unknown2.spdl +++ b/protocols/misc/unknown2.spdl @@ -5,7 +5,7 @@ protocol unknown2(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: SessionKey; var T; @@ -21,7 +21,7 @@ protocol unknown2(I,R,S) role R { - const nr: Nonce; + fresh nr: Nonce; var ni: Nonce; var kir: SessionKey; @@ -36,7 +36,7 @@ protocol unknown2(I,R,S) role S { - const kir: SessionKey; + fresh kir: SessionKey; var ni,nr: Nonce; read_2(R,S, { I,R,ni,nr }k(R,S) ); @@ -50,20 +50,6 @@ protocol unknown2(I,R,S) } } -const Alice,Bob,Eve: Agent; -untrusted Eve; -const ne: Nonce; const kee: SessionKey; -compromised k(Eve,Eve); -compromised k(Eve,Alice); -compromised k(Eve,Bob); -compromised k(Alice,Eve); -compromised k(Bob,Eve); -run unknown2.I(Agent,Agent,Agent); -run unknown2.R(Agent,Agent,Agent); -run unknown2.S(Agent,Agent,Agent); -run unknown2.R(Agent,Agent,Agent); -run unknown2.I(Agent,Agent,Agent); -run unknown2.S(Agent,Agent,Agent); diff --git a/protocols/misc/wmf-brutus.spdl b/protocols/misc/wmf-brutus.spdl index a68c7ac..08335db 100644 --- a/protocols/misc/wmf-brutus.spdl +++ b/protocols/misc/wmf-brutus.spdl @@ -1,5 +1,5 @@ usertype SesKey, Server; -secret const k : Function; +secret fresh k : Function; /* Version from the Brutus reports */ @@ -8,7 +8,7 @@ protocol wmfbrutus(A,B,S) { role A { - const kab : SesKey; + fresh kab : SesKey; send_1(A,S, A, { B,kab }k(A,S) ); } @@ -34,15 +34,6 @@ protocol wmfbrutus(A,B,S) const Alice, Bob, Eve: Agent; const Simon: Server; -untrusted Eve; -compromised k(Eve,Simon); -run wmfbrutus.A(Agent, Agent, Simon); -run wmfbrutus.B(Agent, Agent, Simon); -run wmfbrutus.A(Agent, Agent, Simon); -run wmfbrutus.B(Agent, Agent, Simon); -run wmfbrutus.A(Agent, Agent, Simon); -run wmfbrutus.B(Agent, Agent, Simon); -run wmfbrutus.S(Agent, Agent, Simon); diff --git a/protocols/misc/woolam-cmv.spdl b/protocols/misc/woolam-cmv.spdl index b20aeda..f101e8d 100644 --- a/protocols/misc/woolam-cmv.spdl +++ b/protocols/misc/woolam-cmv.spdl @@ -5,16 +5,12 @@ usertype Server, SessionKey, Token, Ticket; secret k: Function; -const Alice, Bob, Charlie, Eve: Agent; const Simon: Server; /* give the intruder something to work with */ // Scyther finds an attack using basic type flaws -const ne: Nonce; const ke: SessionKey; -untrusted Eve; -compromised k(Eve,Simon); const authToken: Token; @@ -22,7 +18,7 @@ protocol woolamcmv(A,B,S) { role A { - const Na: Nonce; + fresh Na: Nonce; var Nb: Nonce; var Kab: SessionKey; var t1,t2; @@ -41,7 +37,7 @@ protocol woolamcmv(A,B,S) role B { var Na: Nonce; - const Nb: Nonce; + fresh Nb: Nonce; var Kab: SessionKey; var t1,t2; @@ -61,7 +57,7 @@ protocol woolamcmv(A,B,S) role S { var Na, Nb: Nonce; - const Kab: SessionKey; + fresh Kab: SessionKey; read_4(B,S, { A,B, Na,Nb }k(A,S), { A,B,Na,Nb }k(B,S) ); send_5(S,B, { B,Na,Nb,Kab }k(A,S), { A,Na,Nb,Kab }k(B,S) ); @@ -70,6 +66,4 @@ protocol woolamcmv(A,B,S) } } -run woolamcmv.B(Alice,Bob,Simon); -run woolamcmv.B(Alice,Bob,Simon); diff --git a/protocols/misc/woolam-pi-f.spdl b/protocols/misc/woolam-pi-f.spdl index 20145da..ab2d8fb 100644 --- a/protocols/misc/woolam-pi-f.spdl +++ b/protocols/misc/woolam-pi-f.spdl @@ -7,13 +7,9 @@ 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) { @@ -28,7 +24,7 @@ protocol woolampif(A,B,S) role B { - const Nb: Nonce; + fresh Nb: Nonce; var T: Ticket; read_1(A,B, A); @@ -50,6 +46,4 @@ protocol woolampif(A,B,S) } } -run woolampif.B(Alice,Bob,Simon); -run woolampif.B(Alice,Bob,Simon); diff --git a/protocols/misc/yahalom-ban.spdl b/protocols/misc/yahalom-ban.spdl index b3ee2cd..90bf4fd 100644 --- a/protocols/misc/yahalom-ban.spdl +++ b/protocols/misc/yahalom-ban.spdl @@ -15,7 +15,7 @@ protocol yahalomBan(A,B,S) { role A { - const na; + fresh na; var nb; var ticket; var kab; @@ -28,7 +28,7 @@ protocol yahalomBan(A,B,S) role B { - const nb; + fresh nb; var na; var ticket; var kab; @@ -41,7 +41,7 @@ protocol yahalomBan(A,B,S) role S { - const kab; + fresh kab; var na,nb; read_2(B,S, B,nb, {A,na}k(B,S) ); diff --git a/protocols/misc/yahalom-lowe.spdl b/protocols/misc/yahalom-lowe.spdl index dc6251b..d4660a5 100644 --- a/protocols/misc/yahalom-lowe.spdl +++ b/protocols/misc/yahalom-lowe.spdl @@ -5,19 +5,15 @@ usertype Sessionkey; -const Alice,Bob,Simon,Eve : Agent; secret k : Function; -untrusted Eve; -compromised k(Eve,Simon); -const ne: Nonce; const kee: Sessionkey; protocol yahalomlowe(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: Sessionkey; @@ -32,7 +28,7 @@ protocol yahalomlowe(I,R,S) role R { - const nr: Nonce; + fresh nr: Nonce; var ni: Nonce; var kir: Sessionkey; @@ -47,7 +43,7 @@ protocol yahalomlowe(I,R,S) role S { - const kir: Sessionkey; + fresh kir: Sessionkey; var ni,nr: Nonce; read_2(R,S, {I,ni,nr}k(R,S) ); @@ -56,10 +52,5 @@ protocol yahalomlowe(I,R,S) } } -run yahalomlowe.I(Agent,Agent,Simon); -run yahalomlowe.R(Agent,Agent,Simon); -run yahalomlowe.S(Agent,Agent,Simon); -run yahalomlowe.I(Agent,Agent,Simon); -run yahalomlowe.R(Agent,Agent,Simon); diff --git a/protocols/misc/yahalom-paulson.spdl b/protocols/misc/yahalom-paulson.spdl index 282c02a..f10fcc6 100644 --- a/protocols/misc/yahalom-paulson.spdl +++ b/protocols/misc/yahalom-paulson.spdl @@ -5,19 +5,15 @@ usertype Sessionkey, Ticket; -const Alice,Bob,Simon,Eve : Agent; secret k : Function; -untrusted Eve; -compromised k(Eve,Simon); -const ne: Nonce; const kee: Sessionkey; protocol yahalompaulson(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: Sessionkey; var T: Ticket; @@ -33,7 +29,7 @@ protocol yahalompaulson(I,R,S) role R { - const nr: Nonce; + fresh nr: Nonce; var ni: Nonce; var kir: Sessionkey; @@ -48,7 +44,7 @@ protocol yahalompaulson(I,R,S) role S { - const kir: Sessionkey; + fresh kir: Sessionkey; var ni,nr: Nonce; read_2(R,S, R,nr, {I,ni}k(R,S) ); @@ -56,10 +52,5 @@ protocol yahalompaulson(I,R,S) } } -run yahalompaulson.I(Agent,Agent,Simon); -run yahalompaulson.R(Agent,Agent,Simon); -run yahalompaulson.S(Agent,Agent,Simon); -run yahalompaulson.I(Agent,Agent,Simon); -run yahalompaulson.R(Agent,Agent,Simon);