From cbb617b3a1171e1058316ff2a1f9a6d986d69046 Mon Sep 17 00:00:00 2001 From: gijs Date: Wed, 18 May 2005 11:43:42 +0000 Subject: [PATCH] - Adding CJ modified version of splice protocol - Adding tmn - Fixed a modelling error in splice --- spdl/SPORE/splice-as-cj.spdl | 83 ++++++++++++++++++++++++++++++++++++ spdl/SPORE/splice-as-hc.spdl | 16 ++++--- spdl/SPORE/splice-as.spdl | 12 +++++- spdl/SPORE/tmn.spdl | 65 ++++++++++++++++++++++++++++ 4 files changed, 168 insertions(+), 8 deletions(-) create mode 100644 spdl/SPORE/splice-as-cj.spdl create mode 100644 spdl/SPORE/tmn.spdl diff --git a/spdl/SPORE/splice-as-cj.spdl b/spdl/SPORE/splice-as-cj.spdl new file mode 100644 index 0000000..a7be252 --- /dev/null +++ b/spdl/SPORE/splice-as-cj.spdl @@ -0,0 +1,83 @@ +# 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 spliceASCJ(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); + +run spliceASCJI(Agent,Agent,Agent); +run spliceASCJR(Agent,Agent,Agent); +run spliceASCJS(Agent,Agent,Agent); + +#run spliceASCJ.I(Alice,Bob,Simon); +#run spliceASCJ.R(Alice,Bob,Simon); +#run spliceASCJ.S(Alice,Bob,Simon); + diff --git a/spdl/SPORE/splice-as-hc.spdl b/spdl/SPORE/splice-as-hc.spdl index 2581d72..931132b 100644 --- a/spdl/SPORE/splice-as-hc.spdl +++ b/spdl/SPORE/splice-as-hc.spdl @@ -13,7 +13,7 @@ inversekeys (pk,sk); const inc,dec: Function; inversekeys (inc,dec); -protocol spliceAS(I,R,S) +protocol spliceASHC(I,R,S) { role I { @@ -23,7 +23,7 @@ protocol spliceAS(I,R,S) 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(R) ); + 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); @@ -62,14 +62,18 @@ protocol spliceAS(I,R,S) } } -const Al,Bo,Eve: Agent; +const Alice,Bob,Simon,Eve: Agent; untrusted Eve; const ne: Nonce; compromised sk(Eve); -run spliceAS.I(Agent,Agent,Agent); -run spliceAS.R(Agent,Agent,Agent); -run spliceAS.S(Agent,Agent,Agent); +#run spliceASHC.I(Alice,Bob,Simon); +#run spliceASHC.R(Alice,Bob,Simon); +#run spliceASHC.S(Alice,Bob,Simon); + +run spliceASHC.I(Agent,Agent,Agent); +run spliceASHC.R(Agent,Agent,Agent); +run spliceASHC.S(Agent,Agent,Agent); diff --git a/spdl/SPORE/splice-as.spdl b/spdl/SPORE/splice-as.spdl index 9dad516..6952245 100644 --- a/spdl/SPORE/splice-as.spdl +++ b/spdl/SPORE/splice-as.spdl @@ -3,6 +3,11 @@ # 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; @@ -23,7 +28,7 @@ protocol spliceAS(I,R,S) 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(R) ); + 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); @@ -62,7 +67,7 @@ protocol spliceAS(I,R,S) } } -const Al,Bo,Eve: Agent; +const Alice,Bob,Simon,Eve: Agent; untrusted Eve; const ne: Nonce; @@ -72,4 +77,7 @@ run spliceAS.I(Agent,Agent,Agent); run spliceAS.R(Agent,Agent,Agent); run spliceAS.S(Agent,Agent,Agent); +#run spliceAS.I(Alice,Bob,Simon); +#run spliceAS.R(Alice,Bob,Simon); +#run spliceAS.S(Alice,Bob,Simon); diff --git a/spdl/SPORE/tmn.spdl b/spdl/SPORE/tmn.spdl new file mode 100644 index 0000000..173abca --- /dev/null +++ b/spdl/SPORE/tmn.spdl @@ -0,0 +1,65 @@ +# TMN +# +# Modelled after the description in the SPORE library +# http://www.lsv.ens-cachan.fr/spore/tmn.html +# + +usertype Key; + +const pk: Function; +secret sk: Function; +inversekeys(pk,sk); + +protocol tmn(I,R,S) +{ + role I + { + const Ki: Key; + var Kr: Key; + + send_1(I,S, R,{Ki}pk(S) ); + read_4(S,I, R,{Kr}Ki ); + + claim_I1(I,Secret,Ki); + claim_I2(I,Secret,Kr); + } + + role R + { + const Kr: Key; + + read_2(S,R, I ); + send_3(R,S, I, { Kr }pk(S) ); + + claim_R1(R,Secret,Kr); + } + + role S + { + var Ki,Kr: Key; + + 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: Key; + + +untrusted Eve; +compromised sk(Eve); + +# Scenario to recreate an attack in SPORE +#run tmn.I (Alice,Bob,Simon); +#run tmn.R (Alice,Bob,Simon); +#run tmn.S (Alice,Bob,Simon); + +run tmn.I (Agent,Agent,Simon); +run tmn.R (Agent,Agent,Simon); +run tmn.S (Agent,Agent,Simon); + + +