64 lines
1.3 KiB
Plaintext
64 lines
1.3 KiB
Plaintext
(* Channel *)
|
|
free c.
|
|
|
|
free error1,error2,GetC.
|
|
|
|
fun vk/1.
|
|
fun sign/2.
|
|
reduc checksign(sign(m,k),vk(k))=m.
|
|
reduc getmess(sign(m,k))=m.
|
|
|
|
fun senc/2.
|
|
reduc sdec(senc(m,k),k)=m.
|
|
|
|
let passport =
|
|
in(d,(ke,km));
|
|
in(c,=GetC);
|
|
new nt;
|
|
out(c,nt);
|
|
in(c,cert);
|
|
let x=checksign(cert,vk(km)) in
|
|
let (nr,=nt,kr)=sdec(x,ke) in
|
|
new kt;
|
|
out(c,sign(senc((nt,nr,kt),ke),km))
|
|
else
|
|
out(c,error2)
|
|
else
|
|
out(c,error1);
|
|
0.
|
|
|
|
|
|
let reader =
|
|
in(d,(ke,km));
|
|
out(c,GetC);
|
|
in(c,nt);
|
|
new nr;
|
|
new kr;
|
|
out(c,sign(senc((nr,nt,kr),ke),km));
|
|
in(c,cert);
|
|
let x=checksign(cert,vk(km)) in
|
|
let (=nt,=nr,kt)=sdec(x,ke) in
|
|
0.
|
|
|
|
|
|
process
|
|
new ke1;
|
|
new km1;
|
|
new ke2;
|
|
new km2;
|
|
new d;
|
|
(
|
|
! reader (* Start the reader *)
|
|
| out(d,(ke1,km1)) (* Send out first key pair *)
|
|
| out(d,(ke2,km2)) (* Send out second key pair *)
|
|
| passport (* Start first passport *)
|
|
| passport (* Start second passport *)
|
|
(* Attacker records the signatures sent by reader *)
|
|
| phase 1;
|
|
(
|
|
(* Start process again with either first or second key pair *)
|
|
passport
|
|
| out(d,choice[(ke1,km1),(ke2,km2)])
|
|
)
|
|
)
|