From 500710519e7a65546ec237a7125728900767289a Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 10 Sep 2004 07:46:00 +0000 Subject: [PATCH] - Added protocols for Bertinoro VODCA talk. --- spdl/soph-keyexch.spdl | 39 +++++++++++++++++++++++++++++++++++++++ spdl/soph.spdl | 34 ++++++++++++++++++++++++++++++++++ 2 files changed, 73 insertions(+) create mode 100644 spdl/soph-keyexch.spdl create mode 100644 spdl/soph.spdl diff --git a/spdl/soph-keyexch.spdl b/spdl/soph-keyexch.spdl new file mode 100644 index 0000000..611ba09 --- /dev/null +++ b/spdl/soph-keyexch.spdl @@ -0,0 +1,39 @@ +usertype Sessionkey; +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol sophkx(I,R) +{ + role I + { + const ni: Nonce; + const kir: Sessionkey; + var nr: Nonce; + + send_1(I,R, ni, {I,kir}pk(R) ); + read_2(R,I, {ni}kir ); + claim_4(I,Secret,kir); + } + + role R + { + var ni: Nonce; + var kir: Sessionkey; + const nr: Nonce; + + read_1(I,R, ni, {I,kir}pk(R) ); + send_2(R,I, {ni}kir ); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const nc: Nonce; +const ke: Sessionkey; +compromised sk(Eve); + +run sophkx.I(Agent,Agent); +run sophkx.R(Agent,Agent); +run sophkx.I(Agent,Agent); diff --git a/spdl/soph.spdl b/spdl/soph.spdl new file mode 100644 index 0000000..905dc61 --- /dev/null +++ b/spdl/soph.spdl @@ -0,0 +1,34 @@ +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +protocol soph(I,R) +{ + role I + { + const ni: Nonce; + + send_1(I,R, {I,ni}pk(R) ); + read_2(R,I, ni ); + claim_4(I,Niagree); + } + + role R + { + var ni: Nonce; + + read_1(I,R, {I,ni}pk(R) ); + send_2(R,I, ni ); + } +} + +const Alice,Bob,Eve: Agent; + +untrusted Eve; +const nc: Nonce; +compromised sk(Eve); + +run soph.I(Agent,Agent); +run soph.R(Agent,Agent); +run soph.I(Agent,Agent); +run soph.R(Agent,Agent);