diff --git a/gui/Protocols/MultiProtocolAttacks/BKE.spdl b/gui/Protocols/MultiProtocolAttacks/BKE.spdl index 426ac1b..1afa87f 100644 --- a/gui/Protocols/MultiProtocolAttacks/BKE.spdl +++ b/gui/Protocols/MultiProtocolAttacks/BKE.spdl @@ -37,9 +37,4 @@ protocol bke(I,R) } } -// An untrusted agent, with leaked information - -const Eve: Agent; -untrusted Eve; -compromised sk(Eve); diff --git a/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl b/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl index e9a31b4..c5389b3 100644 --- a/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl +++ b/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl @@ -65,9 +65,3 @@ protocol andrew-Concrete(I,R) } } -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -const kee: SessionKey; - diff --git a/gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl b/gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl index 3866337..51f140e 100644 --- a/gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl +++ b/gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl @@ -50,14 +50,3 @@ protocol andrew-Ban(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); - diff --git a/gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl b/gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl index 1123ed8..bb00132 100644 --- a/gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl +++ b/gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl @@ -55,16 +55,3 @@ protocol andrew-LoweBan(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); - - - diff --git a/gui/Protocols/MultiProtocolAttacks/boyd.spdl b/gui/Protocols/MultiProtocolAttacks/boyd.spdl index 48f4c9f..a5b915d 100644 --- a/gui/Protocols/MultiProtocolAttacks/boyd.spdl +++ b/gui/Protocols/MultiProtocolAttacks/boyd.spdl @@ -54,17 +54,3 @@ protocol boyd(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -const mcsde: Macseed; -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); - diff --git a/gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl b/gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl index 6834104..c633587 100644 --- a/gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl +++ b/gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl @@ -37,9 +37,3 @@ protocol ccitt509-ban3(I,R) } } -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - diff --git a/gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl b/gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl index b406a62..213c80d 100644 --- a/gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl +++ b/gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl @@ -63,12 +63,4 @@ protocol denningSacco-Lowe(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const kee: SessionKey; -const tee: TimeStamp; -compromised k(Eve,Simon); - - diff --git a/gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl b/gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl index 5a2f224..8bcf846 100644 --- a/gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl +++ b/gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl @@ -51,12 +51,5 @@ protocol denningSacco(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const kee: SessionKey; -const tee: TimeStamp; -compromised k(Eve,Simon); - diff --git a/gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl b/gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl index 894ae70..6b9943e 100644 --- a/gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl +++ b/gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl @@ -58,17 +58,3 @@ 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); - diff --git a/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl b/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl index 801e5a2..9040e40 100644 --- a/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl +++ b/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl @@ -55,17 +55,3 @@ 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); - diff --git a/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl b/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl index 735b869..a8eac3b 100644 --- a/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl +++ b/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl @@ -40,17 +40,3 @@ 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); - diff --git a/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl b/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl index a3f937b..be1c4c8 100644 --- a/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl +++ b/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl @@ -53,17 +53,3 @@ protocol kaochow-2(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); - diff --git a/gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl b/gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl index eeb43ed..0bfc94a 100644 --- a/gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl +++ b/gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl @@ -57,17 +57,3 @@ protocol kaochow-3(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); - diff --git a/gui/Protocols/MultiProtocolAttacks/kaochow.spdl b/gui/Protocols/MultiProtocolAttacks/kaochow.spdl index 7724a72..4126ec3 100644 --- a/gui/Protocols/MultiProtocolAttacks/kaochow.spdl +++ b/gui/Protocols/MultiProtocolAttacks/kaochow.spdl @@ -53,17 +53,3 @@ protocol kaochow(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); - diff --git a/gui/Protocols/MultiProtocolAttacks/ksl.spdl b/gui/Protocols/MultiProtocolAttacks/ksl.spdl index 25042a7..58856fc 100644 --- a/gui/Protocols/MultiProtocolAttacks/ksl.spdl +++ b/gui/Protocols/MultiProtocolAttacks/ksl.spdl @@ -9,21 +9,16 @@ usertype Server, SessionKey, TimeStamp, TicketKey; usertype ExpiredTimeStamp; -const a, b, e: Agent; -const s: Server; const Fresh: Function; const Compromised: Function; -untrusted e; -compromised k(e,s); - protocol ksl(I,R,S) { role I { - const Ni, Mi: Nonce; + fresh Ni, Mi: Nonce; var Nc, Mr: Nonce; var T: Ticket; var Kir: SessionKey; @@ -45,10 +40,10 @@ protocol ksl(I,R,S) role R { var Ni,Mi: Nonce; - const Nr,Nc,Mr: Nonce; + fresh Nr,Nc,Mr: Nonce; var Kir: SessionKey; - const Kbb: TicketKey; - const Tr: TimeStamp; + fresh Kbb: TicketKey; + fresh Tr: TimeStamp; var T: Ticket; read_1(I,R, Ni, I); @@ -70,7 +65,7 @@ protocol ksl(I,R,S) role S { var Ni, Nr: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; read_2(R,S, Ni, I, Nr, R ); send_3(S,R, { Nr, I, Kir }k(R,S), { Ni,R,Kir }k(I,S) ); diff --git a/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl index 4488fb6..7c96390 100644 --- a/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl +++ b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl @@ -64,10 +64,3 @@ protocol needhamschroedersk-amend(I,R,S) } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised k(Eve,Simon); - - diff --git a/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl index 964ae05..50c87d4 100644 --- a/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl +++ b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl @@ -54,9 +54,3 @@ protocol needhamschroedersk(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised k(Eve,Simon); - diff --git a/gui/Protocols/MultiProtocolAttacks/ns3.spdl b/gui/Protocols/MultiProtocolAttacks/ns3.spdl index fea06ab..b860cbf 100644 --- a/gui/Protocols/MultiProtocolAttacks/ns3.spdl +++ b/gui/Protocols/MultiProtocolAttacks/ns3.spdl @@ -39,8 +39,3 @@ protocol ns3(I,R) } } -// An untrusted agent, with leaked information - -const Eve: Agent; -untrusted Eve; -compromised sk(Eve); diff --git a/gui/Protocols/MultiProtocolAttacks/nsl3.spdl b/gui/Protocols/MultiProtocolAttacks/nsl3.spdl index 479bbbb..af99579 100644 --- a/gui/Protocols/MultiProtocolAttacks/nsl3.spdl +++ b/gui/Protocols/MultiProtocolAttacks/nsl3.spdl @@ -37,8 +37,3 @@ protocol nsl3(I,R) } } -// An untrusted agent, with leaked information - -const Eve: Agent; -untrusted Eve; -compromised sk(Eve); diff --git a/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl b/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl index 7fee42e..64b99dc 100644 --- a/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl +++ b/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl @@ -54,8 +54,3 @@ protocol otwayrees(I,R,S) } } -const Alice, Bob, Eve, Simon: Agent; - -untrusted Eve; -compromised k(Eve,Simon); - diff --git a/gui/Protocols/MultiProtocolAttacks/soph.spdl b/gui/Protocols/MultiProtocolAttacks/soph.spdl index be14707..c6e3223 100644 --- a/gui/Protocols/MultiProtocolAttacks/soph.spdl +++ b/gui/Protocols/MultiProtocolAttacks/soph.spdl @@ -19,9 +19,3 @@ protocol soph(I,R) } } -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const nc: Nonce; -compromised sk(Eve); - diff --git a/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl b/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl index 351faab..87960b3 100644 --- a/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl +++ b/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl @@ -64,9 +64,3 @@ protocol spliceAS-CJ(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - diff --git a/gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl b/gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl index cf5feb9..858e02a 100644 --- a/gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl +++ b/gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl @@ -7,9 +7,6 @@ usertype TimeStamp, LifeTime; -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); const inc,dec: Function; inversekeys (inc,dec); @@ -62,11 +59,3 @@ protocol spliceAS-HC(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - - - diff --git a/gui/Protocols/MultiProtocolAttacks/splice-as.spdl b/gui/Protocols/MultiProtocolAttacks/splice-as.spdl index 01f8552..9890adb 100644 --- a/gui/Protocols/MultiProtocolAttacks/splice-as.spdl +++ b/gui/Protocols/MultiProtocolAttacks/splice-as.spdl @@ -64,9 +64,3 @@ protocol spliceAS(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - diff --git a/gui/Protocols/MultiProtocolAttacks/tmn.spdl b/gui/Protocols/MultiProtocolAttacks/tmn.spdl index d80fe8a..267d30f 100644 --- a/gui/Protocols/MultiProtocolAttacks/tmn.spdl +++ b/gui/Protocols/MultiProtocolAttacks/tmn.spdl @@ -49,12 +49,3 @@ protocol tmn(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Ke: SessionKey; - - -untrusted Eve; -compromised sk(Eve); - - - diff --git a/gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl b/gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl index e980104..618acef 100644 --- a/gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl +++ b/gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl @@ -30,11 +30,3 @@ protocol wmfbrutus(A,B,S) } } -const Alice, Bob, Eve: Agent; -const Simon: Server; - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl b/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl index 7fbce47..61c5b7f 100644 --- a/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl +++ b/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl @@ -61,13 +61,3 @@ protocol wmf-Lowe(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Ke: SessionKey; -const Te: TimeStamp; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/MultiProtocolAttacks/wmf.spdl b/gui/Protocols/MultiProtocolAttacks/wmf.spdl index f893d76..4c787a8 100644 --- a/gui/Protocols/MultiProtocolAttacks/wmf.spdl +++ b/gui/Protocols/MultiProtocolAttacks/wmf.spdl @@ -52,13 +52,3 @@ protocol wmf(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Ke: SessionKey; -const Te: TimeStamp; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl index 0db8c2a..d38c837 100644 --- a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-1.spdl @@ -18,7 +18,7 @@ protocol woolamPi-1(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var T: Ticket; read_1(I,R, I); @@ -39,13 +39,3 @@ protocol woolamPi-1(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Te: Ticket; -const Ne: Nonce; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl index dc6b0d4..10b61d4 100644 --- a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-2.spdl @@ -18,7 +18,7 @@ protocol woolamPi-2(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var T: Ticket; read_1(I,R, I); @@ -39,13 +39,3 @@ protocol woolamPi-2(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Te: Ticket; -const Ne: Nonce; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl index 847416b..65b074f 100644 --- a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-3.spdl @@ -18,7 +18,7 @@ protocol woolamPi-3(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var T: Ticket; read_1(I,R, I); @@ -39,13 +39,3 @@ protocol woolamPi-3(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Te: Ticket; -const Ne: Nonce; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl index 1d2cd7e..80f3312 100644 --- a/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl @@ -39,11 +39,3 @@ protocol woolamPi-f(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Te: Ticket; -const Ne: Nonce; - - -untrusted Eve; -compromised k(Eve,Simon); - diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl index 8cf2bb9..ee9805b 100644 --- a/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl @@ -9,9 +9,6 @@ usertype Server; usertype SessionKey; -const a,b,c : Agent; -const s : Server; - protocol yahalom-BAN-Paulson-modified(A,B,S) { role A diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl index 16e29ca..40cfee7 100644 --- a/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl @@ -7,9 +7,6 @@ usertype Server; usertype SessionKey; -const a,b,c : Agent; -const s : Server; - protocol yahalom-BAN-Paulson(A,B,S) { role A diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl index d4d6cba..9119065 100644 --- a/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl @@ -52,5 +52,4 @@ protocol yahalom-BAN(I,R,S) } } -const Alice,Bob,Charlie,David: Agent; diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl index 3656625..921e30a 100644 --- a/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl @@ -50,5 +50,4 @@ protocol yahalom-Lowe(I,R,S) } } -const Alice,Bob,Simon : Agent; diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom.spdl index c99d8dc..e949cc6 100644 --- a/gui/Protocols/MultiProtocolAttacks/yahalom.spdl +++ b/gui/Protocols/MultiProtocolAttacks/yahalom.spdl @@ -50,10 +50,3 @@ protocol yahalom(I,R,S) } } -const Alice,Bob,Simon : Agent; - -const Eve: Agent; -untrusted Eve; - -compromised k(Eve,Simon); - diff --git a/gui/Protocols/andrew-ban-concrete.spdl b/gui/Protocols/andrew-ban-concrete.spdl index dd2c417..b85a74f 100644 --- a/gui/Protocols/andrew-ban-concrete.spdl +++ b/gui/Protocols/andrew-ban-concrete.spdl @@ -17,7 +17,6 @@ # usertype SessionKey; -secret k: Function; const Fresh: Function; const Compromised: Function; @@ -38,7 +37,7 @@ protocol andrew-Concrete(I,R) role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: SessionKey; @@ -54,8 +53,8 @@ protocol andrew-Concrete(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}k(I,R) ); @@ -67,9 +66,3 @@ protocol andrew-Concrete(I,R) } } -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -const kee: SessionKey; - diff --git a/gui/Protocols/andrew-ban.spdl b/gui/Protocols/andrew-ban.spdl index 653ad87..663ab4c 100644 --- a/gui/Protocols/andrew-ban.spdl +++ b/gui/Protocols/andrew-ban.spdl @@ -12,7 +12,6 @@ # According to SPORE there are no known attacks on this protocol # usertype SessionKey; -secret k: Function; const Fresh: Function; const Compromised: Function; @@ -20,7 +19,7 @@ protocol andrew-Ban(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr,nr2: Nonce; var kir: SessionKey; @@ -38,8 +37,8 @@ protocol andrew-Ban(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) ); @@ -53,14 +52,3 @@ protocol andrew-Ban(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); - diff --git a/gui/Protocols/andrew-lowe-ban.spdl b/gui/Protocols/andrew-lowe-ban.spdl index 1f24904..bb00132 100644 --- a/gui/Protocols/andrew-lowe-ban.spdl +++ b/gui/Protocols/andrew-lowe-ban.spdl @@ -19,7 +19,6 @@ # usertype SessionKey; -secret k: Function; const Fresh: Function; const Compromised: Function; @@ -27,7 +26,7 @@ protocol andrew-LoweBan(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: SessionKey; @@ -43,8 +42,8 @@ protocol andrew-LoweBan(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,R}k(I,R) ); @@ -56,16 +55,3 @@ protocol andrew-LoweBan(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); - - - diff --git a/gui/Protocols/andrew.spdl b/gui/Protocols/andrew.spdl index ded8fec..2597353 100644 --- a/gui/Protocols/andrew.spdl +++ b/gui/Protocols/andrew.spdl @@ -10,7 +10,6 @@ # usertype SessionKey; -secret k: Function; const succ: Function; const Fresh: Function; const Compromised: Function; @@ -19,7 +18,7 @@ protocol andrew(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr,nr2: Nonce; var kir: SessionKey; @@ -36,8 +35,8 @@ protocol andrew(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, {succ(ni),nr}k(I,R) ); @@ -50,16 +49,3 @@ protocol andrew(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); - - - diff --git a/gui/Protocols/ccitt509-1.spdl b/gui/Protocols/ccitt509-1.spdl index 5ed23ba..1308afb 100644 --- a/gui/Protocols/ccitt509-1.spdl +++ b/gui/Protocols/ccitt509-1.spdl @@ -9,17 +9,14 @@ # which can currently not be modelled in scyther # -const pk: Function; -secret sk: Function; -inversekeys(pk,sk); usertype Timestamp; protocol ccitt509-1(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}pk(R)}sk(I)); # claim_2(I,Nisynch); # This claim is useless as there are no preceding read events @@ -36,11 +33,3 @@ protocol ccitt509-1(I,R) } } -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -const te: Timestamp; -compromised sk(Eve); - - diff --git a/gui/Protocols/ccitt509-1c.spdl b/gui/Protocols/ccitt509-1c.spdl index 228550c..7adccd3 100644 --- a/gui/Protocols/ccitt509-1c.spdl +++ b/gui/Protocols/ccitt509-1c.spdl @@ -7,10 +7,7 @@ # According to SPORE there are no known attacks on this protocol # -const pk,hash: Function; -secret sk,unhash: Function; -inversekeys (hash,unhash); -inversekeys(pk,sk); +hashfunction hash; usertype Timestamp; protocol ccitt509-1c(I,R) @@ -35,10 +32,3 @@ protocol ccitt509-1c(I,R) } } -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -const te: Timestamp; -compromised sk(Eve); - diff --git a/gui/Protocols/ccitt509-3.spdl b/gui/Protocols/ccitt509-3.spdl index e8ae1f1..cf5f926 100644 --- a/gui/Protocols/ccitt509-3.spdl +++ b/gui/Protocols/ccitt509-3.spdl @@ -8,18 +8,15 @@ # this can not be verified using scyther # -const pk: Function; -secret sk: Function; -inversekeys(pk,sk); usertype Timestamp; protocol ccitt509-3(I,R) { role I { - const Ta: Timestamp; + fresh Ta: Timestamp; var Tb: Timestamp; - const Na,Xa,Ya: Nonce; + fresh Na,Xa,Ya: Nonce; var Xb,Nb,Yb: Nonce; send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); read_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); @@ -32,9 +29,9 @@ protocol ccitt509-3(I,R) role R { var Ta: Timestamp; - const Tb: Timestamp; + fresh Tb: Timestamp; var Na,Xa,Ya: Nonce; - const Xb,Yb,Nb: Nonce; + fresh Xb,Yb,Nb: Nonce; read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); send_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); @@ -46,10 +43,3 @@ protocol ccitt509-3(I,R) } } -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -const te: Timestamp; -compromised sk(Eve); - diff --git a/gui/Protocols/ccitt509-ban3.spdl b/gui/Protocols/ccitt509-ban3.spdl index 9c0d3c1..ec442f2 100644 --- a/gui/Protocols/ccitt509-ban3.spdl +++ b/gui/Protocols/ccitt509-ban3.spdl @@ -11,10 +11,6 @@ # According to SPORE there are no known attacks on this protocol # -const pk: Function; -secret sk: Function; -inversekeys(pk,sk); - protocol ccitt509-ban3(I,R) { role I @@ -41,9 +37,3 @@ protocol ccitt509-ban3(I,R) } } -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - diff --git a/gui/Protocols/denning-sacco-lowe.spdl b/gui/Protocols/denning-sacco-lowe.spdl index 1365e6c..28d9132 100644 --- a/gui/Protocols/denning-sacco-lowe.spdl +++ b/gui/Protocols/denning-sacco-lowe.spdl @@ -11,7 +11,6 @@ usertype Key; usertype SessionKey; usertype TimeStamp; usertype ExpiredTimeStamp; -secret k: Function; usertype PseudoFunction; const dec: PseudoFunction; const Fresh: Function; @@ -41,7 +40,7 @@ protocol denningSacco-Lowe(I,R,S) { var Kir: SessionKey; var T: TimeStamp; - const Nr: Nonce; + fresh Nr: Nonce; read_3(I,R, {Kir,I,T}k(R,S)); send_4(R,I, {Nr}Kir); @@ -55,20 +54,11 @@ protocol denningSacco-Lowe(I,R,S) role S { var W: Ticket; - const Kir: SessionKey; - const T: TimeStamp; + fresh Kir: SessionKey; + fresh T: TimeStamp; read_1(I,S, I,R ); send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const kee: SessionKey; -const tee: TimeStamp; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/denning-sacco.spdl b/gui/Protocols/denning-sacco.spdl index 329c69c..32f76cb 100644 --- a/gui/Protocols/denning-sacco.spdl +++ b/gui/Protocols/denning-sacco.spdl @@ -8,7 +8,6 @@ usertype Key; usertype SessionKey; usertype TimeStamp; usertype ExpiredTimeStamp; -secret k: Function; const Fresh: Function; const Compromised: Function; @@ -44,20 +43,11 @@ protocol denningSacco(I,R,S) role S { var W: Ticket; - const Kir: SessionKey; - const T: TimeStamp; + fresh Kir: SessionKey; + fresh T: TimeStamp; read_1(I,S, I,R ); send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S)); } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const kee: SessionKey; -const tee: TimeStamp; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/kaochow-v2.spdl b/gui/Protocols/kaochow-v2.spdl index b19a94e..be1c4c8 100644 --- a/gui/Protocols/kaochow-v2.spdl +++ b/gui/Protocols/kaochow-v2.spdl @@ -5,7 +5,6 @@ # usertype SessionKey; -secret k: Function; const Fresh: Function; const Compromised: Function; @@ -13,7 +12,7 @@ protocol kaochow-2(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir,kt: SessionKey; @@ -30,7 +29,7 @@ protocol kaochow-2(I,R,S) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; var kir,kt: SessionKey; var T: Ticket; @@ -47,24 +46,10 @@ protocol kaochow-2(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); - diff --git a/gui/Protocols/kaochow-v3.spdl b/gui/Protocols/kaochow-v3.spdl index 1afe57e..0bfc94a 100644 --- a/gui/Protocols/kaochow-v3.spdl +++ b/gui/Protocols/kaochow-v3.spdl @@ -7,7 +7,6 @@ usertype SessionKey; usertype ExpiredTimeStamp; usertype TimeStamp; -secret k: Function; const Fresh: Function; const Compromised: Function; @@ -15,7 +14,7 @@ protocol kaochow-3(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir,kt: SessionKey; var T2: Ticket; @@ -33,10 +32,10 @@ protocol kaochow-3(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, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) ); @@ -51,24 +50,10 @@ protocol kaochow-3(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); - diff --git a/gui/Protocols/kaochow.spdl b/gui/Protocols/kaochow.spdl index 01b378d..4126ec3 100644 --- a/gui/Protocols/kaochow.spdl +++ b/gui/Protocols/kaochow.spdl @@ -5,7 +5,6 @@ # usertype SessionKey; -secret k: Function; const Fresh: Function; const Compromised: Function; @@ -13,7 +12,7 @@ protocol kaochow(I,R,S) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; var kir: SessionKey; @@ -30,7 +29,7 @@ protocol kaochow(I,R,S) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; var kir: SessionKey; var T; @@ -47,24 +46,10 @@ 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); - diff --git a/gui/Protocols/ksl-lowe.spdl b/gui/Protocols/ksl-lowe.spdl index 948d8da..468e8fe 100644 --- a/gui/Protocols/ksl-lowe.spdl +++ b/gui/Protocols/ksl-lowe.spdl @@ -9,24 +9,15 @@ usertype Server, SessionKey, TimeStamp, TicketKey; usertype ExpiredTimeStamp; -secret k: Function; -const a, b, e: Agent; -const s: Server; const Fresh: Function; const Compromised: Function; - -const ne: Nonce; -const kee: SessionKey; -untrusted e; -compromised k(e,s); - protocol ksl-Lowe(I,R,S) { role I { - const Ni, Mi: Nonce; + fresh Ni, Mi: Nonce; var Nc, Mr: Nonce; var T: Ticket; var Kir: SessionKey; @@ -48,10 +39,10 @@ protocol ksl-Lowe(I,R,S) role R { var Ni,Mi: Nonce; - const Nr,Nc,Mr: Nonce; + fresh Nr,Nc,Mr: Nonce; var Kir: SessionKey; - const Kbb: TicketKey; - const Tr: TimeStamp; + fresh Kbb: TicketKey; + fresh Tr: TimeStamp; var T: Ticket; read_1(I,R, Ni, I); @@ -73,11 +64,10 @@ protocol ksl-Lowe(I,R,S) role S { var Ni, Nr: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; read_2(R,S, Ni, I, Nr, R ); send_3(S,R, { I, Nr, Kir }k(R,S), { Ni,R,Kir }k(I,S) ); } } - diff --git a/gui/Protocols/ksl.spdl b/gui/Protocols/ksl.spdl index 62b247e..75cfeb9 100644 --- a/gui/Protocols/ksl.spdl +++ b/gui/Protocols/ksl.spdl @@ -8,25 +8,15 @@ usertype Server, SessionKey, TimeStamp, TicketKey; usertype ExpiredTimeStamp; -secret k: Function; -const a, b, e: Agent; -const s: Server; const Fresh: Function; const Compromised: Function; -const ne: Nonce; -const kee: SessionKey; -untrusted e; -compromised k(e,s); - - - protocol ksl(I,R,S) { role I { - const Ni, Mi: Nonce; + fresh Ni, Mi: Nonce; var Nc, Mr: Nonce; var T: Ticket; var Kir: SessionKey; @@ -48,10 +38,10 @@ protocol ksl(I,R,S) role R { var Ni,Mi: Nonce; - const Nr,Nc,Mr: Nonce; + fresh Nr,Nc,Mr: Nonce; var Kir: SessionKey; - const Kbb: TicketKey; - const Tr: TimeStamp; + fresh Kbb: TicketKey; + fresh Tr: TimeStamp; var T: Ticket; read_1(I,R, Ni, I); @@ -73,11 +63,10 @@ protocol ksl(I,R,S) role S { var Ni, Nr: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; read_2(R,S, Ni, I, Nr, R ); send_3(S,R, { Nr, I, Kir }k(R,S), { Ni,R,Kir }k(I,S) ); } } - diff --git a/gui/Protocols/needham-schroeder-lowe.spdl b/gui/Protocols/needham-schroeder-lowe.spdl index 638f5ab..8abb407 100644 --- a/gui/Protocols/needham-schroeder-lowe.spdl +++ b/gui/Protocols/needham-schroeder-lowe.spdl @@ -10,16 +10,11 @@ # synchronisation and agreement, because the keys that the server sends # out can be replayed. -secret pk: Function; # For some reason SPORE models it such that the agents - # do not know the public keys of the other agents -secret sk: Function; -inversekeys(pk,sk); - protocol needhamschroederpk-Lowe(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; send_1(I,S, (I,R)); @@ -34,7 +29,7 @@ protocol needhamschroederpk-Lowe(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var Ni: Nonce; read_3(I,R,{Ni,I}pk(R)); @@ -56,11 +51,3 @@ protocol needhamschroederpk-Lowe(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); -compromised pk(Eve); -compromised pk(Simon); # Needed because of the way SPORE models nsl - diff --git a/gui/Protocols/needham-schroeder-sk-amend.spdl b/gui/Protocols/needham-schroeder-sk-amend.spdl index 7554dc7..7c96390 100644 --- a/gui/Protocols/needham-schroeder-sk-amend.spdl +++ b/gui/Protocols/needham-schroeder-sk-amend.spdl @@ -10,7 +10,6 @@ -secret k: Function; # Model dec that is invertible by inc const dec,inc: Function; inversekeys(dec,inc); @@ -22,7 +21,7 @@ protocol needhamschroedersk-amend(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var Kir: SessionKey; var T,T2: Ticket; @@ -42,7 +41,7 @@ protocol needhamschroedersk-amend(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var Kir: SessionKey; read_1(I,R,I); @@ -58,17 +57,10 @@ protocol needhamschroedersk-amend(I,R,S) role S { var Ni,Nr: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; read_3(I,S,(I,R,Ni,{I,Nr}k(R,S))); send_4(S,I,{Ni,R,Kir,{Kir,Nr,I}k(R,S)}k(I,S)); } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised k(Eve,Simon); - - diff --git a/gui/Protocols/needham-schroeder-sk.spdl b/gui/Protocols/needham-schroeder-sk.spdl index 38b9919..50c87d4 100644 --- a/gui/Protocols/needham-schroeder-sk.spdl +++ b/gui/Protocols/needham-schroeder-sk.spdl @@ -6,7 +6,6 @@ # -secret k: Function; # Model dec that is invertible by inc const dec,inc: Function; inversekeys(dec,inc); @@ -18,7 +17,7 @@ protocol needhamschroedersk(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var Kir: SessionKey; var T: Ticket; @@ -35,7 +34,7 @@ protocol needhamschroedersk(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var Kir: SessionKey; read_3(I,R,{Kir,I}k(R,S)); @@ -49,15 +48,9 @@ protocol needhamschroedersk(I,R,S) role S { var Ni: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; read_1(I,S,(I,R,Ni)); send_2(S,I,{Ni,R,Kir,{Kir,I}k(R,S)}k(I,S)); } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised k(Eve,Simon); - diff --git a/gui/Protocols/needham-schroeder.spdl b/gui/Protocols/needham-schroeder.spdl index fda6c8c..76db7c2 100644 --- a/gui/Protocols/needham-schroeder.spdl +++ b/gui/Protocols/needham-schroeder.spdl @@ -10,16 +10,11 @@ # synchronisation and agreement, because the keys that the server sends # out can be replayed. -secret pk: Function; # For some reason SPORE models it such that the agents - # do not know the public keys of the other agents -secret sk: Function; -inversekeys(pk,sk); - protocol needhamschroederpk(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; send_1(I,S,(I,R)); @@ -34,7 +29,7 @@ protocol needhamschroederpk(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var Ni: Nonce; read_3(I,R,{Ni,I}pk(R)); @@ -56,12 +51,3 @@ protocol needhamschroederpk(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); -compromised pk(Eve); -compromised pk(Simon); # Needed because SPORE only assumes agents know their - # own public key and that of the server - diff --git a/gui/Protocols/neumannstub-guttman-hwang.spdl b/gui/Protocols/neumannstub-guttman-hwang.spdl index 8353535..f7266be 100644 --- a/gui/Protocols/neumannstub-guttman-hwang.spdl +++ b/gui/Protocols/neumannstub-guttman-hwang.spdl @@ -10,27 +10,20 @@ 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-GuttmanHwang^Repeat(I,R,S) { - const Kir: SessionKey; + fresh Kir: SessionKey; role I { - const Mi: Nonce; + fresh Mi: Nonce; var Mr: Nonce; - const Kir: SessionKey; - const Tr: TimeStamp; + fresh Kir: SessionKey; + fresh Tr: TimeStamp; send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); read_6(R,I,{Mi,Mr}Kir); @@ -43,7 +36,7 @@ protocol neustub-GuttmanHwang^Repeat(I,R,S) role R { - const Mr: Nonce; + fresh Mr: Nonce; var Tr: TimeStamp; var Kir: SessionKey; var Mi: Nonce; @@ -65,7 +58,7 @@ protocol neustub-GuttmanHwang(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var T: Ticket; var Tb: TimeStamp; @@ -84,9 +77,9 @@ protocol neustub-GuttmanHwang(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; read_1(I,R, I, Ni); @@ -102,7 +95,7 @@ protocol neustub-GuttmanHwang(I,R,S) role S { var Ni, Nr: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; var Tb: TimeStamp; read_!2(R,S, R, {I,Ni,Tb,Nr}k(R,S)); diff --git a/gui/Protocols/neumannstub-guttman.spdl b/gui/Protocols/neumannstub-guttman.spdl index ce0443d..06853b0 100644 --- a/gui/Protocols/neumannstub-guttman.spdl +++ b/gui/Protocols/neumannstub-guttman.spdl @@ -10,27 +10,20 @@ 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; - const Kir: SessionKey; - const Tr: TimeStamp; + fresh Kir: SessionKey; + fresh Tr: TimeStamp; send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); read_6(R,I,{Mi,Mr}Kir); @@ -43,7 +36,7 @@ protocol neustub^Repeat(I,R,S) role R { - const Mr: Nonce; + fresh Mr: Nonce; var Tr: TimeStamp; var Kir: SessionKey; var Mi: Nonce; @@ -65,7 +58,7 @@ protocol neustub(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var T: Ticket; var Tb: TimeStamp; @@ -84,9 +77,9 @@ 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; read_1(I,R, I, Ni); @@ -102,7 +95,7 @@ protocol neustub(I,R,S) role S { var Ni, Nr: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; var Tb: TimeStamp; read_!2(R,S, R, {I,Ni,Tb}k(R,S), Nr); diff --git a/gui/Protocols/neumannstub-hwang.spdl b/gui/Protocols/neumannstub-hwang.spdl index bbaff4e..67e598e 100644 --- a/gui/Protocols/neumannstub-hwang.spdl +++ b/gui/Protocols/neumannstub-hwang.spdl @@ -10,23 +10,15 @@ usertype Server, SessionKey, TimeStamp, TicketKey; usertype ExpiredTimeStamp; -secret k: Function; -const a, b, e: Agent; -const s: Server; const Fresh: Function; const Compromised: Function; -const ne: Nonce; -const kee: SessionKey; -untrusted e; -compromised k(e,s); - protocol neustub-Hwang(I,R,S) { role I { - const Ni,Mi: Nonce; + fresh Ni,Mi: Nonce; var Nr,Mr: Nonce; var T: Ticket; var Tb: TimeStamp; @@ -48,9 +40,9 @@ protocol neustub-Hwang(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; read_1(I,R, I, Ni); @@ -69,7 +61,7 @@ protocol neustub-Hwang(I,R,S) role S { var Ni, Nr: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; var Tb: TimeStamp; read_!2(R,S, R, {I,Ni,Tb,Nr}k(R,S)); diff --git a/gui/Protocols/neumannstub-keycompromise.spdl b/gui/Protocols/neumannstub-keycompromise.spdl index c4ccb60..25b15e9 100644 --- a/gui/Protocols/neumannstub-keycompromise.spdl +++ b/gui/Protocols/neumannstub-keycompromise.spdl @@ -10,27 +10,20 @@ 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; - const Kir: SessionKey; - const Tr: TimeStamp; + fresh Kir: SessionKey; + fresh Tr: TimeStamp; send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); read_6(R,I,Mr,{Mi}Kir); @@ -43,7 +36,7 @@ protocol neustub^Repeat(I,R,S) role R { - const Mr: Nonce; + fresh Mr: Nonce; var Tr: TimeStamp; var Kir: SessionKey; var Mi: Nonce; @@ -65,7 +58,7 @@ protocol neustub(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var T: Ticket; var Tb: TimeStamp; @@ -84,9 +77,9 @@ 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; read_1(I,R, I, Ni); @@ -102,7 +95,7 @@ protocol neustub(I,R,S) role S { var Ni, Nr: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; var Tb: TimeStamp; read_2(R,S, R, {I,Ni,Tb}k(R,S), Nr); diff --git a/gui/Protocols/neumannstub.spdl b/gui/Protocols/neumannstub.spdl index a4c7ea1..3327abf 100644 --- a/gui/Protocols/neumannstub.spdl +++ b/gui/Protocols/neumannstub.spdl @@ -10,25 +10,17 @@ usertype Server, SessionKey, TimeStamp, TicketKey; usertype ExpiredTimeStamp; -secret k: Function; - -const Alice, Bob, Simon, Eve: Agent; - -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; - const Kir: SessionKey; - const Tr: TimeStamp; + fresh Kir: SessionKey; + fresh Tr: TimeStamp; send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); read_6(R,I,Mr,{Mi}Kir); @@ -40,7 +32,7 @@ protocol neustub^Repeat(I,R,S) role R { - const Mr: Nonce; + fresh Mr: Nonce; var Tr: TimeStamp; var Kir: SessionKey; var Mi: Nonce; @@ -61,7 +53,7 @@ protocol neustub(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var T: Ticket; var Tb: TimeStamp; @@ -79,9 +71,9 @@ 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; read_1(I,R, I, Ni); @@ -96,7 +88,7 @@ protocol neustub(I,R,S) role S { var Ni, Nr: Nonce; - const Kir: SessionKey; + fresh Kir: SessionKey; var Tb: TimeStamp; read_!2(R,S, R, {I,Ni,Tb}k(R,S), Nr); diff --git a/gui/Protocols/otwayrees.spdl b/gui/Protocols/otwayrees.spdl index 4b112c1..64b99dc 100644 --- a/gui/Protocols/otwayrees.spdl +++ b/gui/Protocols/otwayrees.spdl @@ -5,7 +5,6 @@ # -secret const k : Function; const Fresh: Function; const Compromised: Function; @@ -15,8 +14,8 @@ protocol otwayrees(I,R,S) { role I { - const Ni : Nonce; - const M : String; + fresh Ni : Nonce; + fresh M : String; var Kir : SessionKey; send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) ); @@ -30,7 +29,7 @@ protocol otwayrees(I,R,S) role R { var M : String; - const Nr : Nonce; + fresh Nr : Nonce; var Kir : SessionKey; var T1,T2: Ticket; @@ -48,15 +47,10 @@ protocol otwayrees(I,R,S) { var Ni,Nr : Nonce; var M : String; - const Kir : SessionKey; + fresh Kir : SessionKey; read_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) ); send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) ); } } -const Alice, Bob, Eve, Simon: Agent; - -untrusted Eve; -compromised k(Eve,Simon); - diff --git a/gui/Protocols/smartright.spdl b/gui/Protocols/smartright.spdl index e91c568..da9be17 100644 --- a/gui/Protocols/smartright.spdl +++ b/gui/Protocols/smartright.spdl @@ -10,10 +10,7 @@ # Scyther finds an attack because the value of VoR in te last message can # be replaced with an arbitrary value -const hash: Function; -secret unhash: Function; -secret k: Function; -inversekeys (hash,unhash); +hashfunction hash; usertype SessionKey; usertype XorKey; const Vor: XorKey; @@ -22,9 +19,9 @@ protocol smartright(I,R) { role I { - const VoKey: SessionKey; - const VoR: XorKey; - const CW; + fresh VoKey: SessionKey; + fresh VoR: XorKey; + fresh CW; var VoRi: Nonce; send_1(I,R, {VoKey,{CW}VoR}k(I,R)); @@ -37,7 +34,7 @@ protocol smartright(I,R) var T: Ticket; var VoR: XorKey; var VoKey: SessionKey; - const VoRi: Nonce; + fresh VoRi: Nonce; read_1(I,R, {VoKey,T}k(I,R)); send_2(R,I, VoRi); @@ -47,8 +44,3 @@ protocol smartright(I,R) } } -const Alice,Bob,Eve: Agent; - -untrusted Eve; -const ne: Nonce; - diff --git a/gui/Protocols/splice-as-cj.spdl b/gui/Protocols/splice-as-cj.spdl index 00f4576..87960b3 100644 --- a/gui/Protocols/splice-as-cj.spdl +++ b/gui/Protocols/splice-as-cj.spdl @@ -12,9 +12,6 @@ usertype TimeStamp, LifeTime; -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); const inc,dec: Function; inversekeys (inc,dec); @@ -22,9 +19,9 @@ protocol spliceAS-CJ(I,R,S) { role I { - const N1,N2: Nonce; - const T: TimeStamp; - const L: LifeTime; + fresh N1,N2: Nonce; + fresh T: TimeStamp; + fresh L: LifeTime; send_1(I,S, I, R, N1 ); read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); @@ -48,13 +45,13 @@ protocol spliceAS-CJ(I,R,S) role R { - 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(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); send_4(R,S, R, I, N3 ); @@ -67,9 +64,3 @@ protocol spliceAS-CJ(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - diff --git a/gui/Protocols/splice-as-hc.spdl b/gui/Protocols/splice-as-hc.spdl index d49f7c3..858e02a 100644 --- a/gui/Protocols/splice-as-hc.spdl +++ b/gui/Protocols/splice-as-hc.spdl @@ -7,9 +7,6 @@ usertype TimeStamp, LifeTime; -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); const inc,dec: Function; inversekeys (inc,dec); @@ -17,9 +14,9 @@ protocol spliceAS-HC(I,R,S) { role I { - const N1,N2: Nonce; - const T: TimeStamp; - const L: LifeTime; + fresh N1,N2: Nonce; + fresh T: TimeStamp; + fresh L: LifeTime; send_1(I,S, I, R, N1 ); read_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); @@ -43,13 +40,13 @@ protocol spliceAS-HC(I,R,S) role R { - 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(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); send_4(R,S, R, I, N3 ); @@ -62,11 +59,3 @@ protocol spliceAS-HC(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - - - diff --git a/gui/Protocols/splice-as.spdl b/gui/Protocols/splice-as.spdl index 25df821..9890adb 100644 --- a/gui/Protocols/splice-as.spdl +++ b/gui/Protocols/splice-as.spdl @@ -12,9 +12,6 @@ usertype TimeStamp, LifeTime; -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); const inc,dec: Function; inversekeys (inc,dec); @@ -22,9 +19,9 @@ protocol spliceAS(I,R,S) { role I { - const N1,N2: Nonce; - const T: TimeStamp; - const L: LifeTime; + fresh N1,N2: Nonce; + fresh T: TimeStamp; + fresh L: LifeTime; send_1(I,S, I, R, N1 ); read_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); @@ -48,13 +45,13 @@ protocol spliceAS(I,R,S) role R { - 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(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); send_4(R,S, R, I, N3 ); @@ -67,9 +64,3 @@ protocol spliceAS(I,R,S) } } -const Alice,Bob,Simon,Eve: Agent; - -untrusted Eve; -const ne: Nonce; -compromised sk(Eve); - diff --git a/gui/Protocols/tmn.spdl b/gui/Protocols/tmn.spdl index ce6a7e3..267d30f 100644 --- a/gui/Protocols/tmn.spdl +++ b/gui/Protocols/tmn.spdl @@ -8,9 +8,6 @@ # from the description in SPORE usertype SessionKey; -const pk: Function; -secret sk: Function; -inversekeys(pk,sk); const Fresh: Function; const Compromised: Function; @@ -18,7 +15,7 @@ protocol tmn(I,R,S) { role I { - const Ki: SessionKey; + fresh Ki: SessionKey; var Kr: SessionKey; send_1(I,S, R,{Ki}pk(S) ); @@ -31,7 +28,7 @@ protocol tmn(I,R,S) role R { - const Kr: SessionKey; + fresh Kr: SessionKey; read_2(S,R, I ); send_3(R,S, I, { Kr }pk(S) ); @@ -52,12 +49,3 @@ protocol tmn(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Ke: SessionKey; - - -untrusted Eve; -compromised sk(Eve); - - - diff --git a/gui/Protocols/wmf-lowe.spdl b/gui/Protocols/wmf-lowe.spdl index 17f183f..61c5b7f 100644 --- a/gui/Protocols/wmf-lowe.spdl +++ b/gui/Protocols/wmf-lowe.spdl @@ -17,14 +17,12 @@ inversekeys (succ,pred); const Fresh: Function; const Compromised: Function; -secret k: Function; - protocol wmf-Lowe(I,R,S) { role I { - const Kir: SessionKey; - const Ti: TimeStamp; + fresh Kir: SessionKey; + fresh Ti: TimeStamp; var Kr: SessionKey; var Nr: Nonce; @@ -41,7 +39,7 @@ protocol wmf-Lowe(I,R,S) { var Ts: TimeStamp; var Kir: SessionKey; - const Nr: Nonce; + fresh Nr: Nonce; read_2(S,R, {Ts, I, Kir}k(R,S) ); send_3(R,I, {Nr}Kir); @@ -55,7 +53,7 @@ protocol wmf-Lowe(I,R,S) role S { var Kir: SessionKey; - const Ts: TimeStamp; + fresh Ts: TimeStamp; var Ti: TimeStamp; read_1(I,S, I,{Ti, R, Kir}k(I,S) ); @@ -63,13 +61,3 @@ protocol wmf-Lowe(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Ke: SessionKey; -const Te: TimeStamp; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/wmf.spdl b/gui/Protocols/wmf.spdl index aa2f10d..4c787a8 100644 --- a/gui/Protocols/wmf.spdl +++ b/gui/Protocols/wmf.spdl @@ -12,7 +12,6 @@ usertype SessionKey; usertype TimeStamp; usertype ExpiredTimeStamp; -secret k: Function; const Fresh: Function; const Compromised: Function; @@ -20,8 +19,8 @@ protocol wmf(I,R,S) { role I { - const Kir: SessionKey; - const Ti: TimeStamp; + fresh Kir: SessionKey; + fresh Ti: TimeStamp; var Kr: SessionKey; send_1(I,S, I, {I, Ti, R, Kir}k(I,S)); @@ -45,7 +44,7 @@ protocol wmf(I,R,S) role S { var Kir: SessionKey; - const Ts: TimeStamp; + fresh Ts: TimeStamp; var Ti: TimeStamp; read_1(I,S, I,{I, Ti, R, Kir}k(I,S) ); @@ -53,13 +52,3 @@ protocol wmf(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Ke: SessionKey; -const Te: TimeStamp; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/woo-lam-pi-1.spdl b/gui/Protocols/woo-lam-pi-1.spdl index 6e08913..d38c837 100644 --- a/gui/Protocols/woo-lam-pi-1.spdl +++ b/gui/Protocols/woo-lam-pi-1.spdl @@ -4,8 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/wooLamPi1.html # -secret k: Function; - protocol woolamPi-1(I,R,S) { role I @@ -20,7 +18,7 @@ protocol woolamPi-1(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var T: Ticket; read_1(I,R, I); @@ -41,13 +39,3 @@ protocol woolamPi-1(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Te: Ticket; -const Ne: Nonce; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/woo-lam-pi-2.spdl b/gui/Protocols/woo-lam-pi-2.spdl index 3a39ac0..10b61d4 100644 --- a/gui/Protocols/woo-lam-pi-2.spdl +++ b/gui/Protocols/woo-lam-pi-2.spdl @@ -4,8 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/wooLamPi2.html # -secret k: Function; - protocol woolamPi-2(I,R,S) { role I @@ -20,7 +18,7 @@ protocol woolamPi-2(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var T: Ticket; read_1(I,R, I); @@ -41,13 +39,3 @@ protocol woolamPi-2(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Te: Ticket; -const Ne: Nonce; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/woo-lam-pi-3.spdl b/gui/Protocols/woo-lam-pi-3.spdl index b59027e..65b074f 100644 --- a/gui/Protocols/woo-lam-pi-3.spdl +++ b/gui/Protocols/woo-lam-pi-3.spdl @@ -4,8 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/wooLamPi3.html # -secret k: Function; - protocol woolamPi-3(I,R,S) { role I @@ -20,7 +18,7 @@ protocol woolamPi-3(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var T: Ticket; read_1(I,R, I); @@ -41,13 +39,3 @@ protocol woolamPi-3(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Te: Ticket; -const Ne: Nonce; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/woo-lam-pi-f.spdl b/gui/Protocols/woo-lam-pi-f.spdl index b0a0287..80f3312 100644 --- a/gui/Protocols/woo-lam-pi-f.spdl +++ b/gui/Protocols/woo-lam-pi-f.spdl @@ -4,8 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/wooLamPif.html # -secret k: Function; - protocol woolamPi-f(I,R,S) { role I @@ -20,7 +18,7 @@ protocol woolamPi-f(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var T: Ticket; read_1(I,R, I); @@ -41,11 +39,3 @@ protocol woolamPi-f(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Te: Ticket; -const Ne: Nonce; - - -untrusted Eve; -compromised k(Eve,Simon); - diff --git a/gui/Protocols/woo-lam-pi.spdl b/gui/Protocols/woo-lam-pi.spdl index 05c76ce..cb0878e 100644 --- a/gui/Protocols/woo-lam-pi.spdl +++ b/gui/Protocols/woo-lam-pi.spdl @@ -8,8 +8,6 @@ # SPORE. # -secret k: Function; - protocol woolamPi(I,R,S) { role I @@ -24,7 +22,7 @@ protocol woolamPi(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var T: Ticket; read_1(I,R, I); @@ -45,13 +43,3 @@ protocol woolamPi(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Te: Ticket; -const Ne: Nonce; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/woo-lam.spdl b/gui/Protocols/woo-lam.spdl index abf2e2a..ac7f36d 100644 --- a/gui/Protocols/woo-lam.spdl +++ b/gui/Protocols/woo-lam.spdl @@ -7,7 +7,6 @@ usertype SessionKey; -secret k: Function; const Fresh: Function; const Compromised: Function; @@ -15,7 +14,7 @@ protocol woolam(I,R,S) { role I { - const N1: Nonce; + fresh N1: Nonce; var Kir: SessionKey; var N2: Nonce; @@ -33,7 +32,7 @@ protocol woolam(I,R,S) role R { - const N2: Nonce; + fresh N2: Nonce; var N1: Nonce; var Kir: SessionKey; var T1,T2: Ticket; @@ -53,7 +52,7 @@ protocol woolam(I,R,S) role S { - const Kir: SessionKey; + fresh Kir: SessionKey; var N1,N2: Nonce; read_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S)); @@ -61,14 +60,3 @@ protocol woolam(I,R,S) } } -const Alice,Bob,Eve,Simon: Agent; -const Ke: SessionKey; -const Te: Ticket; -const Ne: Nonce; - - -untrusted Eve; -compromised k(Eve,Simon); - - - diff --git a/gui/Protocols/yahalom-ban.spdl b/gui/Protocols/yahalom-ban.spdl index 63ae5b7..4d40ac7 100644 --- a/gui/Protocols/yahalom-ban.spdl +++ b/gui/Protocols/yahalom-ban.spdl @@ -4,8 +4,6 @@ # http://www.lsv.ens-cachan.fr/spore/yahalomBAN.html # -secret k : Function; - usertype SessionKey; const Fresh: Function; const Compromised: Function; @@ -14,7 +12,7 @@ protocol yahalom-BAN(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var T: Ticket; var Kir: SessionKey; @@ -30,7 +28,7 @@ protocol yahalom-BAN(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var Ni: Nonce; var T: Ticket; var Kir: SessionKey; @@ -46,7 +44,7 @@ protocol yahalom-BAN(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) ); @@ -54,5 +52,3 @@ protocol yahalom-BAN(I,R,S) } } -const Alice,Bob,Charlie,David: Agent; - diff --git a/gui/Protocols/yahalom-lowe.spdl b/gui/Protocols/yahalom-lowe.spdl index 176c00f..f04aca9 100644 --- a/gui/Protocols/yahalom-lowe.spdl +++ b/gui/Protocols/yahalom-lowe.spdl @@ -5,8 +5,6 @@ # # -secret k : Function; - usertype SessionKey; @@ -14,7 +12,7 @@ protocol yahalom-Lowe(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var Kir: SessionKey; @@ -28,7 +26,7 @@ protocol yahalom-Lowe(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var Ni: Nonce; var Kir: SessionKey; @@ -43,7 +41,7 @@ protocol yahalom-Lowe(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) ); @@ -52,5 +50,3 @@ protocol yahalom-Lowe(I,R,S) } } -const Alice,Bob,Simon : Agent; - diff --git a/gui/Protocols/yahalom-paulson.spdl b/gui/Protocols/yahalom-paulson.spdl index 1b6a10d..0c4ce68 100644 --- a/gui/Protocols/yahalom-paulson.spdl +++ b/gui/Protocols/yahalom-paulson.spdl @@ -5,7 +5,6 @@ # # -secret k : Function; const Fresh: Function; const Compromised: Function; @@ -15,7 +14,7 @@ protocol yahalom-Paulson(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var T: Ticket; var Kir: SessionKey; @@ -31,7 +30,7 @@ protocol yahalom-Paulson(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var Ni: Nonce; var T: Ticket; var Kir: SessionKey; @@ -47,7 +46,7 @@ protocol yahalom-Paulson(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) ); @@ -55,5 +54,3 @@ protocol yahalom-Paulson(I,R,S) } } -const Alice,Bob,Simon : Agent; - diff --git a/gui/Protocols/yahalom.spdl b/gui/Protocols/yahalom.spdl index 056db46..e949cc6 100644 --- a/gui/Protocols/yahalom.spdl +++ b/gui/Protocols/yahalom.spdl @@ -5,15 +5,13 @@ # # -secret k : Function; - usertype SessionKey; protocol yahalom(I,R,S) { role I { - const Ni: Nonce; + fresh Ni: Nonce; var Nr: Nonce; var T: Ticket; var Kir: SessionKey; @@ -27,7 +25,7 @@ protocol yahalom(I,R,S) role R { - const Nr: Nonce; + fresh Nr: Nonce; var Ni: Nonce; var T: Ticket; var Kir: SessionKey; @@ -41,7 +39,7 @@ protocol yahalom(I,R,S) role S { - const Kir: SessionKey; + fresh Kir: SessionKey; var Ni,Nr: Nonce; read_2(R,S, R, {I,Ni,Nr}k(R,S) ); @@ -52,10 +50,3 @@ protocol yahalom(I,R,S) } } -const Alice,Bob,Simon : Agent; - -const Eve: Agent; -untrusted Eve; - -compromised k(Eve,Simon); - diff --git a/gui/mpa.spdl b/gui/mpa.spdl index fff98b4..99d3ed6 100644 --- a/gui/mpa.spdl +++ b/gui/mpa.spdl @@ -2,19 +2,13 @@ * Needham-Schroeder-Lowe protocol */ -// PKI infrastructure - -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); - // The protocol description protocol nsl3(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {ni,I}pk(R) ); @@ -30,7 +24,7 @@ protocol nsl3(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {ni,I}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); @@ -43,30 +37,18 @@ protocol nsl3(I,R) } } -// An untrusted agent, with leaked information - -const Eve: Agent; -untrusted Eve; -compromised sk(Eve); - /* * Needham-Schroeder-Lowe protocol, * broken version (wrong role name in first message) */ -// PKI infrastructure - -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); - // The protocol description protocol nsl3-broken(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {ni,R}pk(R) ); @@ -82,7 +64,7 @@ protocol nsl3-broken(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {ni,R}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); @@ -95,9 +77,3 @@ protocol nsl3-broken(I,R) } } -// An untrusted agent, with leaked information - -const Eve: Agent; -untrusted Eve; -compromised sk(Eve); - diff --git a/gui/ns3.spdl b/gui/ns3.spdl index 2016c7a..e78c1a7 100644 --- a/gui/ns3.spdl +++ b/gui/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, {ni,I}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, {ni,I}pk(R) ); send_2(R,I, {ni,nr}pk(I) ); diff --git a/gui/nsl3-broken.spdl b/gui/nsl3-broken.spdl index 50b5fd6..b84b5c2 100644 --- a/gui/nsl3-broken.spdl +++ b/gui/nsl3-broken.spdl @@ -3,19 +3,13 @@ * broken version (wrong role name in first message) */ -// PKI infrastructure - -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); - // The protocol description protocol nsl3-broken(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {ni,R}pk(R) ); @@ -31,7 +25,7 @@ protocol nsl3-broken(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {ni,R}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); @@ -44,9 +38,3 @@ protocol nsl3-broken(I,R) } } -// An untrusted agent, with leaked information - -const Eve: Agent; -untrusted Eve; -compromised sk(Eve); - diff --git a/gui/nsl3.spdl b/gui/nsl3.spdl index e26e8a4..af99579 100644 --- a/gui/nsl3.spdl +++ b/gui/nsl3.spdl @@ -2,19 +2,13 @@ * Needham-Schroeder-Lowe protocol */ -// PKI infrastructure - -const pk: Function; -secret sk: Function; -inversekeys (pk,sk); - // The protocol description protocol nsl3(I,R) { role I { - const ni: Nonce; + fresh ni: Nonce; var nr: Nonce; send_1(I,R, {ni,I}pk(R) ); @@ -30,7 +24,7 @@ protocol nsl3(I,R) role R { var ni: Nonce; - const nr: Nonce; + fresh nr: Nonce; read_1(I,R, {ni,I}pk(R) ); send_2(R,I, {ni,nr,R}pk(I) ); @@ -43,9 +37,3 @@ protocol nsl3(I,R) } } -// An untrusted agent, with leaked information - -const Eve: Agent; -untrusted Eve; -compromised sk(Eve); -