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

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

(* Type declarations.  D represents range and domain of the one-way
permutation f. [fixed] means that it is possible to uniformly pick
random values of this type *)
type D [fixed].

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

(* Function declarations. Both f and g are functions from D to D. *)
fun f(D):D.
fun g(D):D.

(* Injectivity of f. *)
forall x:D, x':D; (f(x)=f(x')) = (x=x').

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

(* One-wayness of f *)
equiv
!n new x: D; (() -> f(x), (x':D) -> x=x')
<=(negl)=>
!n new x: D; (() -> f(x), (x':D) -> false).

(* Definition of g *)
forall x:D; g(x) = f(f(x)).

query event bad ==> false.

(* One-wayness game for g *)
process
        in(start,());
        new x : D;
        out(adv,g(x));
        in(adv,x':D);
        if g(x)=g(x') then event bad