swh:1:snp:f92f30fa3090eae65efe8d40c3d27dad22819990
Tip revision: 955e909402cf7a5dc3dc55e4de13bbf373edd920 authored by Pierre-Yves Strub on 30 July 2015, 08:20:28 UTC
NewList: last_ -> last.
NewList: last_ -> last.
Tip revision: 955e909
PRG.ec
require import Int List Real FSet FMap Distr.
require (*--*) Monoid.
(*---*) import Monoid.Miplus.
(*** Some type definitions *)
(** Our PRG uses a type for internal seeds
and a type for its actual output. *)
type seed.
op dseed: { seed distr | is_uniform_over dseed predT } as dseed_uf_fu.
lemma dseed_ll: is_lossless dseed by [].
lemma dseed_suf: is_subuniform dseed by [].
lemma dseed_fu: is_full dseed by [].
op pr_dseed = mu_x dseed witness.
type output.
op dout: { output distr | is_lossless dout } as dout_ll.
(** We use a PRF that, on input a seed, produces a seed and an output... *)
module type PRF = {
proc * init() : unit
proc f(x:seed): seed * output
}.
(** ... to build a PRG that produces random output without requiring new input... *)
module type PRG = {
proc * init(): unit (* We let our PRG have internal state, which we should be able to initialize *)
proc prg() : output
}.
(*** Defining security *)
(** Distinguishers can call
the PRG at most qP times and
the PRF at most qF times and
return a boolean *)
op qP:int.
axiom leq0_qP: 0 <= qP.
op qF:int.
axiom leq0_qF: 0 <= qF.
module type APRF = {
proc f(x:seed): seed * output
}.
module type APRG = {
proc prg(): output
}.
module type Adv (F:APRF,P:APRG) = {
proc a(): bool {F.f P.prg} (* Fixing the order of oracles for stability *)
}.
module Exp (A:Adv,F:PRF,P:PRG) = {
module A = A(F,P)
proc main():bool = {
var b: bool;
F.init();
P.init();
b = A.a();
return b;
}
}.
(** A PRG is secure iff it is indistinguishable from
sampling in $dout by an adversary with access to the PRF
and the PRG interfaces *)
module PrgI = {
proc init () : unit = { }
proc prg(): output = {
var r;
r = $dout;
return r;
}
}.
(*** Concrete considerations *)
(** We use the following PRF *)
module F = {
var m:(seed,seed * output) map
proc init(): unit = {
m = FMap.empty;
}
proc f (x:seed) : seed * output = {
var r1, r2;
r1 = $dseed;
r2 = $dout;
if (!mem x (dom m))
m.[x] = (r1,r2);
return oget (m.[x]);
}
}.
lemma FfL: islossless F.f.
proof.
by proc; wp; do!rnd predT;
skip; smt.
qed.
(** And we are proving the security of the following PRG *)
module P (F:PRF) = {
var seed: seed
var logP: seed list
proc init(): unit = {
seed = $dseed;
}
proc prg(): output = {
var r;
(seed,r) = F.f (seed);
return r;
}
}.
(** We use the following oracle in an intermediate game
that links two sections. Ideally, we would hide it
somehwere, but nested sections don't work yet. *)
(* Note that it uses P's state (in which we have a
useless thing) to avoid contaminating the final
result. *)
module Psample = {
proc init(): unit = {
P.seed = $dseed;
P.logP = [];
}
proc prg(): output = {
var r1, r2;
r1 = $dseed;
r2 = $dout;
P.logP = P.seed :: P.logP;
P.seed = r1;
return r2;
}
}.
lemma PsampleprgL: islossless Psample.prg.
proof. by proc; wp; do 2!rnd predT; skip; smt. qed.
(** In preparation of the eager/lazy reasoning step *)
(* Again, note that none of these have their own state.
Therefore, it does not matter overmuch that they
are not hidden. *)
module Resample = {
proc resample() : unit = {
var n, r;
n = length P.logP;
P.logP = [];
P.seed = $dseed;
while (length P.logP < n) {
r = $dseed;
P.logP = r :: P.logP;
}
}
}.
module Exp'(A:Adv) = {
module A = A(F,Psample)
proc main():bool = {
var b : bool;
F.init();
Psample.init();
b = A.a();
Resample.resample();
return b;
}
}.
(*** The Proof ***)
section.
declare module A:Adv {P,F}.
axiom AaL (F <: APRF {A}) (P <: APRG {A}):
islossless F.f =>
islossless P.prg =>
islossless A(F,P).a.
(** Adding some logging so we can express the bad event *)
local module Plog = {
proc init(): unit = {
P.seed = $dseed;
P.logP = [];
}
proc prg(): output = {
var r;
P.logP = P.seed :: P.logP;
(P.seed,r) = F.f(P.seed);
return r;
}
}.
local lemma PlogprgL: islossless Plog.prg.
proof. by proc; call FfL; wp. qed.
local lemma P_Plog &m:
Pr[Exp(A,F,P(F)).main() @ &m: res] = Pr[Exp(A,F,Plog).main() @ &m: res].
proof.
byequiv (_: ={glob A} ==> ={res})=> //.
by do !sim.
qed.
pred Bad logP (m:('a,'b) map) = (* Bad holds whenever: *)
!unique logP (* - there is a cycle in the state, OR *)
\/ exists r, mem r logP /\ mem r (dom m). (* - an adversary query collides with an internal seed. *)
lemma notBad logP (m:('a,'b) map):
!Bad logP m <=>
(unique logP /\ forall r, !mem r logP \/ !mem r (dom m))
by smt.
(* In this game, we replace the PRF with fresh samples *)
pred inv (m1 m2:('a,'b) map) (logP:'a list) =
(forall r, mem r (dom m1) <=> (mem r (dom m2) \/ mem r logP)) /\
(forall r, mem r (dom m2) => m1.[r] = m2.[r]).
local lemma Plog_Psample &m:
Pr[Exp(A,F,Plog).main() @ &m: res] <=
Pr[Exp(A,F,Psample).main() @ &m: res] +
Pr[Exp(A,F,Psample).main() @ &m: Bad P.logP F.m].
proof.
apply (Trans _ (Pr[Exp(A,F,Psample).main() @ &m: res \/ Bad P.logP F.m]));
last by rewrite Pr [mu_or]; smt.
byequiv (_: ={glob A} ==> !(Bad P.logP F.m){2} => ={res})=> //; last smt.
proc.
call (_: Bad P.logP F.m, ={P.seed} /\ inv F.m{1} F.m{2} P.logP{2}).
(* adversary is lossless *)
by apply AaL.
(* [F.f ~ F.f: I] when Bad does not hold *)
proc; wp; do !rnd; wp; skip; rewrite /Top.inv; progress;expect 13 smt.
(* F.f is lossless when Bad holds *)
by intros=> _ _; apply FfL.
(* F.f preserves bad *)
intros=> _ //=; proc.
case (mem x (dom F.m)).
by rcondf 3; wp; do !rnd=> //; wp; skip; smt.
rcondt 3; first by do !rnd; wp.
auto; progress. smt. smt.
elim H=> H; [by left | right].
elim H=> r [r_in_logP r_in_m].
by exists r; split=> //; rewrite dom_set mem_add; left.
(* [Psample.prg ~ Plog.prg: I] when Bad does not hold *)
proc; inline F.f. swap{2} 3 -2.
wp; do 2!rnd; wp; skip; progress; first 2 last; last 9 smt.
by move: H6; rewrite notBad=> [logP_unique contradiction]; smt.
(* Plog.prg is lossless when Bad holds *)
by intros=> _ _; proc; inline F.f;
wp; do 2!rnd predT; wp;
skip; smt.
(* Psample.prg preserves bad *)
move=> _ //=; proc.
wp; do 2!rnd; wp.
by skip; rewrite /Bad; progress; smt.
(* Returning to main *)
call (_: ={glob F} ==> ={glob P} /\ inv F.m{1} F.m{2} P.logP{2});
first by proc; wp; rnd; skip; smt.
call (_: true ==> ={glob F}); first by sim.
by skip; smt.
qed.
local lemma Psample_PrgI &m:
Pr[Exp(A,F,Psample).main() @ &m: res] = Pr[Exp(A,F,PrgI).main() @ &m: res].
proof.
byequiv (_: ={glob A} ==> ={res})=> //; proc.
call (_: ={glob F})=> //.
(* F.f *)
by sim.
(* Psample.prg ~ PrgI.prg *)
by proc; wp; rnd; rnd{1}; wp; skip; smt.
conseq* (_: _ ==> ={glob A, glob F})=> //.
by inline *; auto; smt.
qed.
local lemma Resample_resampleL: islossless Resample.resample.
proof.
proc.
while (true) (n - length P.logP);
first by intros=> z; wp; rnd predT; skip; smt.
by rnd predT; wp; skip; smt.
qed.
local module Exp'A = Exp'(A).
local lemma ExpPsample_Exp' &m:
Pr[Exp(A,F,Psample).main() @ &m: Bad P.logP F.m] = Pr[Exp'(A).main() @ &m: Bad P.logP F.m].
proof.
byequiv (_: ={glob A} ==> ={P.logP, F.m})=> //; proc.
transitivity{1} { F.init(); Psample.init(); Resample.resample(); b = Exp'A.A.a(); }
(={glob A} ==> ={F.m, P.logP})
(={glob A} ==> ={F.m, P.logP})=> //.
(* Equality on A's globals *)
by intros=> &1 &2 A; exists (glob A){1}.
(* no sampling ~ presampling *)
sim; inline Resample.resample Psample.init F.init.
rcondf{2} 7;
first by intros=> _; rnd; wp; conseq (_: _ ==> true) => //.
by wp; rnd; wp; rnd{2} (True); wp; skip; smt.
(* presampling ~ postsampling *)
seq 2 2: (={glob A, glob F, glob Plog}); first by sim.
eager (H: Resample.resample(); ~ Resample.resample();: ={glob Plog} ==> ={glob Plog}):
(={glob A, glob Plog, glob F})=> //;
first by sim.
eager proc H (={glob Plog, glob F})=> //.
by eager proc; swap{1} 1 4; sim.
by sim.
eager proc; inline Resample.resample.
swap{1} 3 3. swap{2} [4..5] 2. swap{2} [6..8] 1.
swap{1} 4 3. swap{1} 4 2. swap{2} 2 4.
sim.
splitwhile {2} 5 : (length P.logP < n - 1).
conseq* (_ : _ ==> ={P.logP})=> //.
seq 3 5: (={P.logP} /\ (length P.logP = n - 1){2}).
while (={P.logP} /\ n{2} = n{1} + 1 /\ length P.logP{1} <= n{1});
first by wp; rnd; skip; progress; smt.
by wp; rnd{2}; skip; progress=> //; smt.
rcondt{2} 1; first by intros=> _; skip; smt.
rcondf{2} 3; first by intros=> _; wp; rnd; skip; smt.
by sim.
by sim.
qed.
lemma P_PrgI &m:
Pr[Exp(A,F,P(F)).main() @ &m: res] <=
Pr[Exp(A,F,PrgI).main() @ &m: res] + Pr[Exp'(A).main() @ &m: Bad P.logP F.m].
proof.
by rewrite (P_Plog &m) -(ExpPsample_Exp' &m) -(Psample_PrgI &m) (Plog_Psample &m).
qed.
end section.
(** We now bound Pr[Exp(A,F,Psample).main() @ &m: Bad Plog.logP F.m] *)
(* For now, we use the following counting variant of
the adversary to epxress the final result. Everything
up to now applies to non-counting adversaries, but we
need the counting to bound the probability of Bad. *)
module C (A:Adv,F:APRF,P:APRG) = {
var cF, cP:int
module CF = {
proc f(x): seed * output = {
var r = witness;
if (cF < qF) { cF = cF + 1; r = F.f(x);}
return r;
}
}
module CP = {
proc prg (): output = {
var r = witness;
if (cP < qP) { cP = cP + 1; r = P.prg();}
return r;
}
}
module A = A(CF,CP)
proc a(): bool = {
var b:bool;
cF = 0;
cP = 0;
b = A.a();
return b;
}
}.
lemma CFfL (A <: Adv) (F <: APRF) (P <: APRG):
islossless F.f =>
islossless C(A,F,P).CF.f.
proof.
intros=> FfL.
proc; sp; if=> //.
by call FfL; wp.
qed.
lemma CPprgL (A <: Adv) (F <: APRF) (P <: APRG):
islossless P.prg =>
islossless C(A,F,P).CP.prg.
proof.
intros=> PprgL.
proc; sp; if=> //.
by call PprgL; wp.
qed.
lemma CaL (A <: Adv {C}) (F <: APRF {A}) (P <: APRG {A}):
(forall (F <: APRF {A}) (P <: APRG {A}),
islossless F.f =>
islossless P.prg =>
islossless A(F,P).a) =>
islossless F.f =>
islossless P.prg =>
islossless C(A,F,P).a.
proof.
intros=> AaL FfL PprgL.
proc.
call (AaL (<: C(A,F,P).CF) (<: C(A,F,P).CP) _ _).
by apply (CFfL A F P); assumption.
by apply (CPprgL A F P); assumption.
by wp.
qed.
section.
declare module A:Adv {C,P,F}.
axiom AaL (F <: APRF {A}) (P <: APRG {A}):
islossless F.f =>
islossless P.prg =>
islossless A(F,P).a.
lemma pr &m:
Pr[Exp(C(A),F,P(F)).main() @ &m: res] <=
Pr[Exp(C(A),F,PrgI).main() @ &m: res] + Pr[Exp'(C(A)).main() @ &m: Bad P.logP F.m].
proof.
apply (P_PrgI (<: C(A)) _ &m).
intros=> F0 P0 F0fL P0prgL; apply (CaL A F0 P0); last 2 assumption.
by apply AaL.
qed.
local lemma Bad_bound:
phoare [Exp'(C(A)).main : true ==> Bad P.logP F.m] <= ((qP * qF + (qP - 1) * qP /% 2)%r * pr_dseed).
proof.
proc.
seq 3: true
1%r ((qP * qF + (qP - 1) * qP /% 2)%r * pr_dseed)
0%r 1%r
(length P.logP <= qP /\ card (dom F.m) <= qF)=> //.
inline Exp'(C(A)).A.a; wp.
call (_: length P.logP = C.cP /\ C.cP <= qP /\
card (dom F.m) <= C.cF /\ C.cF <= qF).
(* f *)
proc; sp; if=> //.
call (_: card (dom F.m) < C.cF ==> card (dom F.m) <= C.cF);
first by proc; wp; do !rnd; skip; smt.
by wp; skip; smt.
(* prg *)
proc; sp; if=> //.
call (_: length P.logP = C.cP - 1 ==> length P.logP = C.cP);
first by proc; wp; do !rnd; skip; smt.
by wp; skip; smt.
by inline Psample.init F.init;
wp; rnd; wp; skip; smt.
inline Resample.resample.
exists* P.logP; elim* => logP.
seq 3: true
1%r ((qP * qF + (qP - 1) * qP /% 2)%r * pr_dseed)
0%r 1%r
(n = length logP /\ n <= qP /\ P.logP = [] /\
card (dom F.m) <= qF)=> //.
by rnd; wp.
conseq (_:_: <= (if Bad P.logP F.m then 1%r else
((sum_n (qF + length P.logP) (qF + n - 1))%r * pr_dseed))).
progress; cut ->: Bad [] F.m{hr} = false by smt.
rewrite //=; apply CompatOrderMult=> //; last smt.
generalize H0 H; elim/list_case logP=> //=.
(* logP = [] *)
rewrite /sum_n sum_ij_gt; first smt.
cut HqP: 0 <= (qP - 1)* qP by smt.
cut Hmod: 0 <= (qP - 1) * qP /% 2 by smt.
by rewrite from_intMle; smt.
(* logP = x::xs *)
intros=> x l H0 H; rewrite sumn_ij; first smt.
rewrite !FromInt.Add.
apply addleM.
cut ->: (qF + (1 + length l) - 1 - qF + 1) = (1 + length l) by smt.
cut ->: qF * (1 + length l) = (1 + length l) * qF by smt.
smt.
rewrite from_intMle; apply ediv_Mle=> //.
by apply mulMle; smt.
while{1} (n <= qP /\ card (dom F.m) <= qF).
intros Hw.
exists* P.logP, F.m, n; elim* => logPw m n0.
case (Bad P.logP F.m).
by conseq* ( _ : _ : <= (1%r))=> //; smt.
seq 2: (Bad P.logP F.m)
((qF + length logPw)%r * pr_dseed) 1%r
1%r ((sum_n (qF + (length logPw + 1)) (qF + n - 1))%r * pr_dseed)
(n = n0 /\ F.m = m /\ r::logPw = P.logP /\
n <= qP /\ card (dom F.m) <= qF)=> //.
by wp; rnd=> //.
wp; rnd; skip; progress.
generalize H2; rewrite !FromInt.Add Mul_distr_r /Bad -nor=> //= [Hu Hf].
apply (Real.Trans _ (mu dseed (predU (fun x, mem x (dom F.m{hr}))
(fun x, mem x P.logP{hr}))));
first by apply mu_sub=> x /=; smt.
apply mu_or_le.
rewrite (mu_eq _ _ (cpMem (dom F.m{hr})));
first by intros x; rewrite /= /cpMem; smt.
apply (Real.Trans _ ((card (dom F.m{hr}))%r * pr_dseed)).
apply mu_cpMem_le=> x _.
by rewrite (dseed_suf x witness) 3:/pr_dseed // dseed_fu.
by apply CompatOrderMult; smt.
by apply mu_Lmem_le_length; smt.
conseq Hw; progress=> //.
generalize H1; rewrite -neqF=> -> //=.
cut ->: 1 + length logPw = length logPw + 1 by smt.
done.
progress => //.
generalize H2; rewrite -neqF=> -> //=.
rewrite -Mul_distr_r -Int.CommutativeGroup.Assoc -FromInt.Add sum_n_i1j //.
smt.
by skip; progress; smt.
qed.
lemma conclusion &m:
Pr[Exp(C(A),F,P(F)).main() @ &m: res] <=
Pr[Exp(C(A),F,PrgI).main() @ &m: res] + (qP * qF + (qP - 1) * qP /% 2)%r* mu_x dseed witness.
proof.
apply (Real.Trans _ (Pr[Exp(C(A),F,PrgI).main() @ &m: res] +
Pr[Exp'(C(A)).main() @ &m: Bad P.logP F.m])).
by apply (pr &m).
cut: Pr[Exp'(C(A)).main() @ &m: Bad P.logP F.m] <= (qP * qF + (qP - 1) * qP/%2)%r * pr_dseed
by byphoare Bad_bound.
smt.
qed.
end section.
(**** This is leftover from an old proof that went all the way to the absolute value... Should we care? *)
(*
module NegA (A:Adv, P:AOrclPrg, R:OrclRnd) = {
module A = A(P,R)
fun a() : bool = {
var ba:bool;
ba = A.a();
return !ba;
}
}.
lemma lossNegA (A<:Adv) :
(forall (O1 <: AOrclPrg{A}) (O2 <: OrclRnd{A}),
islossless O1.prg => islossless O2.f => islossless A(O1, O2).a) =>
forall (O1 <: AOrclPrg{NegA(A)}) (O2 <: OrclRnd{NegA(A)}),
islossless O1.prg => islossless O2.f => islossless NegA(A, O1, O2).a.
proof.
intros Hloss O1 O2 HO1 HO2;fun.
call (_:true) => //.
qed.
lemma NegA_Neg_main (P<:OrclPrg) (A<:Adv{P,F,C}) &m:
Pr[AdvAbsVal.Neg_main(Exp(C(A),P)).main() @ &m : res] =
Pr[Exp(C(NegA(A)),P).main() @ &m : res].
proof.
equiv_deno (_ : ={glob A, glob P, glob F} ==> ={res}) => //.
fun.
inline Exp(C(A), P).main Exp(C(NegA(A)), P).A.a C(NegA(A), P, F).A.a
Exp(C(A), P).A.a;wp; eqobs_in.
qed.
lemma lossExp (P<:OrclPrg) (A<:Adv{P,F,C}):
(forall (O1 <: AOrclPrg{A}) (O2 <: OrclRnd{A}),
islossless O1.prg => islossless O2.f => islossless A(O1, O2).a) =>
islossless P.prg => islossless P.init =>
islossless Exp(C(A),P).main.
proof.
intros HA Hp Hi;fun.
call (_: true).
call (_: true) => //.
fun.
if;last by wp.
by call Hp;wp.
fun.
if; last by wp.
by call lossless_Ff;wp.
by wp.
call Hi.
by call (_:true);first wp.
qed.
lemma conclusion (A<:Adv{Prg,F,C}) :
(forall (O1 <: AOrclPrg{A}) (O2<:OrclRnd{A}), islossless O1.prg => islossless O2.f =>
islossless A(O1,O2).a) =>
forall &m,
`| Pr[Exp(C(A),Prg).main() @ &m : res] - Pr[Exp(C(A),Prg_r).main() @ &m : res] | <=
(qP*qF + (qP - 1)*qP/%2)%r*bd1.
proof.
intros Hloss &m.
case (Pr[Exp(C(A), Prg).main() @ &m : res] <= Pr[Exp(C(A), Prg_r).main() @ &m : res]) => Hle.
cut H := conclusion_aux (NegA(A)) _ &m.
by apply (lossNegA A).
generalize H;rewrite -(NegA_Neg_main Prg A &m) -(NegA_Neg_main Prg_r A &m).
rewrite (AdvAbsVal.Neg_A_Pr_minus (Exp(C(A), Prg)) &m).
apply (lossExp Prg A) => //.
by fun;call lossless_Ff.
fun;rnd;skip;smt.
rewrite (AdvAbsVal.Neg_A_Pr_minus (Exp(C(A), Prg_r)) &m);last smt.
apply (lossExp Prg_r A) => //.
by fun;rnd;skip;smt.
by fun.
by cut H := conclusion_aux A _ &m => //;smt.
save.
*)