diff --git a/spdl/denning-sacco-shared.spdl b/spdl/denning-sacco-shared.spdl index ceb7422..4ace1c8 100644 --- a/spdl/denning-sacco-shared.spdl +++ b/spdl/denning-sacco-shared.spdl @@ -32,7 +32,7 @@ compromised k(e,b); compromised k(a,e); compromised k(b,e); -protocol denningsaccoshared(A,S,B) +protocol denningsaccosh(A,S,B) { role A { diff --git a/spdl/yahalom.spdl b/spdl/yahalom.spdl index 33aca1e..65313f0 100644 --- a/spdl/yahalom.spdl +++ b/spdl/yahalom.spdl @@ -16,6 +16,7 @@ protocol yahalom(A,B,S) send_1(A,B, A,na); read_3(S,A, nb, {B,kab,na,nb}k(A,S), ticket ); send_4(A,B, ticket, {nb}kab ); + claim_5(A, Secret,kab); } @@ -29,6 +30,7 @@ protocol yahalom(A,B,S) read_1(A,B, A,na); send_2(B,S, B,nb, {A,na,nb}k(B,S) ); read_4(A,B, {A,kab}k(B,S) , {nb}kab ); + claim_6(B, Secret,kab); }