swh:1:snp:1160b607213f14ec0f922dad3284705c8e588b30
Tip revision: 9b906a364f732efd3b8a29f5316c0fd22ede833c authored by Pierre-Yves Strub on 10 February 2020, 09:45:49 UTC
Merge branch '1.0' into deploy-lamport
Merge branch '1.0' into deploy-lamport
Tip revision: 9b906a3
PRF.eca
(*** A formalization of pseudo-random functions **)
require import Int Real FSet SmtMap Distr.
(** 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, R, K.
op dK: { K distr | is_lossless dK } as dK_ll.
op F:K -> D -> R.
(** The Real PRF is defined as follows *)
module PRFr = {
var k:K
proc init(): unit = { k = $dK; }
proc f(x:D): R = { return F k x; }
}.
(** Security is expressed with respect to
the Random Function defined by some
uniform distribution on an
unspecified subset of R. *)
op uR: { R distr | is_uniform uR } as uR_uf.
module type PRF = {
proc init(): unit
proc f(x:D): R
}.
module type PRFA = {
proc f(x:D): R
}.
module type Distinguisher(F:PRFA) = {
proc distinguish(): bool
}.
module IND (F:PRF,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] = $uR;
return (oget m.[x]);
}
}.
(** Advantage of a distinguisher against a PRF F:
Adv_F(D) = `|IND(F,D) - IND(PRFi,D)| **)
lemma PRFr_init_ll: islossless PRFr.init.
proof. by proc; auto; rewrite -/predT; smt (dK_ll). qed.
lemma PRFr_f_ll: islossless PRFr.f.
proof. by proc. qed.