(* Channel *)
free d.

(* secret message *)
private free m.

fun commit/2.
fun open/3.

equation open(commit(m,k),m,k) = m.

query attacker:m phase 1.

noninterf m.

let alice =
    phase 1;
    new k;
    out(d,commit(m,k)).

let server =
    phase 1;
    in(d,x).

process
    alice | server