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 = {
var r;
if (x \notin m) {
r <$ uR;
m.[x] <- r;
}
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.