(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2021 - Inria
 * Copyright (c) - 2012--2021 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

(* One-Way Trapdoor Permutations *)
require import Core Distr.

(** Abstract declarations to be refined when instantiating *)
(* Domain and Range *)
type D, R.

(* Keys *)
type pkey, skey.

op dkeys: (pkey * skey) distr.
axiom dkeys_ll: is_lossless dkeys.

pred valid_keys (ks:pkey * skey) = support dkeys ks.
pred valid_pkey (pk:pkey) = exists sk, valid_keys (pk,sk).
pred valid_skey (sk:skey) = exists pk, valid_keys (pk,sk).

(* The distribution from which the challenge is sampled *)
(* Note: We use its support as the permutation's domain! *)
op challenge: pkey -> D distr.

axiom challenge_ll pk:
  valid_pkey pk => is_lossless (challenge pk).

axiom challenge_uni pk:
  valid_pkey pk => is_uniform (challenge pk).

(** Concrete definitions *)
op f: pkey -> D -> R.

pred f_dom (pk:pkey) (x:D) =
  valid_pkey pk => x \in (challenge pk).

pred f_rng (pk:pkey) (y:R) =
  valid_pkey pk => exists x, f_dom pk x /\ y = f pk x.

op finv: skey -> R -> D.

axiom finv_correct (pk:pkey) (sk:skey) y:
  valid_keys (pk,sk) =>
  f_rng pk y =>
  f_dom pk (finv sk y).

axiom finvof (pk:pkey) (sk:skey) (x:D):
  valid_keys (pk,sk) =>
  f_dom pk x =>
  finv sk (f pk x) = x.

axiom fofinv (pk:pkey) (sk:skey) (x:R):
  valid_keys (pk,sk) =>
  f_rng pk x =>
  f pk (finv sk x) = x.

(* This is often useful to extract plaintexts *)
lemma f_pk_inj (x, y:D) (pk:pkey) (sk:skey):
  valid_keys (pk,sk) =>
  f_dom pk x => f_dom pk y =>
  f pk x = f pk y => x = y.
proof.
by move=> Hsupp Hdom_x Hdom_y Heqf;
   rewrite -(finvof pk sk) // -(finvof pk sk y) // Heqf.
qed.

(** We can now define the module types and modules that define security **)
module type Inverter = {
  proc invert(pk : pkey, y : R) : D
}.

module OW(I :Inverter) ={
  proc main(): bool ={
    var x,x':D;
    var pk:pkey;
    var sk:skey;

    (pk,sk) <$ dkeys;
    x       <$ challenge pk;
    x'      <@ I.invert(pk,f pk x);
    return (x = x');
  }
}.