andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Added some type information to the Yahalom protocol model.

Browse Source
This commit is contained in:
ccremers 2005-01-14 18:22:22 +00:00
parent 820c2caed8
commit 9a86e80c96
1 changed files with 12 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
spdl/yahalom.spdl
View File

@ -3,15 +3,17 @@
const a,b,s : Agent; const a,b,s : Agent;
secret k : Function; secret k : Function;
usertype Nonce, Ticket, SessionKey;
protocol yahalom(A,B,S) protocol yahalom(A,B,S)
{ {
role A role A
{ {
const na; const na: Nonce;
var nb; var nb: Nonce;
var ticket; var ticket: Ticket;
var kab; var kab: SessionKey;
send_1(A,B, A,na); send_1(A,B, A,na);
read_3(S,A, nb, {B,kab,na,nb}k(A,S), ticket ); read_3(S,A, nb, {B,kab,na,nb}k(A,S), ticket );
@ -22,10 +24,10 @@ protocol yahalom(A,B,S)
role B role B
{ {
const nb; const nb: Nonce;
var na; var na: Nonce;
var ticket; var ticket: Ticket;
var kab; var kab: SessionKey;
read_1(A,B, A,na); read_1(A,B, A,na);
send_2(B,S, B,nb, {A,na,nb}k(B,S) ); send_2(B,S, B,nb, {A,na,nb}k(B,S) );
@ -36,8 +38,8 @@ protocol yahalom(A,B,S)
role S role S
{ {
const kab; const kab: SessionKey;
var na,nb; var na,nb: Nonce;
read_2(B,S, B,nb, {A,na}k(B,S) ); 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) ); send_3(S,A, nb, {B,kab,na,nb}k(A,S), {A,kab}k(B,S) );