https://github.com/EasyCrypt/easycrypt
Tip revision: 9db28d59d65422c4ba10a109a3dc53d190f7d806 authored by Pierre-Yves Strub on 27 January 2020, 13:46:58 UTC
script for testing EasyCrypt on various external devs
script for testing EasyCrypt on various external devs
Tip revision: 9db28d5
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.