SchoolNancy2017: PRG_ex.ec

File PRG_ex.ec, 13.8 KB (added by François Dupressoir, 2 months ago)
Line 
1(* -------------------------------------------------------------------- *)
2require import AllCore Int List Real Distr FSet NewFMap.
3require import IntExtra IntDiv RealExtra Mu_mem StdRing StdOrder StdBigop.
4(*---*) import Bigint Ring.IntID RField IntOrder RealOrder BIA.
5require (*--*) FinType.
6
7(* ---------------- Sane Default Behaviours --------------------------- *)
8pragma -oldip.
9pragma +implicits.
10
11(* -------------------------------------------------------------------- *)
12(** A finite type of seeds equipped with its uniform distribution **)
13clone include MFinite
14rename
15  [type] "t" as "seed"
16  "dunifin" as "dseed"
17  "duniform" as "dseed".
18
19(* -------------------------------------------------------------------- *)
20(** Some output type equipped with some lossless distribution **)
21type output.
22op dout: { output distr | is_lossless dout } as dout_ll.
23
24(* -------------------------------------------------------------------- *)
25(** We use a public RF that, on input a seed, produces a seed and
26    an output...                                                        *)
27module type RF = {
28  proc * init() : unit
29  proc f(x:seed): seed * output
30}.
31
32(** ...to build a PRG that produces random outputs... **)
33(** We let our PRG have internal state, which we need to initialize **)
34module type PRG = {
35  proc * init(): unit
36  proc prg()   : output
37}.
38
39(* -------------------------------------------------------------------- *)
40(** Distinguishers can call
41  *   - the PRG at most qP times, and
42  *   - the PRF at most qF times, and
43  *   - return a boolean *)
44op qP : { int | 0 <= qP } as ge0_qP.
45op qF : { int | 0 <= qF } as ge0_qF.
46
47module type ARF = {
48  proc f(_:seed): seed * output
49}.
50
51module type APRG = {
52  proc prg(): output
53}.
54
55module type Adv (F:ARF) (P:APRG) = {
56  proc a(): bool
57}.
58
59module Exp (A:Adv) (F:RF) (P:PRG) = {
60  module A = A(F,P)
61
62  proc main():bool = {
63    var b: bool;
64
65         F.init();
66         P.init();
67    b <@ A.a();
68    return b;
69  }
70}.
71
72(** A PRG is secure iff it is indistinguishable from sampling in $dout
73    by an adversary with access to the PRF and the PRG interfaces *)
74module PrgI = {
75  proc init () : unit = { }
76
77  proc prg(): output = {
78    var r;
79
80    r <$ dout;
81    return r;
82  }
83}.
84(* Adv^PRG_A,F,P = `| Exp(A,F,P) - Exp(A,F,PrgI) | *)
85
86(* -------------------------------------------------------------------- *)
87(* Concrete considerations                                              *)
88
89(* We use the following RF *)
90module F = {
91  var m:(seed,seed * output) fmap
92
93  proc init(): unit = {
94     m <- map0;
95  }
96
97  proc f (x:seed) : seed * output = {
98    var r1, r2;
99
100    r1 <$ dseed;
101    r2 <$ dout;
102    if (!mem (dom m) x)
103      m.[x] <- (r1,r2);
104
105    return oget (m.[x]);
106  }
107}.
108
109lemma FfL: islossless F.f.
110proof. by proc; auto; rewrite dseed_ll dout_ll. qed.
111
112(* And we are proving the security of the following PRG *)
113module P (F:RF) = {
114  var seed: seed
115  var logP: seed list
116
117  proc init(): unit = {
118    seed <$ dseed;
119  }
120
121  proc prg(): output = {
122    var r;
123
124    (seed,r) <@ F.f (seed);
125    return r;
126  }
127}.
128
129(* -------------------------------------------------------------------- *)
130(* We use the following oracle in an intermediate game that links two
131   sections.                                                            *)
132
133module Psample = {
134  proc init(): unit = {
135    P.seed <$ dseed;
136    P.logP <- [];
137  }
138
139  proc prg(): output = {
140    var r1, r2;
141
142    r1     <$ dseed;
143    r2     <$ dout;
144    P.logP <- P.seed :: P.logP;
145    P.seed <- r1;
146    return r2;
147  }
148}.
149
150lemma PsampleprgL: islossless Psample.prg.
151proof. by proc; auto; rewrite dseed_ll dout_ll. qed.
152
153(* -------------------------------------------------------------------- *)
154(* In preparation of the eager/lazy reasoning step                      *)
155(* -------------------------------------------------------------------- *)
156module Resample = {
157  proc resample() : unit = {
158    var n, r;
159
160    n      <- size P.logP;
161    P.logP <- [];
162    P.seed <$ dseed;
163    while (size P.logP < n) {
164      r      <$ dseed;
165      P.logP <- r :: P.logP;
166    }
167  }
168}.
169
170module Exp'(A:Adv) = {
171  module A = A(F,Psample)
172
173  proc main():bool = {
174    var b : bool;
175         F.init();
176         Psample.init();
177    b <@ A.a();
178         Resample.resample();
179    return b;
180  }
181}.
182
183(* The Proof                                                            *)
184
185section.
186(* Forall Adversary A that does not share memory with P or F... *)
187declare module A:Adv {P,F}.
188
189(* ... and whose a procedure is lossless whenever F.f and P.prg are *)
190axiom AaL (F <: ARF {A}) (P <: APRG {A}):
191  islossless P.prg =>
192  islossless F.f =>
193  islossless A(F,P).a.
194
195(* We show that the adversary can distinguish P from Psample only
196   when P.prg is called twice with the same input. *)
197
198(* First, we add some logging so we can express the bad event *)
199local module Plog = {
200  proc init(): unit = {
201    P.seed <$ dseed;
202    P.logP <- [];
203  }
204
205  proc prg(): output = {
206    var r;
207
208    P.logP     <- P.seed :: P.logP;
209    (P.seed,r) <@ F.f(P.seed);
210    return r;
211  }
212}.
213
214local lemma PlogprgL: islossless Plog.prg.
215proof. by proc; call FfL; wp. qed.
216
217local lemma P_Plog &m:
218  Pr[Exp(A,F,P(F)).main() @ &m: res] = Pr[Exp(A,F,Plog).main() @ &m: res].
219proof.
220byequiv (_: ={glob A} ==> ={res})=> //.
221by do !sim.
222qed.
223
224(* Bad holds whenever:
225 *  - there is a cycle in the state, OR
226 *  - an adversary query collides with an internal seed. *)
227inductive Bad logP (m : ('a,'b) fmap) =
228  | Cycle of (!uniq logP)
229  | Collision r of (mem logP r) & (mem (dom m) r).
230
231lemma negBadE logP (m : ('a,'b) fmap):
232  !Bad logP m <=>
233    (uniq logP /\ forall r, !mem logP r \/ !mem (dom m) r).
234proof.
235(* EX: Prove this. *) admit.
236qed.
237
238(* In this game, we replace the PRF queries with fresh sampling operations *)
239inductive inv (m1 m2 : ('a,'b) fmap) (logP : 'a list) =
240  | Invariant of
241        (forall r, mem (dom m1) r <=> (mem (dom m2) r \/ mem logP r))
242      & (forall r, mem (dom m2) r => m1.[r] = m2.[r]).
243
244local lemma Plog_Psample &m:
245  Pr[Exp(A,F,Plog).main() @ &m: res] <=
246    Pr[Exp(A,F,Psample).main() @ &m: res] +
247    Pr[Exp(A,F,Psample).main() @ &m: Bad P.logP F.m].
248proof.
249apply (ler_trans (Pr[Exp(A,F,Psample).main() @ &m: res \/ Bad P.logP F.m]));
250  last by rewrite Pr [mu_or]; smt(mu_bounded).
251byequiv (_: ={glob A} ==> !(Bad P.logP F.m){2} => ={res})=> // [|/#].
252(* EX: Prove this *) admit.
253qed.
254
255local lemma Psample_PrgI &m:
256  Pr[Exp(A,F,Psample).main() @ &m: res] = Pr[Exp(A,F,PrgI).main() @ &m: res].
257proof.
258(* EX: Prove this *) admit.
259qed.
260
261local lemma Resample_resampleL: islossless Resample.resample.
262proof.
263proc; while (true) (n - size P.logP);
264  first by move=> z; auto; rewrite dseed_ll /#.
265by auto; rewrite dseed_ll /#.
266qed.
267
268local module Exp'A = Exp'(A).
269
270local lemma ExpPsample_Exp' &m:
271    Pr[Exp(A,F,Psample).main() @ &m: Bad P.logP F.m]
272  = Pr[Exp'(A).main() @ &m: Bad P.logP F.m].
273proof.
274byequiv (_: ={glob A} ==> ={P.logP, F.m})=> //; proc.
275(* we first insert the (empty) resampling on the left *)
276transitivity{1} { F.init(); Psample.init(); Resample.resample(); b = Exp'A.A.a(); }
277   (={glob A} ==> ={F.m, P.logP})
278   (={glob A} ==> ={F.m, P.logP})=> //.
279  (* Equality on A's globals *)
280+ by move=> /> &2; exists (glob A){2}.
281  (* no sampling ~ presampling *)
282+ call (: ={P.logP, P.seed, F.m}); first 2 by sim.
283  inline Resample.resample Psample.init F.init.
284  rcondf{2} 7;
285    first by move=> &hr; rnd; wp; conseq (_: _ ==> true) => //.
286  by wp; rnd; wp; rnd{2} predT; auto; rewrite dseed_ll.
287(* presampling ~ postsampling *)
288seq 2 2: (={glob A, glob F, glob Plog}); first by sim.
289eager (H: Resample.resample(); ~ Resample.resample();
290  : ={glob Plog} ==> ={glob Plog})
291  : (={glob A, glob Plog, glob F})=> //;
292  first by sim.
293eager proc H (={glob Plog, glob F})=> //.
294+ eager proc; inline Resample.resample.
295  swap{1} 3 3. swap{2} [4..5] 2. swap{2} [6..8] 1.
296  swap{1} 4 3. swap{1} 4 2. swap{2} 2 4.
297  sim.
298  splitwhile {2} 5 : (size P.logP < n - 1).
299  conseq (_ : _ ==> ={P.logP})=> //.
300  seq 3 5: (={P.logP} /\ (size P.logP = n - 1){2}).
301  + while (={P.logP} /\ n{2} = n{1} + 1 /\ size P.logP{1} <= n{1});
302      first by auto=> /#.
303    by wp; rnd{2}; auto=> />; rewrite dseed_ll; smt(size_ge0).
304  rcondt{2} 1; first by move=> &hr; auto=> /#.
305  rcondf{2} 3; first by move=> &hr; auto=> /#.
306+ by sim.
307+ by sim.
308+ by eager proc; swap{1} 1 4; sim.
309by sim.
310qed.
311
312lemma P_PrgI &m:
313  Pr[Exp(A,F,P(F)).main() @ &m: res] <=
314    Pr[Exp(A,F,PrgI).main() @ &m: res] + Pr[Exp'(A).main() @ &m: Bad P.logP F.m].
315proof.
316(* EX: Prove this *) admit.
317qed.
318end section.
319
320(* -------------------------------------------------------------------- *)
321
322(* We now bound Pr[Exp(A,F,Psample).main() @ &m: Bad Plog.logP F.m] *)
323
324(* For now, we use the following counting variant of the adversary to
325   epxress the final result. Everything up to now applies to
326   non-counting adversaries, but we need the counting to bound the
327   probability of Bad. *)
328
329module C (A:Adv,F:ARF,P:APRG) = {
330  var cF, cP:int
331
332  module CF = {
333    proc f(x): seed * output = {
334      var r = witness;
335
336      if (cF < qF) { cF = cF + 1; r = F.f(x);}
337      return r;
338    }
339  }
340
341  module CP = {
342    proc prg (): output = {
343      var r = witness;
344
345      if (cP < qP) { cP = cP + 1; r = P.prg();}
346      return r;
347    }
348  }
349
350  module A = A(CF,CP)
351
352  proc a(): bool = {
353    var b:bool;
354
355    cF = 0;
356    cP = 0;
357    b = A.a();
358    return b;
359  }
360}.
361
362lemma CFfL (A <: Adv) (F <: ARF) (P <: APRG):
363  islossless F.f =>
364  islossless C(A,F,P).CF.f.
365proof. by move=> FfL; proc; sp; if=> //; call FfL; wp. qed.
366
367lemma CPprgL (A <: Adv) (F <: ARF) (P <: APRG):
368  islossless P.prg =>
369  islossless C(A,F,P).CP.prg.
370proof. by move=> PprgL; proc; sp; if=> //; call PprgL; wp. qed.
371
372lemma CaL (A <: Adv {C}) (F <: ARF {A}) (P <: APRG {A}):
373  (forall (F <: ARF {A}) (P <: APRG {A}),
374    islossless P.prg => islossless F.f => islossless A(F,P).a) =>
375     islossless F.f
376  => islossless P.prg
377  => islossless C(A,F,P).a.
378proof.
379move=> AaL PprgL FfL; proc.
380call (AaL (<: C(A,F,P).CF) (<: C(A,F,P).CP) _ _).
381+ by apply (CPprgL A F P).
382+ by apply (CFfL A F P).
383by wp.
384qed.
385
386section.
387declare module A:Adv {C,P,F}.
388axiom AaL (F <: ARF {A}) (P <: APRG {A}):
389  islossless P.prg =>
390  islossless F.f =>
391  islossless A(F,P).a.
392
393lemma pr &m:
394  Pr[Exp(C(A),F,P(F)).main() @ &m: res] <=
395      Pr[Exp(C(A),F,PrgI).main() @ &m: res]
396    + Pr[Exp'(C(A)).main() @ &m: Bad P.logP F.m].
397proof.
398apply (P_PrgI (<: C(A)) _ &m).
399move=> F0 P0 F0fL P0prgL; apply (CaL A F0 P0) => //.
400by apply AaL.
401qed.
402
403local lemma Bad_bound:
404  phoare [Exp'(C(A)).main : true ==>
405    Bad P.logP F.m] <= ((qP * qF + (qP - 1) * qP %/ 2)%r / Support.card%r).
406proof.
407proc.
408seq 3: true
409       1%r ((qP * qF + (qP - 1) * qP %/ 2)%r / Support.card%r)
410       0%r 1%r
411       (size P.logP <= qP /\ card (dom F.m) <= qF)=> //.
412+ inline Exp'(C(A)).A.a; wp.
413  call (_: size P.logP = C.cP /\ C.cP <= qP /\
414           card (dom F.m) <= C.cF /\ C.cF <= qF).
415  (* prg *)
416  + proc; sp; if=> //.
417    call (_: size P.logP = C.cP - 1 ==> size P.logP = C.cP).
418    + by proc; auto=> /#.
419    by auto=> /#.
420  (* f *)
421  + proc; sp; if=> //.
422    call (_: card (dom F.m) < C.cF ==> card (dom F.m) <= C.cF).
423    + proc; auto=> /> &hr h r1 _ r2 _.
424      by rewrite dom_set fcardU fcard1; smt(fcard_ge0).
425    by auto=> /#.
426  inline *; auto=> />.
427  by rewrite dom0 fcards0 /=; smt(ge0_qP ge0_qF).
428inline Resample.resample.
429exists* P.logP; elim* => logP.
430seq 3: true
431       1%((qP * qF + (qP - 1) * qP %/ 2)%r / Support.card%r)
432       0%r 1%r
433       (n = size logP /\ n <= qP /\ P.logP = [] /\
434        card (dom F.m) <= qF)=> //.
435+ by rnd; wp.
436conseq (_ : _ : <= (if Bad P.logP F.m then 1%r else
437    (sumid (qF + size P.logP) (qF + n))%r / Support.card%r)).
438+ move=> /> &hr.
439  have /= -> /= szlog_le_qP szm_le_qF := negBadE A AaL [] F.m{hr}.
440  apply/ler_wpmul2r; first smt(Support.card_gt0).
441  apply/le_fromint.
442  rewrite -{1}(@add0z qF) big_addn /= /predT -/predT.
443  rewrite (@addzC qF) !addrK big_split big_constz.
444  rewrite count_predT size_range /= max_ler ?size_ge0 addrC.
445  rewrite ler_add 1:mulrC ?ler_wpmul2r // ?ge0_qF.
446  rewrite sumidE ?size_ge0 leq_div2r // mulrC.
447  move: (size_ge0 logP) szlog_le_qP => /IntOrder.ler_eqVlt [<- /#|gt0_sz le].
448  by apply/IntOrder.ler_pmul => // /#.
449while{1} (n <= qP /\ card (dom F.m) <= qF).
450+ move=> Hw; exists* P.logP, F.m, n; elim* => logPw m n0.
451  case: (Bad P.logP F.m).
452  + by conseq (_ : _ : <= (1%r))=> // /#.
453  seq 2: (Bad P.logP F.m)
454         ((qF + size logPw)%r / Support.card%r) 1%r 1%r
455         ((sumid (qF + (size logPw + 1)) (qF + n))%r / Support.card%r)
456         (n = n0 /\ F.m = m /\ r::logPw = P.logP /\
457          n <= qP /\ card (dom F.m) <= qF)=> //.
458  + by wp; rnd=> //.
459  + wp; rnd; auto=> /> &hr _ /le_fromint domF_le_qF _.
460    rewrite (negBadE A AaL)=> //= -[uniq_logP logP_disj_domF].
461    apply (ler_trans (mu dseed (predU (mem (dom F.m{hr}))
462                                      (mem P.logP{hr})))).
463    + by apply mu_sub=> x [] /#.
464    rewrite mu_or (@mu_mem (dom F.m{hr}) dseed (inv (Support.card%r))).
465    + by move=> x _; rewrite dseed1E.
466    rewrite (@mu_mem_card (P.logP{hr}) dseed (inv (Support.card%r))).
467    + by move=> x _; rewrite dseed1E.
468    rewrite (@cardE (oflist P.logP{hr})) (@perm_eq_size _ (P.logP{hr})) 1:perm_eq_sym 1:oflist_uniq //.
469    have -> /=: mu dseed (predI (mem (dom F.m{hr})) (mem P.logP{hr})) = 0%r.
470    + by rewrite -(@mu0 dseed) /predI; apply/mu_eq=> x; move: (logP_disj_domF x)=> [] ->.
471    rewrite -mulrDl fromintD.
472    have: (card (dom F.m{hr}))%r + (size P.logP{hr})%r <= qF%r + (size P.logP{hr})%r.
473    + exact/ler_add.
474    have: 0%r <= Support.card%r by smt(@Support).
475    smt(@RealExtra).
476  + conseq Hw; progress=> //.
477    by rewrite H1 /= (Ring.IntID.addrC 1) lerr.
478  progress=> //; rewrite H2 /= -mulrDl addrA -fromintD.
479  rewrite
480    (@BIA.big_cat_int (qF + size P.logP{hr} + 1) (_ + List.size _))
481    ?BIA.big_int1 /#.
482by skip; progress=> /#.
483qed.
484
485lemma conclusion &m:
486  Pr[Exp(C(A),F,P(F)).main() @ &m: res] <=
487      Pr[Exp(C(A),F,PrgI).main() @ &m: res]
488    + (qP * qF + (qP - 1) * qP %/ 2)%r / Support.card%r.
489proof.
490(* EX: Prove thi *) admit.
491qed.
492end section.