(* 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