diff --git a/spdl/bke.spdl b/spdl/bke.spdl index fbf256a..027e414 100644 --- a/spdl/bke.spdl +++ b/spdl/bke.spdl @@ -22,6 +22,7 @@ protocol bkepk(I,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 ); } role R @@ -34,6 +35,7 @@ protocol bkepk(I,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 ); } }