66 lines
1.3 KiB
Plaintext
66 lines
1.3 KiB
Plaintext
(* Honest participants *)
|
|
free C,S.
|
|
|
|
(* Channel *)
|
|
free c.
|
|
|
|
free hello,ack.
|
|
|
|
(* Shared secret between C and S *)
|
|
private free m.
|
|
(* Secret signing key of CA *)
|
|
private free dkCA.
|
|
|
|
fun vk/1.
|
|
fun ek/1.
|
|
fun h/1.
|
|
|
|
fun sign/2.
|
|
reduc checksign(sign(m,k),vk(k)) = m.
|
|
reduc getmess(sign(m,k)) = m.
|
|
|
|
fun aenc/2.
|
|
reduc adec(aenc(m,ek(k)),k) = m.
|
|
|
|
fun senc/2.
|
|
reduc sdec(senc(m,k),k) = m.
|
|
|
|
query ev:endServerAuth(x,y) ==> ev:beginServerAuth(x,y).
|
|
query ev:endClientAuth(x,y,z) ==> ev:beginClientAuth(x,y,z).
|
|
|
|
let client =
|
|
in(d,(idC,idS));
|
|
new nC;
|
|
out(c,(hello,nC));
|
|
in(c,(=hello,nS));
|
|
in(c,(cert,=vk(dkCA)));
|
|
let (=idS,ekS)=checksign(cert,vk(dkCA)) in
|
|
new secret;
|
|
out(c,aenc(secret,ekS));
|
|
event beginClientAuth(nC,nS,secret);
|
|
let k=h((secret,nC,nS)) in
|
|
out(c,senc((m),k));
|
|
in(c,x);
|
|
let (=ack)=sdec(x,k) in
|
|
event endServerAuth(nC,nS).
|
|
|
|
let server =
|
|
in(d,(idC,idS));
|
|
new dkS;
|
|
in(c,(=hello,nC));
|
|
new nS;
|
|
event beginServerAuth(nC,nS);
|
|
out(c,(hello,nS));
|
|
out(c,(sign((idS,ek(dkS)),dkCA),vk(dkCA)));
|
|
in(c,x);
|
|
let secret=adec(x,dkS) in
|
|
let k=h((secret,nC,nS)) in
|
|
in(c,y);
|
|
let (=m)=sdec(y,k) in
|
|
event endClientAuth(nC,nS,secret);
|
|
out(c,senc((ack),k)).
|
|
|
|
process
|
|
new d;
|
|
! (out(d,(C,S)) | client | server)
|