(* Channel *)
free d.

fun commit/4.
fun open/3.

equation open(commit(m1,m2,m3,k),m1,k) = m1.
equation open(commit(m1,m2,m3,k),m2,k) = m2.
equation open(commit(m1,m2,m3,k),m3,k) = 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 k;
    phase 1;
    out(d,commit(m1,m2,m3,k));
    phase 2;
    out(d,(m2,k)).

let server =
    phase 1;
    in(d,x);
    phase 2;
    in(d,(m2,k));
    let (=m2)=(open(x,m2,k)) in 0.

process
    alice | server