diff --git a/spdl/SPORE/ccitt509-3.spdl b/spdl/SPORE/ccitt509-3.spdl new file mode 100644 index 0000000..c42bba0 --- /dev/null +++ b/spdl/SPORE/ccitt509-3.spdl @@ -0,0 +1,62 @@ +# 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 ccitt5093(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_4(I,Nisynch); + } + + 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_5(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); + +# This scenario should find the attack described in SPORE +# run ccitt5093.I(Alice,Bob); +# run ccitt5093.I(Alice,Eve); +# run ccitt5093.R(Alice,Bob); + +# General scenario, 2 parallel runs of the protocol + +run ccitt5093.I(Agent,Agent); +run ccitt5093.R(Agent,Agent); +run ccitt5093.I(Agent,Agent); +run ccitt5093.R(Agent,Agent); diff --git a/spdl/SPORE/ccitt509-ban3.spdl b/spdl/SPORE/ccitt509-ban3.spdl new file mode 100644 index 0000000..d01a089 --- /dev/null +++ b/spdl/SPORE/ccitt509-ban3.spdl @@ -0,0 +1,55 @@ +# 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 ccitt509ban3(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); + +# General scenario, 2 parallel runs of the protocol + +run ccitt509ban3.I(Agent,Agent); +run ccitt509ban3.R(Agent,Agent); +run ccitt509ban3.I(Agent,Agent); +run ccitt509ban3.R(Agent,Agent);