From 45dbcfad21997b8b2cb704f05c1e1d41fefb3dc7 Mon Sep 17 00:00:00 2001 From: ccremers Date: Tue, 21 Nov 2006 13:42:06 +0000 Subject: [PATCH] - Added SPORE protocols. --- spdl/SPORE/NotModelled.txt | 23 +++ spdl/SPORE/andrew-ban-concrete.spdl | 96 ++++++++++++ spdl/SPORE/andrew-ban.spdl | 86 +++++++++++ spdl/SPORE/andrew-lowe-ban.spdl | 91 +++++++++++ spdl/SPORE/andrew.spdl | 85 +++++++++++ spdl/SPORE/ccitt509-1.spdl | 46 ++++++ spdl/SPORE/ccitt509-1c.spdl | 44 ++++++ spdl/SPORE/ccitt509-3.spdl | 55 +++++++ spdl/SPORE/ccitt509-ban3.spdl | 49 ++++++ spdl/SPORE/denning-sacco-lowe.spdl | 100 +++++++++++++ spdl/SPORE/denning-sacco.spdl | 87 +++++++++++ spdl/SPORE/kaochow-v2.spdl | 97 ++++++++++++ spdl/SPORE/kaochow-v3.spdl | 104 +++++++++++++ spdl/SPORE/kaochow.spdl | 95 ++++++++++++ .../key-compromise/needham-schroeder-sk.spdl | 88 +++++++++++ spdl/SPORE/ksl-lowe.spdl | 115 ++++++++++++++ spdl/SPORE/ksl.spdl | 86 +++++++++++ spdl/SPORE/needham-schroeder-lowe.spdl | 66 ++++++++ spdl/SPORE/needham-schroeder-sk-amend.spdl | 101 +++++++++++++ spdl/SPORE/needham-schroeder-sk.spdl | 88 +++++++++++ spdl/SPORE/needham-schroeder.spdl | 67 +++++++++ spdl/SPORE/neumannstub-guttman-hwang.spdl | 116 ++++++++++++++ spdl/SPORE/neumannstub-guttman.spdl | 116 ++++++++++++++ spdl/SPORE/neumannstub-hwang.spdl | 108 ++++++++++++++ spdl/SPORE/neumannstub-keycompromise.spdl | 141 ++++++++++++++++++ spdl/SPORE/neumannstub.spdl | 116 ++++++++++++++ spdl/SPORE/otwayrees.spdl | 87 +++++++++++ spdl/SPORE/smartright.spdl | 58 +++++++ spdl/SPORE/splice-as-cj.spdl | 75 ++++++++++ spdl/SPORE/splice-as-hc.spdl | 72 +++++++++ spdl/SPORE/splice-as.spdl | 75 ++++++++++ spdl/SPORE/tmn.spdl | 82 ++++++++++ spdl/SPORE/wmf-lowe.spdl | 96 ++++++++++++ spdl/SPORE/wmf.spdl | 84 +++++++++++ spdl/SPORE/woo-lam-pi-1.spdl | 57 +++++++ spdl/SPORE/woo-lam-pi-2.spdl | 57 +++++++ spdl/SPORE/woo-lam-pi-3.spdl | 57 +++++++ spdl/SPORE/woo-lam-pi-f.spdl | 55 +++++++ spdl/SPORE/woo-lam-pi.spdl | 61 ++++++++ spdl/SPORE/woo-lam.spdl | 102 +++++++++++++ spdl/SPORE/yahalom-ban.spdl | 85 +++++++++++ spdl/SPORE/yahalom-lowe.spdl | 56 +++++++ spdl/SPORE/yahalom-paulson.spdl | 84 +++++++++++ spdl/SPORE/yahalom.spdl | 84 +++++++++++ 44 files changed, 3593 insertions(+) create mode 100644 spdl/SPORE/NotModelled.txt create mode 100644 spdl/SPORE/andrew-ban-concrete.spdl create mode 100644 spdl/SPORE/andrew-ban.spdl create mode 100644 spdl/SPORE/andrew-lowe-ban.spdl create mode 100644 spdl/SPORE/andrew.spdl create mode 100644 spdl/SPORE/ccitt509-1.spdl create mode 100644 spdl/SPORE/ccitt509-1c.spdl create mode 100644 spdl/SPORE/ccitt509-3.spdl create mode 100644 spdl/SPORE/ccitt509-ban3.spdl create mode 100644 spdl/SPORE/denning-sacco-lowe.spdl create mode 100644 spdl/SPORE/denning-sacco.spdl create mode 100644 spdl/SPORE/kaochow-v2.spdl create mode 100644 spdl/SPORE/kaochow-v3.spdl create mode 100644 spdl/SPORE/kaochow.spdl create mode 100644 spdl/SPORE/key-compromise/needham-schroeder-sk.spdl create mode 100644 spdl/SPORE/ksl-lowe.spdl create mode 100644 spdl/SPORE/ksl.spdl create mode 100644 spdl/SPORE/needham-schroeder-lowe.spdl create mode 100644 spdl/SPORE/needham-schroeder-sk-amend.spdl create mode 100644 spdl/SPORE/needham-schroeder-sk.spdl create mode 100644 spdl/SPORE/needham-schroeder.spdl create mode 100644 spdl/SPORE/neumannstub-guttman-hwang.spdl create mode 100644 spdl/SPORE/neumannstub-guttman.spdl create mode 100644 spdl/SPORE/neumannstub-hwang.spdl create mode 100644 spdl/SPORE/neumannstub-keycompromise.spdl create mode 100644 spdl/SPORE/neumannstub.spdl create mode 100644 spdl/SPORE/otwayrees.spdl create mode 100644 spdl/SPORE/smartright.spdl create mode 100644 spdl/SPORE/splice-as-cj.spdl create mode 100644 spdl/SPORE/splice-as-hc.spdl create mode 100644 spdl/SPORE/splice-as.spdl create mode 100644 spdl/SPORE/tmn.spdl create mode 100644 spdl/SPORE/wmf-lowe.spdl create mode 100644 spdl/SPORE/wmf.spdl create mode 100644 spdl/SPORE/woo-lam-pi-1.spdl create mode 100644 spdl/SPORE/woo-lam-pi-2.spdl create mode 100644 spdl/SPORE/woo-lam-pi-3.spdl create mode 100644 spdl/SPORE/woo-lam-pi-f.spdl create mode 100644 spdl/SPORE/woo-lam-pi.spdl create mode 100644 spdl/SPORE/woo-lam.spdl create mode 100644 spdl/SPORE/yahalom-ban.spdl create mode 100644 spdl/SPORE/yahalom-lowe.spdl create mode 100644 spdl/SPORE/yahalom-paulson.spdl create mode 100644 spdl/SPORE/yahalom.spdl diff --git a/spdl/SPORE/NotModelled.txt b/spdl/SPORE/NotModelled.txt new file mode 100644 index 0000000..120e55f --- /dev/null +++ b/spdl/SPORE/NotModelled.txt @@ -0,0 +1,23 @@ +The following protocols have not been modelled for use in Scyther: + +- CAM http://www.lsv.ens-cachan.fr/spore/cam.html +This protocol only consists of one message and corresponding database actions. +The description given in SPORE is unsuitable for formalisation. + +- Diffie Helman http://www.lsv.ens-cachan.fr/spore/diffieHelman.html +This protocol relies on algebraic properties that can not be modelled in +scyther. + +- GJM http://www.lsv.ens-cachan.fr/spore/gjm.html +This protocol contains complicated if-then-else constructions that can +not be modelled in scyther. + +- Gong http://www.lsv.ens-cachan.fr/spore/gong.html +This protocol relies on algebraic properties that can not be modelled in +scyther. + +- SK3 +This protocol relies on algebraic properties that can not be modelled in +scyther. It also has the notion of channels that can not be attacked, +which can not be modelled in scyther either. + diff --git a/spdl/SPORE/andrew-ban-concrete.spdl b/spdl/SPORE/andrew-ban-concrete.spdl new file mode 100644 index 0000000..d008d6b --- /dev/null +++ b/spdl/SPORE/andrew-ban-concrete.spdl @@ -0,0 +1,96 @@ +# 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; +secret k: Function; +const Fresh: Function; +const Compromised: 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^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const ni,nr: Nonce; + const kir: SessionKey; + var I,R: Agent; + + read_C1(C,C, I,R); + send_C2(C,C, (I,ni), + {ni,kir}k(I,R), + {ni}kir, + nr, + kir + ); + claim_C3(C,Empty, (Compromised,kir)); + } +} + + +protocol andrew-Concrete(I,R) +{ + + role I + { + const 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; + const nr: Nonce; + const 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/spdl/SPORE/andrew-ban.spdl b/spdl/SPORE/andrew-ban.spdl new file mode 100644 index 0000000..01dff68 --- /dev/null +++ b/spdl/SPORE/andrew-ban.spdl @@ -0,0 +1,86 @@ +# 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; +secret k: Function; +const Fresh: Function; +const Compromised: Function; + +protocol andrew-Ban^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const ni,nr,nr2: Nonce; + const kir: SessionKey; + var I,R: Agent; + + read_C1(C,C, I,R); + send_C2(C,C, (I,{ni}k(I,R)), + {ni,nr}k(I,R), + {nr}k(I,R), + {kir,nr2,ni}k(I,R), + kir + ); + claim_C3(C,Empty, (Compromised,kir)); + } +} + +protocol andrew-Ban(I,R) +{ + role I + { + const 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_I4(I,Secret, k(I,R)); + claim_I5(I,Empty, (Fresh,kir)); + } + + role R + { + var ni: Nonce; + const nr,nr2: Nonce; + const 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_R4(R,Secret, k(I,R)); + 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/spdl/SPORE/andrew-lowe-ban.spdl b/spdl/SPORE/andrew-lowe-ban.spdl new file mode 100644 index 0000000..0958dd8 --- /dev/null +++ b/spdl/SPORE/andrew-lowe-ban.spdl @@ -0,0 +1,91 @@ +# 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; +secret k: Function; +const Fresh: Function; +const Compromised: Function; + +protocol andrew-LoweBan^KeyCompromise(C) +{ + // Read the names of 2 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const ni,nr: Nonce; + const kir: SessionKey; + var I,R: Agent; + + read_C1(C,C, I,R); + send_C2(C,C, (I,ni), + {ni,kir,R}k(I,R), + {ni}kir, + nr, + kir + ); + claim_C3(C,Empty, (Compromised,kir)); + } +} + +protocol andrew-LoweBan(I,R) +{ + role I + { + const 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; + const nr: Nonce; + const 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/spdl/SPORE/andrew.spdl b/spdl/SPORE/andrew.spdl new file mode 100644 index 0000000..f56f43d --- /dev/null +++ b/spdl/SPORE/andrew.spdl @@ -0,0 +1,85 @@ +# Andrew Secure RPC +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/andrew.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 +# + +usertype SessionKey; +secret k: Function; +const succ: Function; +const Fresh: Function; +const Compromised: Function; + +protocol andrew^KeyCompromise(C) +{ + // Read the names of 2 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const ni,nr,nr2: Nonce; + const kir: SessionKey; + var I,R: Agent; + + read_C1(C,C, I,R); + send_C2(C,C, (I,{ni}k(I,R)), + {succ(ni),nr}k(I,R), + {succ(nr)}k(I,R), + {kir,nr2}k(I,R), + kir + ); + claim_C3(C,Empty, (Compromised,kir)); + } +} + +protocol andrew(I,R) +{ + role I + { + const ni: Nonce; + var nr,nr2: Nonce; + var kir: SessionKey; + + send_1(I,R, I,{ni}k(I,R) ); + read_2(R,I, {succ(ni),nr}k(I,R) ); + send_3(I,R, {succ(nr)}k(I,R) ); + read_4(R,I, {kir,nr2}k(I,R) ); + claim_I1(I,Secret,kir); + claim_I2(I,Nisynch); + claim_I3(I,Niagree); + claim_I4(I,Empty,(Fresh,kir)); + } + + role R + { + var ni: Nonce; + const nr,nr2: Nonce; + const kir: SessionKey; + + read_1(I,R, I,{ni}k(I,R) ); + send_2(R,I, {succ(ni),nr}k(I,R) ); + read_3(I,R, {succ(nr)}k(I,R) ); + send_4(R,I, {kir,nr2}k(I,R) ); + claim_R1(R,Secret,kir); + claim_R2(R,Nisynch); + claim_R3(R,Niagree); + claim_R4(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/spdl/SPORE/ccitt509-1.spdl b/spdl/SPORE/ccitt509-1.spdl new file mode 100644 index 0000000..5ed23ba --- /dev/null +++ b/spdl/SPORE/ccitt509-1.spdl @@ -0,0 +1,46 @@ +# CCITT X.509 (1) +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/ccittx509_1.html +# +# Note: +# The attack in SPORE is not found as this is not an attack against +# synchronisation, but an attack against the freshness of Xa and Ya +# 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; + 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 + } + + role R + { + var Ta: Timestamp; + var Na,Xa,Ya: Nonce; + + read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I)); + claim_3(R,Nisynch); + # There should also be Fresh Xa and Fresh Ya claims here + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const te: Timestamp; +compromised sk(Eve); + + diff --git a/spdl/SPORE/ccitt509-1c.spdl b/spdl/SPORE/ccitt509-1c.spdl new file mode 100644 index 0000000..228550c --- /dev/null +++ b/spdl/SPORE/ccitt509-1c.spdl @@ -0,0 +1,44 @@ +# CCITT X.509 (1c) +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/ccittx509_1c.html +# +# Note: +# 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); +usertype Timestamp; + +protocol ccitt509-1c(I,R) +{ + role I + { + const Ta: Timestamp; + const Na,Xa,Ya: Nonce; + send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); + # claim_2(I,Nisynch); + # This claim is useless as there are no preceding read events + } + + role R + { + var Ta: Timestamp; + var Na,Xa,Ya: Nonce; + + read_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I)); + claim_3(R,Nisynch); + # There should also be Fresh Xa and Fresh Ya claims here + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const te: Timestamp; +compromised sk(Eve); + diff --git a/spdl/SPORE/ccitt509-3.spdl b/spdl/SPORE/ccitt509-3.spdl new file mode 100644 index 0000000..e8ae1f1 --- /dev/null +++ b/spdl/SPORE/ccitt509-3.spdl @@ -0,0 +1,55 @@ +# CCITT X.509 (3) +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/ccittx509_3.html +# +# Note: +# The protocol description also states that Xa and Ya should be fresh +# 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; + var Tb: Timestamp; + const 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)); + send_3(I,R, I, {Nb}sk(I)); + claim_I1(I,Nisynch); + claim_I2(I,Secret,Ya); + claim_I3(I,Secret,Yb); + } + + role R + { + var Ta: Timestamp; + const Tb: Timestamp; + var Na,Xa,Ya: Nonce; + const 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)); + read_3(I,R, I, {Nb}sk(I)); + claim_R1(R,Nisynch); + claim_R2(R,Secret,Ya); + claim_R3(R,Secret,Yb); + # There should also be Fresh Xa and Fresh Ya claims here + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const te: Timestamp; +compromised sk(Eve); + diff --git a/spdl/SPORE/ccitt509-ban3.spdl b/spdl/SPORE/ccitt509-ban3.spdl new file mode 100644 index 0000000..9c0d3c1 --- /dev/null +++ b/spdl/SPORE/ccitt509-ban3.spdl @@ -0,0 +1,49 @@ +# 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 +# + +const pk: Function; +secret sk: Function; +inversekeys(pk,sk); + +protocol ccitt509-ban3(I,R) +{ + role I + { + const 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; + const 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/spdl/SPORE/denning-sacco-lowe.spdl b/spdl/SPORE/denning-sacco-lowe.spdl new file mode 100644 index 0000000..bb0e576 --- /dev/null +++ b/spdl/SPORE/denning-sacco-lowe.spdl @@ -0,0 +1,100 @@ +# Lowe modified Denning-Sacco shared key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/denningSaccoLowe.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# +# 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; +secret k: Function; +usertype PseudoFunction; +const dec: PseudoFunction; +const Fresh: Function; +const Compromised: Function; + +protocol denningSacco-Lowe^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + const T: ExpiredTimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R), + {R,Kir,T,{Kir,I,T}k(R,S)}k(I,S), + {Kir,I,T}k(R,S), + {Nr}Kir, + {{Nr}dec}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +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; + const 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; + const Kir: SessionKey; + const 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/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl new file mode 100644 index 0000000..3fd1d94 --- /dev/null +++ b/spdl/SPORE/denning-sacco.spdl @@ -0,0 +1,87 @@ +# Denning-Sacco shared key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/denningSacco.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +usertype Key; +usertype SessionKey; +usertype TimeStamp; +usertype ExpiredTimeStamp; +secret k: Function; +const Fresh: Function; +const Compromised: Function; + +protocol denningSacco^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + const T: ExpiredTimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R), + {R,Kir,T,{Kir,I,T}k(R,S)}k(I,S), + {Kir,I,T}k(R,S), + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +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; + const Kir: SessionKey; + const 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/spdl/SPORE/kaochow-v2.spdl b/spdl/SPORE/kaochow-v2.spdl new file mode 100644 index 0000000..450a60f --- /dev/null +++ b/spdl/SPORE/kaochow-v2.spdl @@ -0,0 +1,97 @@ +# Kao Chow Authentication v.2 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/kaoChow2.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +usertype SessionKey; +secret k: Function; +const Fresh: Function; +const Compromised: Function; + +protocol kaochow-2^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir,Kt: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R,Ni), + {I,R,Ni,Kir,Kt}k(I,S), + {I,R,Ni,Kir,Kt}k(R,S), + R, Nr, + {Nr,Kir}Kt, + Kir + // Kt + ); + claim_C3(C,Empty, (Compromised,Kir)); + // claim_C4(C,Empty, (Compromised,Kt)); + } +} + +protocol kaochow-2(I,R,S) +{ + role I + { + const 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; + const 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; + const 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/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl new file mode 100644 index 0000000..54bf862 --- /dev/null +++ b/spdl/SPORE/kaochow-v3.spdl @@ -0,0 +1,104 @@ +# Kao Chow Authentication v.3 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/kaoChow3.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +usertype SessionKey; +usertype ExpiredTimeStamp; +usertype TimeStamp; +secret k: Function; +const Fresh: Function; +const Compromised: Function; + +protocol kaochow-3^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir,Kt: SessionKey; + const T2: ExpiredTimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R,Ni), + {I,R,Ni,Kir,Kt}k(I,S), + {I,R,Ni,Kir,Kt}k(R,S), + {Ni,Kir}Kt, + Nr, + {I,R,T2,Kir}k(R,S), + {Nr,Kir}Kt, + Kir + // Kt + ); + claim_C3(C,Empty, (Compromised,Kir)); + // claim_C4(C,Empty, (Compromised,Kt)); + } +} + +protocol kaochow-3(I,R,S) +{ + role I + { + const 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; + const nr: Nonce; + var kir,kt: SessionKey; + var T: Ticket; + const 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; + const 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/spdl/SPORE/kaochow.spdl b/spdl/SPORE/kaochow.spdl new file mode 100644 index 0000000..021397a --- /dev/null +++ b/spdl/SPORE/kaochow.spdl @@ -0,0 +1,95 @@ +# Kao Chow Authentication v.1 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/kaoChow1.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +usertype SessionKey; +secret k: Function; +const Fresh: Function; +const Compromised: Function; + +protocol kaochow^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R,Ni), + {I,R,Ni,Kir}k(I,S), + {I,R,Ni,Kir}k(R,S), + {Ni}Kir, Nr, + {Nr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +protocol kaochow(I,R,S) +{ + role I + { + const 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; + const 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; + const 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/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl b/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl new file mode 100644 index 0000000..9be70bf --- /dev/null +++ b/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl @@ -0,0 +1,88 @@ +# Needham Schroeder Symmetric Key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/nssk.html +# +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + + +secret k: Function; +# Model dec that is invertible by inc +const dec,inc: Function; +inversekeys(dec,inc); +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol needhamschroederSessionKeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R,Ni), + {Ni,R,Kir,{Kir,I}k(R,S)}k(I,S), + {Kir,I}k(R,S), + {Nr}Kir, + {{Nr}dec}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +protocol needhamschroedersk(I,R,S) +{ + role I + { + const 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 + { + const 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; + const 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/spdl/SPORE/ksl-lowe.spdl b/spdl/SPORE/ksl-lowe.spdl new file mode 100644 index 0000000..3a5063b --- /dev/null +++ b/spdl/SPORE/ksl-lowe.spdl @@ -0,0 +1,115 @@ +# Lowe modified KSL +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/kslLowe.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# +# Note: +# According to SPORE there are no attacks on this protocol, scyther +# finds one however. This has to be investigated further. + +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^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr,Nc,Ma,Mb: Nonce; + const Kir: SessionKey; + const Kbb: TicketKey; + const Tr: ExpiredTimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (Ni,I), + (Ni,I,Nr,R), + {I,Nr,Kir}k(R,S),{Ni,R,Kir}k(I,S), + {Tr,I,Kir}Kbb,Nc,{R,Ni}k(I,R), + {Nc}Kir, + Ma, + Mb,{Ma,R}Kir, + {I,Mb}Kir, + Kir, + Kbb + ); + claim_C3(C,Empty, (Compromised,Kir)); + claim_C4(C,Empty, (Compromised,Kbb)); + } +} + +protocol ksl-Lowe(I,R,S) +{ + role I + { + const Ni, Mi: Nonce; + var Nc, Mr: Nonce; + var T: Ticket; + var Kir: SessionKey; + + send_1(I,R, Ni, I); + read_4(R,I, { Ni,R,Kir }k(I,S), T, Nc, {R,Ni}Kir ); + send_5(I,R, { Nc }Kir ); + + send_6(I,R, Mi,T ); + read_7(R,I, Mr,{Mi, R}Kir ); + send_8(I,R, {I,Mr}Kir ); + + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty, (Fresh,Kir)); + } + + role R + { + var Ni,Mi: Nonce; + const Nr,Nc,Mr: Nonce; + var Kir: SessionKey; + const Kbb: TicketKey; + const Tr: TimeStamp; + var T: Ticket; + + read_1(I,R, Ni, I); + send_2(R,S, Ni, I, Nr, R ); + read_3(S,R, { I, Nr, Kir }k(R,S), T ); + send_4(R,I, T, { Tr, I, Kir }Kbb, Nc, {R, Ni}Kir ); + read_5(I,R, { Nc }Kir ); + + read_6(I,R, Mi,{ Tr, I, Kir }Kbb ); + send_7(R,I, Mr,{Mi,R}Kir ); + read_8(I,R, {I,Mr}Kir ); + + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty, (Fresh,Kir)); + } + + role S + { + var Ni, Nr: Nonce; + const 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/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl new file mode 100644 index 0000000..dddf135 --- /dev/null +++ b/spdl/SPORE/ksl.spdl @@ -0,0 +1,86 @@ +# KSL +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/ksl.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + + +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; + var Nc, Mr: Nonce; + var T: Ticket; + var Kir: SessionKey; + + send_1(I,R, Ni, I); + read_4(R,I, { Ni,R,Kir }k(I,S), T, Nc, {Ni}Kir ); + send_5(I,R, { Nc }Kir ); + + send_6(I,R, Mi,T ); + read_7(R,I, Mr,{Mi}Kir ); + send_8(I,R, {Mr}Kir ); + + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty, (Fresh, Kir)); + } + + role R + { + var Ni,Mi: Nonce; + const Nr,Nc,Mr: Nonce; + var Kir: SessionKey; + const Kbb: TicketKey; + const Tr: TimeStamp; + var T: Ticket; + + read_1(I,R, Ni, I); + send_2(R,S, Ni, I, Nr, R ); + read_3(S,R, { Nr, I, Kir }k(R,S), T ); + send_4(R,I, T, { Tr, I, Kir }Kbb, Nc, {Ni}Kir ); + read_5(I,R, { Nc }Kir ); + + read_6(I,R, Mi,{ Tr, I, Kir }Kbb ); + send_7(R,I, Mr,{Mi}Kir ); + read_8(I,R, {Mr}Kir ); + + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + var Ni, Nr: Nonce; + const 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/spdl/SPORE/needham-schroeder-lowe.spdl b/spdl/SPORE/needham-schroeder-lowe.spdl new file mode 100644 index 0000000..638f5ab --- /dev/null +++ b/spdl/SPORE/needham-schroeder-lowe.spdl @@ -0,0 +1,66 @@ +# Lowe's fixed version of Needham Schroeder Public Key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/nspkLowe.html +# +# +# Note: +# The modelling in SPORE includes a server to distribute the public keys +# of the agents, this is not necessary and it allows for attacks against +# 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; + var Nr: Nonce; + + send_1(I,S, (I,R)); + read_2(S,I, {pk(R), R}sk(S)); + send_3(I,R,{Ni,I}pk(R)); + read_6(R,I, {Ni,Nr,R}pk(I)); + send_7(I,R, {Nr}pk(R)); + claim_I1(I,Secret,Ni); + claim_I2(I,Secret,Nr); + claim_I3(I,Nisynch); + } + + role R + { + const Nr: Nonce; + var Ni: Nonce; + + read_3(I,R,{Ni,I}pk(R)); + send_4(R,S,(R,I)); + read_5(S,R,{pk(I),I}sk(S)); + send_6(R,I,{Ni,Nr,R}pk(I)); + read_7(I,R,{Nr}pk(R)); + claim_R1(R,Secret,Nr); + claim_R2(R,Secret,Ni); + claim_R3(R,Nisynch); + } + + role S + { + read_1(I,S,(I,R)); + send_2(S,I,{pk(R),R}sk(S)); + read_4(R,S,(R,I)); + send_5(S,R,{pk(I),I}sk(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/spdl/SPORE/needham-schroeder-sk-amend.spdl b/spdl/SPORE/needham-schroeder-sk-amend.spdl new file mode 100644 index 0000000..7be987a --- /dev/null +++ b/spdl/SPORE/needham-schroeder-sk-amend.spdl @@ -0,0 +1,101 @@ +# Amended Needham Schroeder Symmetric Key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/nssk_amended.html +# +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# +# Note: +# According to SPORE there are no attacks on this protocol, scyther +# finds one however. This has to be investigated further. + + + +secret k: Function; +# 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^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I, + {I,Nr}k(R,S), + I,R,Ni,{I,Nr}k(R,S), + {Ni,R,Kir,{Kir,Nr,I}k(R,S)}k(I,S), + {Kir,Nr,I}k(R,S), + {Nr}Kir, + {{Nr}dec}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +protocol needhamschroedersk-amend(I,R,S) +{ + role I + { + const 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 + { + const 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; + const 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/spdl/SPORE/needham-schroeder-sk.spdl b/spdl/SPORE/needham-schroeder-sk.spdl new file mode 100644 index 0000000..5fb9a85 --- /dev/null +++ b/spdl/SPORE/needham-schroeder-sk.spdl @@ -0,0 +1,88 @@ +# Needham Schroeder Symmetric Key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/nssk.html +# +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + + +secret k: Function; +# Model dec that is invertible by inc +const dec,inc: Function; +inversekeys(dec,inc); +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol needhamschroedersk^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R,Ni), + {Ni,R,Kir,{Kir,I}k(R,S)}k(I,S), + {Kir,I}k(R,S), + {Nr}Kir, + {{Nr}dec}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +protocol needhamschroedersk(I,R,S) +{ + role I + { + const 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 + { + const 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; + const 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/spdl/SPORE/needham-schroeder.spdl b/spdl/SPORE/needham-schroeder.spdl new file mode 100644 index 0000000..fda6c8c --- /dev/null +++ b/spdl/SPORE/needham-schroeder.spdl @@ -0,0 +1,67 @@ +# Needham Schroeder Public Key +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/nspk.html +# +# +# Note: +# The modelling in SPORE includes a server to distribute the public keys +# of the agents, this is not necessary and it allows for attacks against +# 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; + var Nr: Nonce; + + send_1(I,S,(I,R)); + read_2(S,I, {pk(R), R}sk(S)); + send_3(I,R,{Ni,I}pk(R)); + read_6(R,I, {Ni, Nr}pk(I)); + send_7(I,R, {Nr}pk(R)); + claim_I1(I,Secret,Ni); + claim_I2(I,Secret,Nr); + claim_I3(I,Nisynch); + } + + role R + { + const Nr: Nonce; + var Ni: Nonce; + + read_3(I,R,{Ni,I}pk(R)); + send_4(R,S,(R,I)); + read_5(S,R,{pk(I),I}sk(S)); + send_6(R,I,{Ni,Nr}pk(I)); + read_7(I,R,{Nr}pk(R)); + claim_R1(R,Secret,Nr); + claim_R2(R,Secret,Ni); + claim_R3(R,Nisynch); + } + + role S + { + read_1(I,S,(I,R)); + send_2(S,I,{pk(R),R}sk(S)); + read_4(R,S,(R,I)); + send_5(S,R,{pk(I),I}sk(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/spdl/SPORE/neumannstub-guttman-hwang.spdl b/spdl/SPORE/neumannstub-guttman-hwang.spdl new file mode 100644 index 0000000..f289224 --- /dev/null +++ b/spdl/SPORE/neumannstub-guttman-hwang.spdl @@ -0,0 +1,116 @@ +# Neumann Stubblebine +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# +# Note: +# In SPORE this protocol is not described correctly, there are in fact 2 +# different protocols (the key establishment protocol and the repeated +# authentication protocol) + +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; + + role I + { + const Mi: Nonce; + var Mr: Nonce; + const Kir: SessionKey; + const Tr: TimeStamp; + + send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); + read_6(R,I,{Mi,Mr}Kir); + send_7(I,R,{I,Mr}Kir); + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + const Mr: Nonce; + var Tr: TimeStamp; + var Kir: SessionKey; + var Mi: Nonce; + + read_5(I,R,Mi,{I,Kir,Tr}k(R,S)); + send_6(R,I,{Mi,Mr}Kir); + read_7(I,R,{I,Mr}Kir); + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + } +} +protocol neustub-GuttmanHwang(I,R,S) +{ + role I + { + const Ni: Nonce; + var Nr: Nonce; + var T: Ticket; + var Tb: TimeStamp; + var Kir: SessionKey; + + send_1(I,R, I, Ni); + read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); + send_!4(I,R,T,{Nr}Kir); + + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + var Ni,Mi: Nonce; + const Nr,Mr: Nonce; + var Kir: SessionKey; + const Tb: TimeStamp; + var T: Ticket; + + read_1(I,R, I, Ni); + send_!2(R,S, R, {I, Ni, Tb ,Nr}k(R,S)); + read_!4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); + + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + var Ni, Nr: Nonce; + const Kir: SessionKey; + var Tb: TimeStamp; + + read_!2(R,S, R, {I,Ni,Tb,Nr}k(R,S)); + send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); + } +} + diff --git a/spdl/SPORE/neumannstub-guttman.spdl b/spdl/SPORE/neumannstub-guttman.spdl new file mode 100644 index 0000000..7d343b0 --- /dev/null +++ b/spdl/SPORE/neumannstub-guttman.spdl @@ -0,0 +1,116 @@ +# Neumann Stubblebine +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# +# Note: +# In SPORE this protocol is not described correctly, there are in fact 2 +# different protocols (the key establishment protocol and the repeated +# authentication protocol) + +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; + + role I + { + const Mi: Nonce; + var Mr: Nonce; + const Kir: SessionKey; + const Tr: TimeStamp; + + send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); + read_6(R,I,{Mi,Mr}Kir); + send_7(I,R,{I,Mr}Kir); + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + const Mr: Nonce; + var Tr: TimeStamp; + var Kir: SessionKey; + var Mi: Nonce; + + read_5(I,R,Mi,{I,Kir,Tr}k(R,S)); + send_6(R,I,{Mi,Mr}Kir); + read_7(I,R,{I,Mr}Kir); + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + } +} +protocol neustub(I,R,S) +{ + role I + { + const Ni: Nonce; + var Nr: Nonce; + var T: Ticket; + var Tb: TimeStamp; + var Kir: SessionKey; + + send_1(I,R, I, Ni); + read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); + send_4(I,R,T,{Nr}Kir); + + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + var Ni,Mi: Nonce; + const Nr,Mr: Nonce; + var Kir: SessionKey; + const Tb: TimeStamp; + var T: Ticket; + + read_1(I,R, I, Ni); + send_!2(R,S, R, {I, Ni, Tb}k(R,S),Nr); + read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); + + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + var Ni, Nr: Nonce; + const Kir: SessionKey; + var Tb: TimeStamp; + + read_!2(R,S, R, {I,Ni,Tb}k(R,S), Nr); + send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); + } +} + diff --git a/spdl/SPORE/neumannstub-hwang.spdl b/spdl/SPORE/neumannstub-hwang.spdl new file mode 100644 index 0000000..c079cf5 --- /dev/null +++ b/spdl/SPORE/neumannstub-hwang.spdl @@ -0,0 +1,108 @@ +# Hwang modified Neumann Stubblebine +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/neumannStubblebineHwang.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# +# Note: +# According to SPORE there are no attacks on this protocol, scyther +# finds one however. This has to be investigated further. + + +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^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr,Mi,Mr: Nonce; + const Kir: SessionKey; + const Tr: ExpiredTimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,Ni, + R,{I,Ni,Tr,Nr}k(R,S), + {R,Ni,Kir,Tr}k(I,S), + {I,Kir,Tr}k(R,S), Nr, + {Nr}Kir, + Mi,{I,Kir,Tr}k(R,S), + Mr,{Mi}Kir, + {Mr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +protocol neustub-Hwang(I,R,S) +{ + role I + { + const Ni,Mi: Nonce; + var Nr,Mr: Nonce; + var T: Ticket; + var Tb: TimeStamp; + var Kir: SessionKey; + + send_1(I,R, I, Ni); + read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); + send_4(I,R,T,{Nr}Kir); + send_5(I,R,Mi,T); + read_6(R,I,Mr,{Mi}Kir); + send_7(I,R,{Mr}Kir); + + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + var Ni,Mi: Nonce; + const Nr,Mr: Nonce; + var Kir: SessionKey; + const Tb: TimeStamp; + var T: Ticket; + + read_1(I,R, I, Ni); + send_!2(R,S, R, {I, Ni, Tb, Nr}k(R,S)); + read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); + read_5(I,R,Mi,T); + send_6(R,I,Mr,{Mi}Kir); + read_7(I,R,{Mr}Kir); + + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + var Ni, Nr: Nonce; + const Kir: SessionKey; + var Tb: TimeStamp; + + read_!2(R,S, R, {I,Ni,Tb,Nr}k(R,S)); + send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); + } +} + diff --git a/spdl/SPORE/neumannstub-keycompromise.spdl b/spdl/SPORE/neumannstub-keycompromise.spdl new file mode 100644 index 0000000..e11d13d --- /dev/null +++ b/spdl/SPORE/neumannstub-keycompromise.spdl @@ -0,0 +1,141 @@ +# Neumann Stubblebine +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# +# Note: +# In SPORE this protocol is not described correctly, there are in fact 2 +# different protocols (the key establishment protocol and the repeated +# authentication protocol) + +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^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr,Mi,Mr: Nonce; + const Kir: SessionKey; + const Tr: ExpiredTimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,Ni, + R,{I,Ni,Tr}k(R,S),Nr, + {R,Ni,Kir,Tr}k(I,S), + {I,Kir,Tr}k(R,S), Nr, + {Nr}Kir, + Mi,{I,Kir,Tr}k(R,S), + Mr,{Mi}Kir, + {Mr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +protocol neustub^Repeat(I,R,S) +{ + const Kir: SessionKey; + + role I + { + const Mi: Nonce; + var Mr: Nonce; + const Kir: SessionKey; + const Tr: TimeStamp; + + send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); + read_6(R,I,Mr,{Mi}Kir); + send_7(I,R,{Mr}Kir); + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + const Mr: Nonce; + var Tr: TimeStamp; + var Kir: SessionKey; + var Mi: Nonce; + + read_5(I,R,Mi,{I,Kir,Tr}k(R,S)); + send_6(R,I,Mr,{Mi}Kir); + read_7(I,R,{Mr}Kir); + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + } +} +protocol neustub(I,R,S) +{ + role I + { + const Ni: Nonce; + var Nr: Nonce; + var T: Ticket; + var Tb: TimeStamp; + var Kir: SessionKey; + + send_1(I,R, I, Ni); + read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); + send_4(I,R,T,{Nr}Kir); + + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + var Ni,Mi: Nonce; + const Nr,Mr: Nonce; + var Kir: SessionKey; + const Tb: TimeStamp; + var T: Ticket; + + read_1(I,R, I, Ni); + send_2(R,S, R, {I, Ni, Tb}k(R,S),Nr); + read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); + + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + var Ni, Nr: Nonce; + const Kir: SessionKey; + var Tb: TimeStamp; + + read_2(R,S, R, {I,Ni,Tb}k(R,S), Nr); + send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); + } +} + diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl new file mode 100644 index 0000000..7c5e429 --- /dev/null +++ b/spdl/SPORE/neumannstub.spdl @@ -0,0 +1,116 @@ +# Neumann Stubblebine +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/neumannStubblebine.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# +# Note: +# In SPORE this protocol is not described correctly, there are in fact 2 +# different protocols (the key establishment protocol and the repeated +# authentication protocol) + +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; + + role I + { + const Mi: Nonce; + var Mr: Nonce; + const Kir: SessionKey; + const Tr: TimeStamp; + + send_5(I,R,Mi,{I,Kir,Tr}k(R,S)); + read_6(R,I,Mr,{Mi}Kir); + send_7(I,R,{Mr}Kir); + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + const Mr: Nonce; + var Tr: TimeStamp; + var Kir: SessionKey; + var Mi: Nonce; + + read_5(I,R,Mi,{I,Kir,Tr}k(R,S)); + send_6(R,I,Mr,{Mi}Kir); + read_7(I,R,{Mr}Kir); + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + } +} +protocol neustub(I,R,S) +{ + role I + { + const Ni: Nonce; + var Nr: Nonce; + var T: Ticket; + var Tb: TimeStamp; + var Kir: SessionKey; + + send_1(I,R, I, Ni); + read_!3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr); + send_4(I,R,T,{Nr}Kir); + + claim_I1(I,Secret, Kir); + claim_I2(I,Niagree); + claim_I3(I,Nisynch); + claim_I4(I,Empty,(Fresh,Kir)); + } + + role R + { + var Ni,Mi: Nonce; + const Nr,Mr: Nonce; + var Kir: SessionKey; + const Tb: TimeStamp; + var T: Ticket; + + read_1(I,R, I, Ni); + send_!2(R,S, R, {I, Ni, Tb}k(R,S),Nr); + read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir); + + claim_R1(R,Secret, Kir); + claim_R2(R,Niagree); + claim_R3(R,Nisynch); + claim_R4(R,Empty,(Fresh,Kir)); + } + + role S + { + var Ni, Nr: Nonce; + const Kir: SessionKey; + var Tb: TimeStamp; + + read_!2(R,S, R, {I,Ni,Tb}k(R,S), Nr); + send_!3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr ); + } +} + diff --git a/spdl/SPORE/otwayrees.spdl b/spdl/SPORE/otwayrees.spdl new file mode 100644 index 0000000..a2bee13 --- /dev/null +++ b/spdl/SPORE/otwayrees.spdl @@ -0,0 +1,87 @@ +# Otway Rees +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/otwayRees.html +# +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + + +secret const k : Function; +const Fresh: Function; +const Compromised: Function; + +usertype String,SessionKey; + +protocol otwayRees^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const M: String; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, M,I,R,{Ni,M,I,R}k(I,S), + {Nr,M,I,R}k(R,S), + {Ni,Kir}k(I,S), {Nr,Kir}k(R,S), + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +protocol otwayrees(I,R,S) +{ + role I + { + const Ni : Nonce; + const 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; + const 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; + const 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/spdl/SPORE/smartright.spdl b/spdl/SPORE/smartright.spdl new file mode 100644 index 0000000..3133457 --- /dev/null +++ b/spdl/SPORE/smartright.spdl @@ -0,0 +1,58 @@ +# SmartRight view-only +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/smartright_viewonly.html +# +# Note: +# According to SPORE there are no known attacks on this protocol +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# +# Note: +# 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); +usertype SessionKey; +usertype XorKey; +const Vor: XorKey; + +protocol smartright(I,R) +{ + role I + { + const VoKey: SessionKey; + const VoR: XorKey; + const CW; + var VoRi: Nonce; + + send_1(I,R, {VoKey,{CW}VoR}k(I,R)); + read_2(R,I, VoRi); + send_3(I,R, VoR, {{VoRi}hash}VoKey); + } + + role R + { + var T: Ticket; + var VoR: XorKey; + var VoKey: SessionKey; + const VoRi: Nonce; + + read_1(I,R, {VoKey,T}k(I,R)); + send_2(R,I, VoRi); + read_3(I,R, VoR,{{VoRi}hash}VoKey); + + claim_R1(R,Nisynch); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; + diff --git a/spdl/SPORE/splice-as-cj.spdl b/spdl/SPORE/splice-as-cj.spdl new file mode 100644 index 0000000..00f4576 --- /dev/null +++ b/spdl/SPORE/splice-as-cj.spdl @@ -0,0 +1,75 @@ +# 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 pk: Function; +secret sk: Function; +inversekeys (pk,sk); +const inc,dec: Function; +inversekeys (inc,dec); + +protocol spliceAS-CJ(I,R,S) +{ + role I + { + const N1,N2: Nonce; + const T: TimeStamp; + const 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 + { + const N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; + + var ni: Nonce; + const 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/spdl/SPORE/splice-as-hc.spdl b/spdl/SPORE/splice-as-hc.spdl new file mode 100644 index 0000000..d49f7c3 --- /dev/null +++ b/spdl/SPORE/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 + { + const N1,N2: Nonce; + const T: TimeStamp; + const 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 + { + const N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; + + var ni: Nonce; + const 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/spdl/SPORE/splice-as.spdl b/spdl/SPORE/splice-as.spdl new file mode 100644 index 0000000..25df821 --- /dev/null +++ b/spdl/SPORE/splice-as.spdl @@ -0,0 +1,75 @@ +# 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 pk: Function; +secret sk: Function; +inversekeys (pk,sk); +const inc,dec: Function; +inversekeys (inc,dec); + +protocol spliceAS(I,R,S) +{ + role I + { + const N1,N2: Nonce; + const T: TimeStamp; + const 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 + { + const N3: Nonce; + var N2: Nonce; + var T: TimeStamp; + var L: LifeTime; + + var ni: Nonce; + const 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/spdl/SPORE/tmn.spdl b/spdl/SPORE/tmn.spdl new file mode 100644 index 0000000..59e2736 --- /dev/null +++ b/spdl/SPORE/tmn.spdl @@ -0,0 +1,82 @@ +# 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 pk: Function; +secret sk: Function; +inversekeys(pk,sk); +const Fresh: Function; +const Compromised: Function; + +protocol tmn^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kr,Ki: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, R,{Ki}pk(S), + I, {Kr}pk(S), + {Kr}Ki, + Kr + ); + claim_C3(C,Empty, (Compromised,Kr)); + } +} + +protocol tmn(I,R,S) +{ + role I + { + const 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 + { + const 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/spdl/SPORE/wmf-lowe.spdl b/spdl/SPORE/wmf-lowe.spdl new file mode 100644 index 0000000..0dbade1 --- /dev/null +++ b/spdl/SPORE/wmf-lowe.spdl @@ -0,0 +1,96 @@ +# 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; + +secret k: Function; + +protocol wmf-Lowe^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + const Ti,Ts: ExpiredTimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I, {I,Ti,R,Kir}k(I,S), + {S,Ts,I,Kir}k(R,S), + {R,Nr}Kir, + {I,{Nr}succ}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +protocol wmf-Lowe(I,R,S) +{ + role I + { + const Kir: SessionKey; + const 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; + const 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; + const 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/spdl/SPORE/wmf.spdl b/spdl/SPORE/wmf.spdl new file mode 100644 index 0000000..80ae8f2 --- /dev/null +++ b/spdl/SPORE/wmf.spdl @@ -0,0 +1,84 @@ +# 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; + +secret k: Function; +const Fresh: Function; +const Compromised: Function; + +protocol wmf^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + const Ti,Ts: ExpiredTimeStamp; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I, {I,Ti,R,Kir}k(I,S), + {S,Ts,I,Kir}k(R,S), + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +protocol wmf(I,R,S) +{ + role I + { + const Kir: SessionKey; + const 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; + const 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/spdl/SPORE/woo-lam-pi-1.spdl b/spdl/SPORE/woo-lam-pi-1.spdl new file mode 100644 index 0000000..811ef4a --- /dev/null +++ b/spdl/SPORE/woo-lam-pi-1.spdl @@ -0,0 +1,57 @@ +# Woo and Lam Pi 1 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamPi1.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +secret k: Function; + +protocol woolamPi-1(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 + { + const 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, 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, {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/spdl/SPORE/woo-lam-pi-2.spdl b/spdl/SPORE/woo-lam-pi-2.spdl new file mode 100644 index 0000000..416946c --- /dev/null +++ b/spdl/SPORE/woo-lam-pi-2.spdl @@ -0,0 +1,57 @@ +# Woo and Lam Pi 2 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamPi2.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +secret k: Function; + +protocol woolamPi-2(I,R,S) +{ + role I + { + var Nr: Nonce; + + send_1(I,R, I); + read_2(R,I, Nr); + send_3(I,R, {I,Nr}k(I,S)); + + } + + role R + { + const 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, T}k(R,S)); + read_5(S,R, {I, Nr}k(R,S)); + + claim_R1(R,Nisynch); + } + + role S + { + var Nr: Nonce; + + read_4(R,S, {I, {I,Nr}k(I,S)}k(R,S)); + send_5(S,R, {I,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/spdl/SPORE/woo-lam-pi-3.spdl b/spdl/SPORE/woo-lam-pi-3.spdl new file mode 100644 index 0000000..c930e81 --- /dev/null +++ b/spdl/SPORE/woo-lam-pi-3.spdl @@ -0,0 +1,57 @@ +# Woo and Lam Pi 2 +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamPi3.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +secret k: Function; + +protocol woolamPi-3(I,R,S) +{ + role I + { + var Nr: Nonce; + + send_1(I,R, I); + read_2(R,I, Nr); + send_3(I,R, {Nr}k(I,S)); + + } + + role R + { + const 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, T}k(R,S)); + read_5(S,R, {I, Nr}k(R,S)); + + claim_R1(R,Nisynch); + } + + role S + { + var Nr: Nonce; + + read_4(R,S, {I, {Nr}k(I,S)}k(R,S)); + send_5(S,R, {I,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/spdl/SPORE/woo-lam-pi-f.spdl b/spdl/SPORE/woo-lam-pi-f.spdl new file mode 100644 index 0000000..a3ecd57 --- /dev/null +++ b/spdl/SPORE/woo-lam-pi-f.spdl @@ -0,0 +1,55 @@ +# Woo and Lam Pi f +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamPif.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +secret k: Function; + +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 + { + const 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/spdl/SPORE/woo-lam-pi.spdl b/spdl/SPORE/woo-lam-pi.spdl new file mode 100644 index 0000000..04295f4 --- /dev/null +++ b/spdl/SPORE/woo-lam-pi.spdl @@ -0,0 +1,61 @@ +# Woo and Lam Pi +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamPi.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# +# Note: +# Scyther finds an attack that appears to be legit, but is not present in +# SPORE. +# + +secret k: Function; + +protocol woolamPi(I,R,S) +{ + role I + { + var Nr: Nonce; + + send_1(I,R, I); + read_2(R,I, Nr); + send_3(I,R, {Nr}k(I,S)); + + } + + role R + { + const 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, T}k(R,S)); + read_5(S,R, {Nr}k(R,S)); + + claim_R1(R,Nisynch); + } + + role S + { + var Nr: Nonce; + + read_4(R,S, {I,{Nr}k(I,S)}k(R,S)); + send_5(S,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/spdl/SPORE/woo-lam.spdl b/spdl/SPORE/woo-lam.spdl new file mode 100644 index 0000000..8613167 --- /dev/null +++ b/spdl/SPORE/woo-lam.spdl @@ -0,0 +1,102 @@ +# Woo and Lam Mutual Authentication +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/wooLamMutual.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + + +usertype SessionKey; + +secret k: Function; +const Fresh: Function; +const Compromised: Function; + +protocol woolam^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const N1,N2: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,N1, + R,N2, + {I,R,N1,N2}k(I,S), + {I,R,N1,N2}k(R,S), + {R,N1,N2,Kir}k(I,S), + {I,N1,N2,Kir}k(R,S), + {N1,N2}Kir, + {N2}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + +protocol woolam(I,R,S) +{ + role I + { + const 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 + { + const 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 + { + const 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)); + } +} + +const Alice,Bob,Eve,Simon: Agent; +const Ke: SessionKey; +const Te: Ticket; +const Ne: Nonce; + + +untrusted Eve; +compromised k(Eve,Simon); + + + diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl new file mode 100644 index 0000000..ef6d65a --- /dev/null +++ b/spdl/SPORE/yahalom-ban.spdl @@ -0,0 +1,85 @@ +# BAN simplified version of Yahalom +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/yahalomBAN.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +secret k : Function; + +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol yahalom-BAN^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,Ni, + R,Nr,{I,Ni}k(R,S), + Nr,{R,Kir,Ni}k(I,S), + {I,Kir,Nr}k(R,S), + {Nr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + + + +protocol yahalom-BAN(I,R,S) +{ + role I + { + const 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 + { + const 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 + { + const 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/spdl/SPORE/yahalom-lowe.spdl b/spdl/SPORE/yahalom-lowe.spdl new file mode 100644 index 0000000..176c00f --- /dev/null +++ b/spdl/SPORE/yahalom-lowe.spdl @@ -0,0 +1,56 @@ +# Lowe's modified version of Yahalom +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/yahalomLowe.html +# +# + +secret k : Function; + +usertype SessionKey; + + +protocol yahalom-Lowe(I,R,S) +{ + role I + { + const 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 + { + const 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 + { + const 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/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl new file mode 100644 index 0000000..e902ed9 --- /dev/null +++ b/spdl/SPORE/yahalom-paulson.spdl @@ -0,0 +1,84 @@ +# Paulson's strengthened version of Yahalom +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/yahalomPaulson.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +secret k : Function; +const Fresh: Function; +const Compromised: Function; + +usertype SessionKey; + +protocol yahalom-Paulson^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,Ni, + R,Nr,{I,Ni}k(R,S), + Nr,{R,Kir,Ni}k(I,S), + {I,R,Kir,Nr}k(R,S), + {Nr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + + +protocol yahalom-Paulson(I,R,S) +{ + role I + { + const 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 + { + const 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,R, Kir, Nr}k(R,S) , {Nr}Kir ); + + claim_R1(R, Secret,Kir); + claim_R2(R, Nisynch); + claim_R3(R, Empty, (Fresh,Kir)); + } + + role S + { + const 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,R,Kir,Nr}k(R,S) ); + } +} + +const Alice,Bob,Simon : Agent; + diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl new file mode 100644 index 0000000..57240d4 --- /dev/null +++ b/spdl/SPORE/yahalom.spdl @@ -0,0 +1,84 @@ +# Yahalom +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/yahalom.html +# +# Note: +# This protocol uses a ticket so scyther will only be able to verify +# the protocol using the ARACHNE engine (-a) +# + +secret k : Function; + +usertype SessionKey; +const Fresh: Function; +const Compromised: Function; + +protocol yahalom^KeyCompromise(C) +{ + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { + const Ni,Nr: Nonce; + const Kir: SessionKey; + var I,R,S: Agent; + + read_C1(C,C, I,R,S); + send_C2(C,C, I,Ni, + R,{I,Ni,Nr}k(R,S), + {R,Kir,Ni,Nr}k(I,S), + {I,Kir}k(R,S), + {Nr}Kir, + Kir + ); + claim_C3(C,Empty, (Compromised,Kir)); + } +} + + +protocol yahalom(I,R,S) +{ + role I + { + const 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); + claim_I2(I, Nisynch); + claim_I3(I, Empty, (Fresh,Kir)); + } + + role R + { + const 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); + claim_R2(R, Nisynch); + claim_R3(R, Empty, (Fresh,Kir)); + } + + role S + { + const 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) ); + } +} + +const Alice,Bob,Simon : Agent; +