From 0b22c4a4bbde37dfba9f8b8050f1954a7b794aa1 Mon Sep 17 00:00:00 2001 From: gijs Date: Fri, 29 Apr 2005 10:50:53 +0000 Subject: [PATCH] - Created a directory to hold spdl files of all protocols in SPORE - Import Andrew secure RPC and derived protocols --- spdl/SPORE/andrew-ban-concrete.spdl | 70 ++++++++++++++++++++++++++++ spdl/SPORE/andrew-ban.spdl | 66 ++++++++++++++++++++++++++ spdl/SPORE/andrew-lowe-ban.spdl | 71 ++++++++++++++++++++++++++++ spdl/SPORE/andrew.spdl | 72 +++++++++++++++++++++++++++++ 4 files changed, 279 insertions(+) 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 diff --git a/spdl/SPORE/andrew-ban-concrete.spdl b/spdl/SPORE/andrew-ban-concrete.spdl new file mode 100644 index 0000000..059f917 --- /dev/null +++ b/spdl/SPORE/andrew-ban-concrete.spdl @@ -0,0 +1,70 @@ +# 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) +# So it is possile that certain attacks that use this property are not found +# +# Note: +# The attack mentioned in SPORE is not found because of the property in the +# previous note +# +# 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; + +protocol andrewConcrete(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_4(I,Secret,kir); + claim_5(I,Nisynch); + 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_7(R,Secret,kir); + claim_8(R,Nisynch); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const kee: SessionKey; + +# This scenario should find the attack in SPORE +# run andrewConcrete.I(Alice,Bob); +# run andrewConcrete.R(Bob,Alice); + +# This is the original scenario +run andrewConcrete.I(Agent,Agent); +run andrewConcrete.R(Agent,Agent); +run andrewConcrete.I(Agent,Agent); +run andrewConcrete.R(Agent,Agent); diff --git a/spdl/SPORE/andrew-ban.spdl b/spdl/SPORE/andrew-ban.spdl new file mode 100644 index 0000000..1aa9b8b --- /dev/null +++ b/spdl/SPORE/andrew-ban.spdl @@ -0,0 +1,66 @@ +# 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; + +protocol andrewBan(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_5(I,Nisynch); + claim_5b(I,Niagree); + claim_6(I,Secret, kir); + claim_7(I,Secret, k(I,R)); + } + + 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_8(R,Nisynch); + claim_8b(R,Niagree); + claim_9(R,Secret, kir); + claim_10(R,Secret, k(I,R)); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const ne: Nonce; +const kee: SessionKey; +compromised k(Eve,Eve); +compromised k(Eve,Alice); +compromised k(Eve,Bob); +compromised k(Alice,Eve); +compromised k(Bob,Eve); + +run andrewBan.I(Agent,Agent); +run andrewBan.R(Agent,Agent); +run andrewBan.I(Agent,Agent); +run andrewBan.R(Agent,Agent); diff --git a/spdl/SPORE/andrew-lowe-ban.spdl b/spdl/SPORE/andrew-lowe-ban.spdl new file mode 100644 index 0000000..6693afb --- /dev/null +++ b/spdl/SPORE/andrew-lowe-ban.spdl @@ -0,0 +1,71 @@ +# 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; + +protocol andrewLoweBan(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_5(I,Nisynch); + claim_6(I,Secret, 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_8(R,Nisynch); + claim_9(R,Secret, 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); + + + +run andrewLoweBan.I(Agent,Agent); +run andrewLoweBan.R(Agent,Agent); +run andrewLoweBan.I(Agent,Agent); +run andrewLoweBan.R(Agent,Agent); diff --git a/spdl/SPORE/andrew.spdl b/spdl/SPORE/andrew.spdl new file mode 100644 index 0000000..ae53219 --- /dev/null +++ b/spdl/SPORE/andrew.spdl @@ -0,0 +1,72 @@ +# 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; + +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_5(I,Secret,kir); + claim_6(I,Nisynch); + } + + 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_7(R,Secret,kir); + claim_8(R,Nisynch); + } +} + +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); + + + +# This scenario should recreate the first attack in SPORE when running +# scyther in model checker mode +#run andrew.I(Alice,Bob); +#run andrew.R(Alice,Bob); +#run andrew.I(Alice,Bob); +#run andrew.R(Alice,Bob); + +# General scenario, 2 parallel runs of the protocol + +run andrew.I(Agent,Agent); +run andrew.R(Agent,Agent); +run andrew.I(Agent,Agent); +run andrew.R(Agent,Agent);