From 96ade10f29a393532421d9d495da6859d35a6f34 Mon Sep 17 00:00:00 2001 From: ccremers Date: Thu, 18 Nov 2004 14:47:53 +0000 Subject: [PATCH] - Cleanup. --- spdl/bke-synch.spdl | 62 --------------------------------------------- 1 file changed, 62 deletions(-) delete mode 100644 spdl/bke-synch.spdl diff --git a/spdl/bke-synch.spdl b/spdl/bke-synch.spdl deleted file mode 100644 index 0981f8b..0000000 --- a/spdl/bke-synch.spdl +++ /dev/null @@ -1,62 +0,0 @@ -/* - Bilateral Key Exchange with Public Key protocol (BKEPK) -*/ - -usertype Key; - -const pk,hash: Function; -secret sk,unhash: Function; - -inversekeys (pk,sk); -inversekeys (hash,unhash); - -protocol bkepk(I,R) -{ - role I - { - const ni: Nonce; - var nr: Nonce; - var kir: Key; - - send_1 (I,R, { ni,I }pk(R) ); - read_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); - send_3 (I,R, { hash(nr) }kir ); - claim_4 (I, Secret, kir ); - claim_6 (I, Nisynch ); - claim_8 (I, Niagree ); - } - - role R - { - var ni: Nonce; - const nr: Nonce; - const kir: Key; - - read_1 (I,R, { ni,I }pk(R) ); - send_2 (R,I, { hash(ni),nr,R,kir }pk(I) ); - read_3 (I,R, { hash(nr) }kir ); - claim_5 (R, Secret, kir ); - claim_7 (R, Nisynch ); - claim_9 (R, Niagree ); - } -} - -const a,b,e: Agent; - -untrusted e; -compromised sk(e); -const ne: Nonce; - -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); - -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); - -run bkepk.I(a,Agent); -run bkepk.R(Agent,b); -