38 lines
711 B
Plaintext
38 lines
711 B
Plaintext
(* Honest participants *)
|
|
free C,S.
|
|
|
|
(* Channel *)
|
|
free c.
|
|
|
|
fun h/1.
|
|
|
|
free hello, success.
|
|
|
|
(* Secret key shared by C and S *)
|
|
private free kCS.
|
|
|
|
(* Non-injective agreement *)
|
|
query ev:end(id1,id2,n) ==> ev:begin(id1,id2,n).
|
|
|
|
(* Injective agreement *)
|
|
query evinj:end(id1,id2,n) ==> evinj:begin(id1,id2,n).
|
|
|
|
let initiator =
|
|
in(d,(idI,idR));
|
|
new nonce;
|
|
out(c,(hello,nonce));
|
|
in(c,(=idR,=h((nonce,kCS,idI))));
|
|
event end(idR,idI,nonce);
|
|
out(c,success).
|
|
|
|
let responder =
|
|
in(d,(idI,idR));
|
|
in(c,(=hello,nonce));
|
|
event begin(idR,idI,nonce);
|
|
out(c,(idR,h((nonce,kCS,idI))));
|
|
in(c,=success).
|
|
|
|
process
|
|
new d;
|
|
! initiator | ! responder | ! out(d,(S,C)) | ! out(d,(C,S))
|