From 2e4c5afeb78025ea5916c132cf96591416ce5baf Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 11 May 2005 15:18:32 +0000 Subject: [PATCH] - Added a strange issue, to be resolved tomorrow. --- spdl/problems-johanselst.spdl | 83 +++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 spdl/problems-johanselst.spdl diff --git a/spdl/problems-johanselst.spdl b/spdl/problems-johanselst.spdl new file mode 100644 index 0000000..20e23ac --- /dev/null +++ b/spdl/problems-johanselst.spdl @@ -0,0 +1,83 @@ +/* + * Some authentication protocol + * + * Version by Johan Selst. Seems to segfault at a simple -r4 execution + * with the modelchecker. + * + * Reported on 2005-05-11. + */ + +// PKI infrastructure + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +// The protocol description + +protocol as3a(X, I, Y) +{ + role X + { + var nix: Nonce; + + read_1(I, X, nix); + send_2(X, I, {I,nix}sk(X)); + } + + role I + { + const nix, niy: Nonce; + + send_1(I, X, nix); + read_2(X, I, {I,nix}sk(X)); + send_3(I, Y, niy); + read_4(Y, I, {niy,I}sk(Y)); + claim_i1(I, Nisynch); + } + + role Y + { + var niy: Nonce; + + read_3(I, Y, niy); + send_4(Y, I, {niy,I}sk(Y)); + } +} + +// The trusted agents in the system + +const Alice,Bob,Carol: Agent; + +// An untrusted agent, with leaked information + +const Eve: Agent; +untrusted Eve; +compromised sk(Eve); + +// The runs (only needed for the modelchecker algorithm) + +run as3a.X(Agent,Agent,Agent); +run as3a.I(Agent,Agent,Agent); +run as3a.Y(Agent,Agent,Agent); + +run as3a.X(Agent,Agent,Agent); +run as3a.I(Agent,Agent,Agent); +run as3a.Y(Agent,Agent,Agent); + +run as3a.X(Agent,Agent,Agent); +run as3a.I(Agent,Agent,Agent); +run as3a.Y(Agent,Agent,Agent); + +run as3a.X(Agent,Agent,Agent); +run as3a.I(Agent,Agent,Agent); +run as3a.Y(Agent,Agent,Agent); + +run as3a.X(Agent,Agent,Agent); +run as3a.I(Agent,Agent,Agent); +run as3a.Y(Agent,Agent,Agent); + +run as3a.X(Agent,Agent,Agent); +run as3a.I(Agent,Agent,Agent); +run as3a.Y(Agent,Agent,Agent); +