diff --git a/gui/Protocols/MultiProtocolAttacks/BKE.spdl b/gui/Protocols/MultiProtocolAttacks/BKE.spdl new file mode 100644 index 0000000..eaa08b9 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/BKE.spdl @@ -0,0 +1,39 @@ +/* + Bilateral Key Exchange with Public Key protocol (BKEPK) +*/ + +usertype SessionKey; + +hashfunction hash; + +protocol bke(I,R) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + var kir: SessionKey; + + send_1 (I,R, { ni,I }pk(R) ); + read_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); + send_3 (I,R, { hash(nr) }kir ); + claim_4 (I, Secret, kir ); + //claim_5 (I, Niagree ); + //claim_6 (I, Nisynch ); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + fresh kir: SessionKey; + + read_1 (I,R, { ni,I }pk(R) ); + send_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); + read_3 (I,R, { hash(nr) }kir ); + claim_7 (R, Secret, kir ); + //claim_8 (R, Niagree ); + //claim_9 (R, Nisynch ); + } +} + diff --git a/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl b/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl new file mode 100644 index 0000000..e9a31b4 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/andrew-ban-concrete.spdl @@ -0,0 +1,73 @@ +# BAN concrete Andrew Secure RPC +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/andrewBAN2.html +# +# Note: +# The shared key between I and R is modelled as k(I,R) currently +# there is no way to express that this key is equal to k(R,I) +# In order to overcome this a 'dummy' role X has been hadded that recrypts +# a given term crypted with k(I,R) with k(R,I) +# +# Note: +# Read 4 by the Initatior has been placed after the synchronisation claim +# as it allows trivial synchronisation attacks otherwise (the message is +# completely fresh and can therefore always be replaced by an arbitrary value +# created by the intruder) which are not considered in SPORE +# + +usertype SessionKey; +const Fresh: Function; + +protocol @swapkey(X) +{ + # Protocol added to work around the symmetry problems where k(I,R) != k(R,I) + role X + { + var I,R: Agent; + var T:Ticket; + read_!X1(X,X,I,R,{T}k(I,R)); + send_!X2(X,X,{T}k(R,I)); + } +} + +protocol andrew-Concrete(I,R) +{ + + role I + { + fresh ni: Nonce; + var nr: Nonce; + var kir: SessionKey; + + send_1(I,R, I,ni ); + read_2(R,I, {ni,kir}k(I,R) ); + send_3(I,R, {ni}kir); + claim_I1(I,Secret,kir); + claim_I2(I,Nisynch); + claim_I3(I,Empty,(Fresh,kir)); + read_6(R,I, nr); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + fresh kir: SessionKey; + + read_1(I,R, I,ni ); + send_2(R,I, {ni,kir}k(I,R) ); + read_3(I,R, {ni}kir); + send_6(R,I, nr); + claim_R1(R,Secret,kir); + claim_R2(R,Nisynch); + claim_R3(R,Empty,(Fresh,kir)); + } +} + +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 new file mode 100644 index 0000000..3866337 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/andrew-ban.spdl @@ -0,0 +1,63 @@ +# BAN modified Andrew Secure RPC +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/andrewBAN.html +# +# Note: +# The shared key between I and R is modelled as k(I,R) currently +# there is no way to express that this key is equal to k(R,I) +# So it is possile that certain attacks that use this property are not found +# +# Note: +# According to SPORE there are no known attacks on this protocol +# +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol andrew-Ban(I,R) +{ + role I + { + fresh ni: Nonce; + var nr,nr2: Nonce; + var kir: SessionKey; + + send_1(I,R, I,{ni}k(I,R) ); + read_2(R,I, {ni,nr}k(I,R) ); + send_3(I,R, {nr}k(I,R) ); + read_4(R,I, {kir,nr2,ni}k(I,R) ); + claim_I1(I,Nisynch); + claim_I2(I,Niagree); + claim_I3(I,Secret, kir); + claim_I5(I,Empty, (Fresh,kir)); + } + + role R + { + var ni: Nonce; + 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) ); + read_3(I,R, {nr}k(I,R) ); + send_4(R,I, {kir,nr2,ni}k(I,R) ); + claim_R1(R,Nisynch); + claim_R2(R,Niagree); + claim_R3(R,Secret, kir); + claim_R5(R,Empty, (Fresh,kir)); + } +} + +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 new file mode 100644 index 0000000..1123ed8 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/andrew-lowe-ban.spdl @@ -0,0 +1,70 @@ +# Lowe modified BAN concrete Andrew Secure RPC +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/andrewLowe.html +# +# Note: +# The shared key between I and R is modelled as k(I,R) currently +# there is no way to express that this key is equal to k(R,I) +# So it is possile that certain attacks that use this property are not found +# +# Note: +# Read 4 by the Initatior has been placed after the synchronisation claim +# as it allows trivial synchronisation attacks otherwise (the message is +# completely fresh and can therefore always be replaced by an arbitrary value +# created by the intruder) which are not considered in SPORE +# +# Note: +# According to SPORE there are no known attacks on this protocol +# + +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol andrew-LoweBan(I,R) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + var kir: SessionKey; + + send_1(I,R, I,ni ); + read_2(R,I, {ni,kir,R}k(I,R) ); + send_3(I,R, {ni}kir ); + claim_I1(I,Nisynch); + claim_I2(I,Secret, kir); + claim_I3(I,Empty, (Fresh,kir)); + read_4(R,I, nr ); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + fresh kir: SessionKey; + + read_1(I,R, I,ni ); + send_2(R,I, {ni,kir,R}k(I,R) ); + read_3(I,R, {ni}kir ); + send_4(R,I, nr ); + claim_R1(R,Nisynch); + claim_R2(R,Secret, kir); + claim_R3(R,Empty, (Fresh,kir)); + } +} + +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 new file mode 100644 index 0000000..48f4c9f --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/boyd.spdl @@ -0,0 +1,70 @@ +usertype Sessionkey; +usertype Macseed; +const m: Function; +secret unm: Function; +const f: Function; + +inversekeys (m, unm); + +/* + * Boyd key agreement + * + * Boyd & Mathuria: Protocols for authentication and key establishment + * (2003) p. 101 + * + * Note that MAC_ks(x) has been interpreted as MAC(x,ks); this + * assumption causes some possible false attacks. + */ + +protocol boyd(I,R,S) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + var ks: Macseed; + + send_1 (I,S, I,R, ni ); + read_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr ); + send_4 (I,R, m(nr, m(ks,ni,nr)) ); + + claim_6 (I, Secret, m(ks,ni,nr) ); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + var ks: Macseed; + + read_2 (S,R, { I,R, ks }k(I,S), { I,R, ks }k(R,S), ni ); + send_3 (R,I, { I,R, ks }k(I,S), m(ni, m(ks,ni,nr)), nr ); + read_4 (I,R, m(nr, m(ks,ni,nr)) ); + + claim_10 (R, Secret, m(ks,ni,nr)); + } + + role S + { + var ni,nr: Nonce; + 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 ); + } +} + +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 new file mode 100644 index 0000000..6834104 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/ccitt509-ban3.spdl @@ -0,0 +1,45 @@ +# BAN modified version of CCITT X.509 (3) +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/ccittx509_3BAN.html +# +# Note: +# The protocol description also states that Xa and Ya should be fresh +# this can not be verified using scyther +# +# Note: +# According to SPORE there are no known attacks on this protocol +# + +protocol ccitt509-ban3(I,R) +{ + role I + { + fresh Na,Xa,Ya: Nonce; + var Xb,Nb,Yb: Nonce; + + send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I)); + read_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R)); + send_3(I,R, I,{R, Nb}sk(I)); + claim_4(I,Nisynch); + } + + role R + { + var Na,Xa,Ya: Nonce; + fresh Xb,Yb,Nb: Nonce; + + read_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)); + read_3(I,R, I,{R, Nb}sk(I)); + claim_5(R,Nisynch); + # There should also be Fresh Xa and Fresh Ya claims here + } +} + +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 new file mode 100644 index 0000000..b406a62 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/denning-sacco-lowe.spdl @@ -0,0 +1,74 @@ +# Lowe modified Denning-Sacco shared key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/denningSaccoLowe.html +# +# Note: +# According to SPORE there are no attacks on this protocol, scyther +# finds one however. This has to be investigated further. + +usertype Key; +usertype SessionKey; +usertype TimeStamp; +usertype ExpiredTimeStamp; +usertype PseudoFunction; +const dec: PseudoFunction; +const Fresh: Function; +const Compromised: Function; + +protocol denningSacco-Lowe(I,R,S) +{ + role I + { + var W: Ticket; + var Kir: SessionKey; + var T: TimeStamp; + var Nr: Nonce; + + send_1(I,S, I,R ); + read_2(S,I, {R, Kir, T, W}k(I,S) ); + send_3(I,R, W); + read_4(R,I, {Nr}Kir); + send_5(I,R, {{Nr}dec}Kir); + claim_I1(I,Niagree); + claim_I2(I,Nisynch); + claim_I3(I,Secret,Kir); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + var Kir: SessionKey; + var T: TimeStamp; + fresh Nr: Nonce; + + read_3(I,R, {Kir,I,T}k(R,S)); + send_4(R,I, {Nr}Kir); + read_5(I,R, {{Nr}dec}Kir); + claim_R1(R,Niagree); + claim_R2(R,Nisynch); + claim_R3(R,Secret,Kir); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + var W: Ticket; + 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)); + claim_x(S, Secret, Kir); + } +} + +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 new file mode 100644 index 0000000..5a2f224 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/denning-sacco.spdl @@ -0,0 +1,62 @@ +# Denning-Sacco shared key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/denningSacco.html +# + +usertype Key; +usertype SessionKey; +usertype TimeStamp; +usertype ExpiredTimeStamp; +const Fresh: Function; +const Compromised: Function; + +protocol denningSacco(I,R,S) +{ + role I + { + var W: Ticket; + var Kir: SessionKey; + var T: TimeStamp; + + send_1(I,S, I,R ); + read_2(S,I, {R, Kir, T, W}k(I,S) ); + send_3(I,R, W); + claim_I1(I,Niagree); + claim_I2(I,Nisynch); + claim_I3(I,Secret,Kir); + claim_I4(I,Empty, (Fresh,Kir)); + } + + role R + { + var Kir: SessionKey; + var T: TimeStamp; + + read_3(I,R, {Kir,I,T}k(R,S)); + claim_R1(R,Niagree); + claim_R2(R,Nisynch); + claim_R3(R,Secret,Kir); + claim_R4(R,Empty, (Fresh,Kir)); + } + + role S + { + var W: Ticket; + 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/MultiProtocolAttacks/gong-nonce-b.spdl b/gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl new file mode 100644 index 0000000..57e9b60 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/gong-nonce-b.spdl @@ -0,0 +1,80 @@ +usertype Sessionkey; +usertype Keypart; +hashfunction f; + +/* + * Gong nonce based alternative + * + * Boyd & Mathuria: Protocols for authentication and key establishment + * (2003) p. 101 + */ + +protocol gongnonceb(I,R,S) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + fresh ki: Keypart; + var kr: Keypart; + + send_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni ); + read_4 (S,I, { S,I,R,kr,I }k(I,S), { R,I,ni }f(ki,kr), nr ); + send_5 (I,R, { I,R,nr }f(ki,kr) ); + + claim_6 (I, Secret, ki); + claim_7 (I, Secret, kr); + claim_8 (I, Nisynch); + claim_9 (I, Niagree); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + fresh kr: Keypart; + var ki: Keypart; + + read_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni ); + send_3 (R,S, { R,S,R,kr,I }k(R,S), { R,I, ni }f(ki,kr), nr ); + read_5 (I,R, { I,R,nr }f(ki,kr) ); + + claim_10 (R, Secret, ki); + claim_11 (R, Secret, kr); + claim_12 (R, Nisynch); + claim_13 (R, Niagree); + } + + role S + { + var ni,nr: Nonce; + var ki,kr: Keypart; + var T; + + read_1 (I,S, I,R, { I,S,I, ki, R }k(I,S), ni ); + send_2 (S,R, I,R, { S,R,I, ki, R }k(R,S), ni ); + read_3 (R,S, { R,S,R,kr,I }k(R,S), T, nr ); + send_4 (S,I, { S,I,R,kr,I }k(I,S), T, nr ); + } +} + +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/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl b/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl new file mode 100644 index 0000000..48d053d --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/gong-nonce.spdl @@ -0,0 +1,71 @@ +usertype Sessionkey; +usertype Keypart; + +protocol gongnonce(I,R,S) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + fresh ki: Keypart; + var kr: Keypart; + + send_1 (I,R, I,R,ni ); + read_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr); + send_4 (I,S, { I,S,I, ki, R, nr }k(I,S) ); + + claim_6 (I, Secret, ki); + claim_7 (I, Secret, kr); + claim_8 (I, Nisynch); + claim_9 (I, Niagree); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + fresh kr: Keypart; + var ki: Keypart; + + read_1 (I,R, I,R,ni ); + send_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S)); + read_5 (S,R, { S,R,I, ki, R, nr }k(R,S) ); + + claim_10 (R, Secret, ki); + claim_11 (R, Secret, kr); + claim_12 (R, Nisynch); + claim_13 (R, Niagree); + } + + role S + { + var ni,nr: Nonce; + var ki,kr: Keypart; + + read_2 (R,S, I,R, nr, { R,S,R, kr, I,ni }k(R,S)); + send_3 (S,I, { S,I,R, kr, I, ni }k(I,S), nr); + read_4 (I,S, { I,S,I, ki, R, nr }k(I,S) ); + send_5 (S,R, { S,R,I, ki, R, nr }k(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/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl b/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl new file mode 100644 index 0000000..6715f83 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/isoiec11770-2-13.spdl @@ -0,0 +1,62 @@ +usertype Sessionkey; +usertype Ticket; + +protocol isoiec11770213(I,R,S) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + var kir: Sessionkey; + + send_1 (I,R, ni); + read_4 (R,I, { ni,kir,R }k(I,S) ); + + claim_5 (I, Secret, kir); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + fresh kir: Sessionkey; + var T; + + read_1 (I,R, ni); + send_2 (R,S, { nr,ni,I,kir }k(R,S) ); + read_3 (S,R, { nr, I }k(R,S), T ); + send_4 (R,I, T ); + + claim_6 (R, Secret, kir); + } + + role S + { + var ni,nr: Nonce; + var kir: Sessionkey; + + read_2 (R,S, { nr,ni,I,kir }k(R,S) ); + send_3 (S,R, { nr, I }k(R,S), { ni,kir,R }k(I,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/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl b/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl new file mode 100644 index 0000000..a3f937b --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/kaochow-v2.spdl @@ -0,0 +1,69 @@ +# Kao Chow Authentication v.2 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/kaoChow2.html +# + +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol kaochow-2(I,R,S) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + var kir,kt: SessionKey; + + send_1 (I,S, I,R,ni); + read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr ); + send_4 (I,R, {nr,kir}kt ); + + claim_I1 (I, Nisynch); + claim_I2 (I, Niagree); + claim_I3 (I, Secret, kir); + claim_I4 (I, Empty, (Fresh,kir)); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + var kir,kt: SessionKey; + var T: Ticket; + + read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S) ); + send_3 (R,I, R, T, {ni, kir}kt, nr ); + read_4 (I,R, {nr,kir}kt ); + + claim_R1 (R, Nisynch); + claim_R2 (R, Niagree); + claim_R3 (R, Secret, kir); + claim_R4 (R, Empty, (Fresh,kir)); + } + + role S + { + var ni: Nonce; + 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/MultiProtocolAttacks/kaochow-v3.spdl b/gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl new file mode 100644 index 0000000..eeb43ed --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/kaochow-v3.spdl @@ -0,0 +1,73 @@ +# Kao Chow Authentication v.3 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/kaoChow3.html +# + +usertype SessionKey; +usertype ExpiredTimeStamp; +usertype TimeStamp; +const Fresh: Function; +const Compromised: Function; + +protocol kaochow-3(I,R,S) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + var kir,kt: SessionKey; + var T2: Ticket; + + send_1 (I,S, I,R,ni); + read_3 (R,I, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 ); + send_4 (I,R, {nr,kir}kt, T2 ); + + claim_I1 (I, Nisynch); + claim_I2 (I, Niagree); + claim_I3 (I, Secret, kir); + claim_I4 (I, Empty, (Fresh,kir)); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + var kir,kt: SessionKey; + var T: Ticket; + 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) ); + read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) ); + + claim_R1 (R, Nisynch); + claim_R2 (R, Niagree); + claim_R3 (R, Secret, kir); + claim_R4 (R, Empty, (Fresh,kir)); + } + + role S + { + var ni: Nonce; + 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/MultiProtocolAttacks/kaochow.spdl b/gui/Protocols/MultiProtocolAttacks/kaochow.spdl new file mode 100644 index 0000000..7724a72 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/kaochow.spdl @@ -0,0 +1,69 @@ +# Kao Chow Authentication v.1 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/kaoChow1.html +# + +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol kaochow(I,R,S) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + var kir: SessionKey; + + send_1 (I,S, I,R,ni); + read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr ); + send_4 (I,R, {nr}kir ); + + claim_I1 (I, Nisynch); + claim_I2 (I, Niagree); + claim_I3 (I, Secret, kir); + claim_I4 (I, Empty, (Fresh,kir)); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + var kir: SessionKey; + var T; + + read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); + send_3 (R,I, T, {ni}kir, nr ); + read_4 (I,R, {nr}kir ); + + claim_R1 (R, Nisynch); + claim_R2 (R, Niagree); + claim_R3 (R, Secret, kir); + claim_R4 (R, Empty, (Fresh,kir)); + } + + role S + { + var ni: Nonce; + 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/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl new file mode 100644 index 0000000..4488fb6 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk-amend.spdl @@ -0,0 +1,73 @@ +# Amended Needham Schroeder Symmetric Key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/nssk_amended.html +# +# +# Note: +# According to SPORE there are no attacks on this protocol, scyther +# finds one however. This has to be investigated further. + + + +# Model dec that is invertible by inc +const dec,inc: Function; +inversekeys(dec,inc); +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol needhamschroedersk-amend(I,R,S) +{ + role I + { + fresh Ni: Nonce; + var Nr: Nonce; + var Kir: SessionKey; + var T,T2: Ticket; + + send_1(I,R,I); + read_2(R,I,T); + send_3(I,S,(I,R,Ni,T)); + read_4(S,I, {Ni,R,Kir,T2}k(I,S)); + send_5(I,R,T2); + read_6(R,I,{Nr}Kir); + send_7(I,R,{{Nr}dec}Kir); + + claim_I2(I,Secret,Kir); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + fresh Nr: Nonce; + var Kir: SessionKey; + + read_1(I,R,I); + send_2(R,I,{I,Nr}k(R,S)); + read_5(I,R,{Kir,Nr,I}k(R,S)); + send_6(R,I,{Nr}Kir); + read_7(I,R,{{Nr}dec}Kir); + claim_R1(R,Secret,Nr); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + var Ni,Nr: Nonce; + 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/MultiProtocolAttacks/needham-schroeder-sk.spdl b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl new file mode 100644 index 0000000..964ae05 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/needham-schroeder-sk.spdl @@ -0,0 +1,62 @@ +# Needham Schroeder Symmetric Key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/nssk.html +# +# + + +# Model dec that is invertible by inc +const dec,inc: Function; +inversekeys(dec,inc); +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol needhamschroedersk(I,R,S) +{ + role I + { + fresh Ni: Nonce; + var Nr: Nonce; + var Kir: SessionKey; + var T: Ticket; + + send_1(I,S,(I,R,Ni)); + read_2(S,I, {Ni,R,Kir,T}k(I,S)); + send_3(I,R,T); + read_4(R,I,{Nr}Kir); + send_5(I,R,{{Nr}dec}Kir); + claim_I2(I,Secret,Kir); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + fresh Nr: Nonce; + var Kir: SessionKey; + + read_3(I,R,{Kir,I}k(R,S)); + send_4(R,I,{Nr}Kir); + read_5(I,R,{{Nr}dec}Kir); + claim_R1(R,Secret,Kir); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + var Ni: Nonce; + 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/MultiProtocolAttacks/new.txt b/gui/Protocols/MultiProtocolAttacks/new.txt new file mode 100644 index 0000000..dbba198 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/new.txt @@ -0,0 +1,5 @@ +denning-sacco-lowe.spdl +wmf.spdl +wmf-lowe.spdl +andrew-ban-concrete.spdl +yahalom-ban-paulson.spdl diff --git a/gui/Protocols/MultiProtocolAttacks/ns3.spdl b/gui/Protocols/MultiProtocolAttacks/ns3.spdl new file mode 100644 index 0000000..b860cbf --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/ns3.spdl @@ -0,0 +1,41 @@ +/* + * Needham-Schroeder protocol + */ + +// The protocol description + +protocol ns3(I,R) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + + send_1(I,R, {ni,I}pk(R) ); + read_2(R,I, {ni,nr}pk(I) ); + send_3(I,R, {nr}pk(R) ); + + claim_i1(I,Secret,ni); + claim_i2(I,Secret,nr); + //claim_i3(I,Alive); + claim_i4(I,Niagree); + claim_i5(I,Nisynch); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + + read_1(I,R, {ni,I}pk(R) ); + send_2(R,I, {ni,nr}pk(I) ); + read_3(I,R, {nr}pk(R) ); + + claim_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + //claim_r3(R,Alive); + claim_r4(R,Niagree); + claim_r5(R,Nisynch); + } +} + diff --git a/gui/Protocols/MultiProtocolAttacks/nsl3.spdl b/gui/Protocols/MultiProtocolAttacks/nsl3.spdl new file mode 100644 index 0000000..af99579 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/nsl3.spdl @@ -0,0 +1,39 @@ +/* + * Needham-Schroeder-Lowe protocol + */ + +// The protocol description + +protocol nsl3(I,R) +{ + role I + { + fresh ni: Nonce; + var nr: Nonce; + + send_1(I,R, {ni,I}pk(R) ); + read_2(R,I, {ni,nr,R}pk(I) ); + send_3(I,R, {nr}pk(R) ); + + claim_i1(I,Secret,ni); + claim_i2(I,Secret,nr); + claim_i3(I,Niagree); + claim_i4(I,Nisynch); + } + + role R + { + var ni: Nonce; + fresh nr: Nonce; + + read_1(I,R, {ni,I}pk(R) ); + send_2(R,I, {ni,nr,R}pk(I) ); + read_3(I,R, {nr}pk(R) ); + + claim_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + claim_r3(R,Niagree); + claim_r4(R,Nisynch); + } +} + diff --git a/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl b/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl new file mode 100644 index 0000000..7fee42e --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/otwayrees.spdl @@ -0,0 +1,61 @@ +# Otway Rees +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/otwayRees.html +# + + +const Fresh: Function; +const Compromised: Function; + +usertype String,SessionKey; + +protocol otwayrees(I,R,S) +{ + role I + { + fresh Ni : Nonce; + fresh M : String; + var Kir : SessionKey; + + send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) ); + read_4(R,I, M,{Ni,Kir}k(I,S) ); + + claim_I1(I, Secret,Kir); + claim_I2(I, Nisynch); + claim_I3(I, Empty, (Fresh,Kir)); + } + + role R + { + var M : String; + fresh Nr : Nonce; + var Kir : SessionKey; + var T1,T2: Ticket; + + read_1(I,R, M,I,R, T1 ); + send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) ); + read_3(S,R, M, T2, { Nr,Kir }k(R,S) ); + send_4(R,I, M, T2 ); + + claim_R1(R, Secret,Kir); + claim_R2(R, Nisynch); + claim_R3(R, Empty, (Fresh,Kir)); + } + + role S + { + var Ni,Nr : Nonce; + var M : String; + 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/MultiProtocolAttacks/soph.spdl b/gui/Protocols/MultiProtocolAttacks/soph.spdl new file mode 100644 index 0000000..523f62c --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/soph.spdl @@ -0,0 +1,31 @@ + +protocol soph(I,R) +{ + role I + { + fresh ni: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, ni ); + claim_3(I,Niagree); + } + + role R + { + var ni: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, ni ); + } +} + +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/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl b/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl new file mode 100644 index 0000000..351faab --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/splice-as-cj.spdl @@ -0,0 +1,72 @@ +# Clark and Jacob modified Hwang and Chen modified SPLICE/AS +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/spliceas3.html +# +# Note: +# The assumptions made here do not comply with those in SPORE +# SPORE assumes that the agents do not know the pk function, but only +# their own public key values. +# This can currently not be modelled. + + +usertype TimeStamp, LifeTime; + +const inc,dec: Function; +inversekeys (inc,dec); + +protocol spliceAS-CJ(I,R,S) +{ + role I + { + 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) ); + send_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) ); + read_6(R,I, R, I, {{N2}inc}pk(I) ); + + claim_7(I, Secret, N2); + claim_9(I, Niagree); + claim_10(I, Nisynch); + } + + role S + { + var N1,N3: Nonce; + + read_1(I,S, I, R, N1 ); + send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); + read_4(R,S, R, I, N3 ); + send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); + } + + role R + { + fresh N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; + + var ni: 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 ); + read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); + send_6(R,I, R, I, {{N2}inc}pk(I) ); + + claim_8(R, Secret, N2); + claim_11(R, Niagree); + claim_12(R, Nisynch); + } +} + +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 new file mode 100644 index 0000000..cf5feb9 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/splice-as-hc.spdl @@ -0,0 +1,72 @@ +# Hwang and Chen Modified SPLICE/AS +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/spliceas2.html +# + + +usertype TimeStamp, LifeTime; + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); +const inc,dec: Function; +inversekeys (inc,dec); + +protocol spliceAS-HC(I,R,S) +{ + role I + { + 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) ); + send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); + read_6(R,I, R, I, {R, {N2}inc}pk(I) ); + + claim_7(I, Secret, N2); + claim_9(I, Niagree); + claim_10(I, Nisynch); + } + + role S + { + var N1,N3: Nonce; + + read_1(I,S, I, R, N1 ); + send_2(S,I, S, {S, I, N1, R, pk(R)}sk(S) ); + read_4(R,S, R, I, N3 ); + send_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); + } + + role R + { + fresh N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; + + var ni: 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 ); + read_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) ); + send_6(R,I, R, I, {R, {N2}inc}pk(I) ); + + claim_8(R, Secret, N2); + claim_11(R, Niagree); + claim_12(R, Nisynch); + } +} + +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 new file mode 100644 index 0000000..01f8552 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/splice-as.spdl @@ -0,0 +1,72 @@ +# SPLICE/AS +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/spliceas.html +# +# Note: +# The assumptions made here do not comply with those in SPORE +# SPORE assumes that the agents do not know the pk function, but only +# their own public key values. +# This can currently not be modelled. + + +usertype TimeStamp, LifeTime; + +const inc,dec: Function; +inversekeys (inc,dec); + +protocol spliceAS(I,R,S) +{ + role I + { + 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) ); + send_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) ); + read_6(R,I, R, I, {R, {N2}inc}pk(I) ); + + claim_7(I, Secret, N2); + claim_9(I, Niagree); + claim_10(I, Nisynch); + } + + role S + { + var N1,N3: Nonce; + + read_1(I,S, I, R, N1 ); + send_2(S,I, S, {S, I, N1, pk(R)}sk(S) ); + read_4(R,S, R, I, N3 ); + send_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); + } + + role R + { + fresh N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; + + var ni: 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 ); + read_5(S,R, S, {S, R, N3, pk(I)}sk(S) ); + send_6(R,I, R, I, {R, {N2}inc}pk(I) ); + + claim_8(R, Secret, N2); + claim_11(R, Niagree); + claim_12(R, Nisynch); + } +} + +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 new file mode 100644 index 0000000..d80fe8a --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/tmn.spdl @@ -0,0 +1,60 @@ +# TMN +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/tmn.html +# +# Note: +# According to Boyd and Mathuria Kb is the session key this is not clear +# from the description in SPORE +usertype SessionKey; + +const Fresh: Function; +const Compromised: Function; + +protocol tmn(I,R,S) +{ + role I + { + fresh Ki: SessionKey; + var Kr: SessionKey; + + send_1(I,S, R,{Ki}pk(S) ); + read_4(S,I, R,{Kr}Ki ); + + claim_I1(I,Secret,Kr); + claim_I2(I,Nisynch); + claim_I3(I,Empty,(Fresh,Kr)); + } + + role R + { + fresh Kr: SessionKey; + + read_2(S,R, I ); + send_3(R,S, I, { Kr }pk(S) ); + + claim_R1(R,Secret,Kr); + claim_R2(R,Nisynch); + claim_R3(R,Empty,(Fresh,Kr)); + } + + role S + { + var Ki,Kr: SessionKey; + + read_1(I,S, R,{Ki}pk(S) ); + send_2(S,R, I ); + read_3(R,S, I, { Kr }pk(S) ); + send_4(S,I, R,{Kr}Ki ); + } +} + +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 new file mode 100644 index 0000000..e552f51 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/wmf-brutus.spdl @@ -0,0 +1,47 @@ +usertype SesKey, Server; + +/* Version from the Brutus reports +*/ + +protocol wmfbrutus(A,B,S) +{ + role A + { + fresh kab : SesKey; + + send_1(A,S, A, { B,kab }k(A,S) ); + } + + role B + { + var kab : SesKey; + + read_2(S,B, { A, kab }k(B,S) ); + + claim_3(B, Secret,kab); + } + + role S + { + var kab : SesKey; + + read_1(A,S, A, { B,kab }k(A,S) ); + send_2(S,B, { A, kab }k(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/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl b/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl new file mode 100644 index 0000000..7fbce47 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/wmf-lowe.spdl @@ -0,0 +1,73 @@ +# Lowe modified Wide Mouthed Frog +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wideMouthedFrogLowe.html +# +# Note: +# According to SPORE there are no known attacks on this protocol, scyther +# finds one however this has to do with the unusual assumption that every +# agent can recognise and will reject to read messages that it has created +# itself. + +usertype SessionKey; +usertype TimeStamp; +usertype ExpiredTimeStamp; +const succ,pred: Function; +inversekeys (succ,pred); +const Fresh: Function; +const Compromised: Function; + +protocol wmf-Lowe(I,R,S) +{ + role I + { + fresh Kir: SessionKey; + fresh Ti: TimeStamp; + var Kr: SessionKey; + var Nr: Nonce; + + send_1(I,S, I, {Ti, R, Kir}k(I,S)); + read_3(R,I,{Nr}Kir); + send_4(I,R,{{Nr}succ}Kir); + + claim_I1(I,Secret,Kir); + claim_I2(I,Nisynch); + claim_I3(I,Empty,(Fresh,Kir)); + } + + role R + { + var Ts: TimeStamp; + var Kir: SessionKey; + fresh Nr: Nonce; + + read_2(S,R, {Ts, I, Kir}k(R,S) ); + send_3(R,I, {Nr}Kir); + read_4(I,R, {{Nr}succ}Kir); + + claim_R1(R,Secret,Kir); + claim_R2(R,Nisynch); + claim_R3(R,Empty,(Fresh,Kir)); + } + + role S + { + var Kir: SessionKey; + fresh Ts: TimeStamp; + var Ti: TimeStamp; + + read_1(I,S, I,{Ti, R, Kir}k(I,S) ); + send_2(S,R, {Ts, I, Kir}k(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 new file mode 100644 index 0000000..f893d76 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/wmf.spdl @@ -0,0 +1,64 @@ +# Wide Mouthed Frog +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wideMouthedFrog.html +# +# Note +# The name of the party that has generated a message was added in order +# to model the property described in SPORE that an agent can identify +# its own messages and will reject them. + +usertype SessionKey; +usertype TimeStamp; +usertype ExpiredTimeStamp; + +const Fresh: Function; +const Compromised: Function; + +protocol wmf(I,R,S) +{ + role I + { + fresh Kir: SessionKey; + fresh Ti: TimeStamp; + var Kr: SessionKey; + + send_1(I,S, I, {I, Ti, R, Kir}k(I,S)); + + claim_I1(I,Secret,Kir); + claim_I2(I,Empty,(Fresh,Kir)); + } + + role R + { + var Ts: TimeStamp; + var Kir: SessionKey; + + read_2(S,R, {S, Ts, I, Kir}k(R,S) ); + + claim_R1(R,Secret,Kir); + claim_R2(R,Nisynch); + claim_R3(R,Empty,(Fresh,Kir)); + } + + role S + { + var Kir: SessionKey; + fresh Ts: TimeStamp; + var Ti: TimeStamp; + + read_1(I,S, I,{I, Ti, R, Kir}k(I,S) ); + send_2(S,R, {S, Ts, I, Kir}k(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-f.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl new file mode 100644 index 0000000..1d2cd7e --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam-pi-f.spdl @@ -0,0 +1,49 @@ +# Woo and Lam Pi f +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamPif.html +# + +protocol woolamPi-f(I,R,S) +{ + role I + { + var Nr: Nonce; + + send_1(I,R, I); + read_2(R,I, Nr); + send_3(I,R, {I,R,Nr}k(I,S)); + + } + + role R + { + fresh Nr: Nonce; + var T: Ticket; + + read_1(I,R, I); + send_2(R,I, Nr); + read_3(I,R, T); + send_4(R,S, {I, R, Nr, T}k(R,S)); + read_5(S,R, {I, R, Nr}k(R,S)); + + claim_R1(R,Nisynch); + } + + role S + { + var Nr: Nonce; + + read_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S)); + send_5(S,R, {I, R, Nr}k(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.spdl b/gui/Protocols/MultiProtocolAttacks/woo-lam.spdl new file mode 100644 index 0000000..f29e27c --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/woo-lam.spdl @@ -0,0 +1,64 @@ +# Woo and Lam Mutual Authentication +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamMutual.html +# + + +usertype SessionKey; + +const Fresh: Function; +const Compromised: Function; + +protocol woolam(I,R,S) +{ + role I + { + fresh N1: Nonce; + var Kir: SessionKey; + var N2: Nonce; + + send_1(I,R, I, N1); + read_2(R,I, R, N2); + send_3(I,R, {I, R, N1, N2}k(I,S)); + read_6(R,I, {R, N1, N2, Kir}k(I,S), {N1,N2}Kir); + send_7(I,R, {N2}Kir); + + + claim_I1(I,Secret,Kir); + claim_I2(I,Nisynch); + claim_I3(I,Empty,(Fresh,Kir)); + } + + role R + { + fresh N2: Nonce; + var N1: Nonce; + var Kir: SessionKey; + var T1,T2: Ticket; + + read_1(I,R, I, N1); + send_2(R,I, R, N2); + read_3(I,R, T1); + send_4(R,S, T1, {I, R, N1, N2}k(R,S)); + read_5(S,R, T2, {I, N1, N2, Kir}k(R,S)); + send_6(R,I, T2, {N1,N2}Kir); + read_7(I,R, {N2}Kir); + + claim_R1(R,Secret,Kir); + claim_R2(R,Nisynch); + claim_R3(R,Empty,(Fresh,Kir)); + } + + role S + { + 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)); + send_5(S,R, {R, N1, N2, Kir}k(I,S), {I, N1, N2, Kir}k(R,S)); + } +} + + + diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl new file mode 100644 index 0000000..8cf2bb9 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson-modified.spdl @@ -0,0 +1,52 @@ +// BAN modified version of the yahalom protocol +// +// Modeled as version in Paulson's paper: +// "Relations Between Secrets: Two Formal Analyses of the Yahalom +// Protocol" +// +// Modified (improved) version from page 16. + +usertype Server; +usertype SessionKey; + +const a,b,c : Agent; +const s : Server; + +protocol yahalom-BAN-Paulson-modified(A,B,S) +{ + role A + { + fresh na: Nonce; + var nb: Nonce; + var ticket: Ticket; + var kab: SessionKey; + + send_1(A,B, A,na); + read_3(S,A, nb, {B,kab,na}k(A,S), ticket ); + send_4(A,B, ticket, {nb}kab ); + claim_5(A, Secret,kab); + } + + role B + { + fresh nb: Nonce; + var na: Nonce; + var ticket: Ticket; + var kab: SessionKey; + + read_1(A,B, A,na); + send_2(B,S, B, nb, {A,na}k(B,S) ); + read_4(A,B, {A,B,kab,nb}k(B,S) , {nb}kab ); + claim_6(B, Secret,kab); + } + + role S + { + fresh kab: SessionKey; + var na,nb: Nonce; + + read_2(B,S, B, nb, {A,na}k(B,S) ); + send_3(S,A, nb, {B,kab,na}k(A,S), {A,B,kab,nb}k(B,S) ); + } +} + diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl new file mode 100644 index 0000000..16e29ca --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-ban-paulson.spdl @@ -0,0 +1,50 @@ +// BAN modified version of the yahalom protocol +// +// Modeled as version in Paulson's paper: +// "Relations Between Secrets: Two Formal Analyses of the Yahalom +// Protocol" + +usertype Server; +usertype SessionKey; + +const a,b,c : Agent; +const s : Server; + +protocol yahalom-BAN-Paulson(A,B,S) +{ + role A + { + fresh na: Nonce; + var nb: Nonce; + var ticket: Ticket; + var kab: SessionKey; + + send_1(A,B, A,na); + read_3(S,A, {B,kab,na,nb}k(A,S), ticket ); + send_4(A,B, ticket, {nb}kab ); + claim_5(A, Secret,kab); + } + + role B + { + fresh nb: Nonce; + var na: Nonce; + var ticket: Ticket; + var kab: SessionKey; + + read_1(A,B, A,na); + send_2(B,S, B, {A,na,nb}k(B,S) ); + read_4(A,B, {A,kab}k(B,S) , {nb}kab ); + claim_6(B, Secret,kab); + } + + role S + { + fresh kab: SessionKey; + var na,nb: Nonce; + + read_2(B,S, B, {A,na,nb}k(B,S) ); + send_3(S,A, {B,kab,na,nb}k(A,S), {A,kab}k(B,S) ); + } +} + diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl new file mode 100644 index 0000000..d4d6cba --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-ban.spdl @@ -0,0 +1,56 @@ +# BAN simplified version of Yahalom +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/yahalomBAN.html +# + +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol yahalom-BAN(I,R,S) +{ + role I + { + fresh Ni: Nonce; + var Nr: Nonce; + var T: Ticket; + var Kir: SessionKey; + + send_1(I,R, I,Ni); + read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T ); + send_4(I,R, T, {Nr}Kir ); + + claim_I1(I, Secret,Kir); + claim_I2(I, Nisynch); + claim_I3(I, Empty, (Fresh,Kir)); + } + + role R + { + fresh Nr: Nonce; + var Ni: Nonce; + var T: Ticket; + var Kir: SessionKey; + + read_1(I,R, I,Ni); + send_2(R,S, R, Nr, {I,Ni}k(R,S) ); + read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir ); + + claim_R1(R, Secret,Kir); + claim_R2(R, Nisynch); + claim_R3(R, Empty, (Fresh,Kir)); + } + + role S + { + fresh Kir: SessionKey; + var Ni,Nr: Nonce; + + read_2(R,S, R, Nr, {I,Ni}k(R,S) ); + send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,Kir,Nr}k(R,S) ); + } +} + +const Alice,Bob,Charlie,David: Agent; + diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl new file mode 100644 index 0000000..3656625 --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/yahalom-lowe.spdl @@ -0,0 +1,54 @@ +# Lowe's modified version of Yahalom +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/yahalomLowe.html +# +# + +usertype SessionKey; + + +protocol yahalom-Lowe(I,R,S) +{ + role I + { + fresh Ni: Nonce; + var Nr: Nonce; + var Kir: SessionKey; + + send_1(I,R, I,Ni); + read_3(S,I, {R,Kir,Ni,Nr}k(I,S) ); + send_5(I,R, {I, R, S, Nr}Kir ); + + claim_I1(I, Secret,Kir); + claim_I2(I, Nisynch); + } + + role R + { + fresh Nr: Nonce; + var Ni: Nonce; + var Kir: SessionKey; + + read_1(I,R, I,Ni); + send_2(R,S, {I,Ni,Nr}k(R,S) ); + read_4(S,R, {I,Kir}k(R,S)); + read_5(I,R, {I, R, S, Nr}Kir); + + claim_R1(R, Secret,Kir); + claim_R2(R, Nisynch); + } + + role S + { + fresh Kir: SessionKey; + var Ni,Nr: Nonce; + + read_2(R,S, {I,Ni,Nr}k(R,S) ); + send_3(S,I, {R,Kir,Ni,Nr}k(I,S)); + send_4(S,R, {I,Kir}k(R,S)); + } +} + +const Alice,Bob,Simon : Agent; + diff --git a/gui/Protocols/MultiProtocolAttacks/yahalom.spdl b/gui/Protocols/MultiProtocolAttacks/yahalom.spdl new file mode 100644 index 0000000..c99d8dc --- /dev/null +++ b/gui/Protocols/MultiProtocolAttacks/yahalom.spdl @@ -0,0 +1,59 @@ +# Yahalom +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/yahalom.html +# +# + +usertype SessionKey; + +protocol yahalom(I,R,S) +{ + role I + { + fresh Ni: Nonce; + var Nr: Nonce; + var T: Ticket; + var Kir: SessionKey; + + send_1(I,R, I,Ni); + read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T ); + send_4(I,R, T, {Nr}Kir ); + + claim_I1(I, Secret,Kir); + } + + role R + { + fresh Nr: Nonce; + var Ni: Nonce; + var T: Ticket; + var Kir: SessionKey; + + read_1(I,R, I,Ni); + send_2(R,S, R, {I,Ni,Nr}k(R,S) ); + read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir ); + + claim_R1(R, Secret,Kir); + } + + role S + { + fresh Kir: SessionKey; + var Ni,Nr: Nonce; + + read_2(R,S, R, {I,Ni,Nr}k(R,S) ); + send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) ); + + claim(S, Secret, Ni); + claim(S, Secret, Nr); + } +} + +const Alice,Bob,Simon : Agent; + +const Eve: Agent; +untrusted Eve; + +compromised k(Eve,Simon); +