(* Channel names need to be declared. *)
channel start,adv.

(* Events need to be declared *)
event bad.

(* Type declarations. [fixed] means that it is possible to uniformly
pick random values of this type *)
type D [fixed].
type T [fixed].

(* Parameters. Needed for replications (!n) *)
param n.

(* Function declaration. Example: f takes one argument of type D and
returns a value of type T. g takes two arguments of type T and returns
a value of type T. *)
fun f(D):T.
fun g(T,T):T.

(* Some user-defined equation that we claim to hold *)
forall x:D, x':D; g(g(f(x),f(x)),g(f(x'),f(x'))) = g(f(x),f(x')).

(* Declaration of a negligible probability *)
proba negl.

(* Some crypto assumption *)
equiv
!n new x: T; (() -> x, (x':T) -> g(x,x'))
<=(negl)=>
!n new x: D; (() -> f(x), (x':T) -> g(f(x),x')).

query event bad ==> false.

process
        in(start,());
        new x : D;
        let y = f(x) in
        out(adv,g(y,y));
        in(adv,x':T);
        if g(f(x),x')=g(x',x') then event bad