PRF.eca

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

(*** A formalization of pseudo-random functions **)
require import AllCore Distr FSet SmtMap.

(** 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) fmap *)

(*   proc init(): unit = { m <- empty; } *)

(*   proc f (x:D): R = { *)
(*     if (x \notin 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.