40 lines
641 B
Plaintext
40 lines
641 B
Plaintext
(* Channel *)
|
|
free d.
|
|
|
|
fun commit/6.
|
|
fun open/3.
|
|
|
|
equation open(commit(m1,m2,m3,k1,k2,k3),m1,k1) = m1.
|
|
equation open(commit(m1,m2,m3,k1,k2,k3),m2,k2) = m2.
|
|
equation open(commit(m1,m2,m3,k1,k2,k3),m3,k3) = m3.
|
|
|
|
private free m1,m2,m3.
|
|
|
|
query attacker:m1 phase 1.
|
|
query attacker:m3 phase 1.
|
|
|
|
query attacker:m1 phase 2.
|
|
query attacker:m3 phase 2.
|
|
|
|
noninterf m1.
|
|
noninterf m3.
|
|
|
|
let alice =
|
|
new k1;
|
|
new k2;
|
|
new k3;
|
|
phase 1;
|
|
out(d,commit(m1,m2,m3,k1,k2,k3));
|
|
phase 2;
|
|
out(d,(m2,k2)).
|
|
|
|
let server =
|
|
phase 1;
|
|
in(d,x);
|
|
phase 2;
|
|
in(d,(m2,k2));
|
|
let (=m2)=(open(x,m2,k2)) in 0.
|
|
|
|
process
|
|
alice | server
|