From ef34e0080e03ad7e5215f5f5961d3ef4e0b54ccd Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 6 Oct 2004 09:10:04 +0000 Subject: [PATCH] - Counterexample for Bart's logic. --- spdl/samasc-broken.spdl | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 spdl/samasc-broken.spdl diff --git a/spdl/samasc-broken.spdl b/spdl/samasc-broken.spdl new file mode 100644 index 0000000..755e1fb --- /dev/null +++ b/spdl/samasc-broken.spdl @@ -0,0 +1,36 @@ +/* + Samasc broken +*/ + +usertype Key; + +const pk: Function; +secret sk: Function; + +inversekeys (pk,sk); + +protocol bkepk(I,R) +{ + role R + { + const nr: Nonce; + var kir: Key; + + read_1a (I,R, { kir,I }pk(R) ); + send_1b (R,I, {nr,R}pk(I) ); + + /* Commenting out these two lines yields an attack: */ + read_2a (I,R, { nr }kir ); + send_2b (R,I, { I,R,nr }kir ); + + read_3 (I,R, { I,R }kir ); + + claim_4 (R, Secret, kir ); + } +} + +const a,b,e: Agent; + +untrusted e; +compromised sk(e); +const ne: Nonce;