param N. (* maximum number of executions *)

type key [large, fixed].

channel c,d.

set autoMove = false. (* Prevent an automatic transformation of the game.
    	       	      	 We want to prove secrecy directly on the given game. *)

query secret x.


process
! i <= N
in(c, ());
new k: key;
out(c, ());
in(d, compr: bool);
if compr then
   out(d, k)
else
   let x:key = k in
   out(d, ())