(* --------------------------------------------------------------------
 * Copyright (c) - 2012-2015 - IMDEA Software Institute and INRIA
 * Distributed under the terms of the CeCILL-B licence.
 * -------------------------------------------------------------------- *)

(*** A formalization of pseudo-random functions **)
require import Int Real Distr FSet FMap.

(** A PRF is a family of functions F from domain D to finite range R
    indexed by a keyspace K equipped with a distribution dK. *)
type D.

type R.

type K.

op dK: K distr.
axiom dK_ll: is_lossless dK.

op F:K -> D -> R.

module type PRF = {
  proc keygen()   : K
  proc f(k:K,x:D) : R
}.

(** The Real PRF is defined as follows *)
module PRFr = {
  proc keygen(): K = {
    var k;

    k <$ dK;
    return k;
  }

  proc f(k:K,x:D): R = { return F k x; }
}.

(** PRF-security is expressed as indistinguishability from a truly
    random function (defined by some distribution dR) when the key is
    sampled from dK **)
op dR:R distr.
axiom dR_ll: is_lossless dR.

module type PRF_Oracles = {
  proc f(x:D): R
}.

module type Distinguisher(F:PRF_Oracles) = {
  proc distinguish(): bool
}.

module type PRF_Hiding = {
  proc init(): unit
  proc f(x:D): R
}.

module PRF_Wrap (F:PRF) = {
  var k:K

  proc init(): unit = { k <$ dK; }
  proc f(x:D): R    = { return F k x; }
}.

module IND (F:PRF_Hiding,D:Distinguisher) = {
  module D = D(F)

  proc main(): bool = {
    var b;

    F.init();
    b = D.distinguish();
    return b;
  }
}.

module PRFi = {
  var m:(D,R) map

  proc init(): unit = { m = FMap.empty; }

  proc f (x:D): R = {
    if (!mem x (dom m)) m.[x] = $dR;
    return (oget m.[x]);
  }
}.

(* TODO: define notations *)
(** Advantage of a distinguisher against a PRF F:
      Adv^PRF_F(&m,D) = `|Pr[IND(Wrap_PRF(F),D) @ &m: res] - Pr[IND(PRFi,D) @ &m: res]| **)
(** Advantage of a distinguisher against **the** PRF operator F:
      Adv^PRF_F(&m,D) = `|Pr[IND(Wrap_PRF(PRFr),D) @ &m: res] - Pr[IND(PRFi,D) @ &m: res]| **)

(** Useful lemmas **)
lemma PRFr_keygen_ll: islossless PRFr.keygen.
proof. by proc; auto; smt. qed.

lemma PRFr_f_ll: islossless PRFr.f.
proof. by proc. qed.