Revision 25d7504145c07e4345a472338a8616b023fc8243 authored by Pierre-Yves Strub on 11 July 2015, 19:03:40 UTC, committed by Pierre-Yves Strub on 12 July 2015, 12:14:23 UTC
[fix #17219]
1 parent 9b8598c
PRF.eca
(* --------------------------------------------------------------------
* 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.
Computing file changes ...