From f8a91d744d1515a3a898ffc7d28138d397153976 Mon Sep 17 00:00:00 2001 From: gijs Date: Wed, 15 Jun 2005 09:17:15 +0000 Subject: [PATCH] Little tweak to the key compromise modelling, model key compromise agent as a responder instead of an initiator, remove empty roles from key compromise protocol. --- .../key-compromise/needham-schroeder-sk.spdl | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl b/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl index 81a6974..b61f053 100644 --- a/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl +++ b/spdl/SPORE/key-compromise/needham-schroeder-sk.spdl @@ -16,15 +16,17 @@ const dec,inc: Function; inversekeys(dec,inc); usertype SessionKey; -protocol needhamschroederSessionKeyCompromise(I,R,S) +protocol needhamschroederSessionKeyCompromise(C) { - // Disclose an entire session and the corresponding session key - // to simulate key compromise - role I { + // Read the names of 3 agents and disclose a session between them including + // corresponding session key to simulate key compromise + role C { const Ni,Nr: Nonce; const Kir: SessionKey; + var I,R,S: Agent; - send_D1(I,I, (I,R,Ni), + read_C1(C,C, I,R,S); + send_C2(C,C, (I,R,Ni), {Ni,R,Kir,{Kir,I}k(R,S)}k(I,S), {Kir,I}k(R,S), {Nr}Kir, @@ -32,13 +34,8 @@ protocol needhamschroederSessionKeyCompromise(I,R,S) Kir ); } - - role R { - } - - role S { - } } + protocol needhamschroedersk(I,R,S) { role I