From 9a86e80c96a03ca0a747d1c3a808b5d32d8bf0d7 Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 14 Jan 2005 18:22:22 +0000 Subject: [PATCH] - Added some type information to the Yahalom protocol model. --- spdl/yahalom.spdl | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/spdl/yahalom.spdl b/spdl/yahalom.spdl index 65313f0..5b62b62 100644 --- a/spdl/yahalom.spdl +++ b/spdl/yahalom.spdl @@ -3,15 +3,17 @@ const a,b,s : Agent; secret k : Function; +usertype Nonce, Ticket, SessionKey; + protocol yahalom(A,B,S) { role A { - const na; - var nb; - var ticket; - var kab; + const na: Nonce; + var nb: Nonce; + var ticket: Ticket; + var kab: SessionKey; send_1(A,B, A,na); read_3(S,A, nb, {B,kab,na,nb}k(A,S), ticket ); @@ -22,10 +24,10 @@ protocol yahalom(A,B,S) role B { - const nb; - var na; - var ticket; - var kab; + const nb: Nonce; + var na: Nonce; + var ticket: Ticket; + var kab: SessionKey; read_1(A,B, A,na); send_2(B,S, B,nb, {A,na,nb}k(B,S) ); @@ -36,8 +38,8 @@ protocol yahalom(A,B,S) role S { - const kab; - var na,nb; + const kab: SessionKey; + var na,nb: Nonce; read_2(B,S, B,nb, {A,na}k(B,S) ); send_3(S,A, nb, {B,kab,na,nb}k(A,S), {A,kab}k(B,S) );