SchoolNancy2017: br93_ex.ec

File br93_ex.ec, 17.4 KB (added by François Dupressoir, 5 days ago)
Line 
1(* -------------------------------------------------------------------- *)
2require import AllCore List FSet NewFMap.
3require import Distr DBool.
4require (*--*) BitWord OW ROM.
5
6(* ---------------- Sane Default Behaviours --------------------------- *)
7pragma -oldip.
8pragma +implicits.
9
10(* -------------------------------------------------------------------- *)
11(* We start by proving Bellare and Rogaway's algorithm IND-CPA secure   *)
12(* on abstract datatypes with minimal structure. We then instantiate to *)
13(* semi-concrete fixed-length bitstrings (with abstract lengths).       *)
14(* -------------------------------------------------------------------- *)
15
16abstract theory BR93.
17(* A set `ptxt` of plaintexts, equipped with an nilpotent addition (+^) *)
18type ptxt.
19
20op (+^): ptxt -> ptxt -> ptxt.
21axiom addA p1 p2 p3: (p1 +^ p2) +^ p3 = p1 +^ (p2 +^ p3).
22axiom addC p1 p2: p1 +^ p2 = p2 +^ p1.
23axiom addKp p1 p2: (p1 +^ p1) +^ p2 = p2.
24
25lemma addpK p1 p2: p1 +^ p2 +^ p2 = p1.
26proof. by rewrite addC -addA addC -addA addKp. qed.
27
28(* and a lossless, full, uniform distribution dptxt                     *)
29op dptxt: { ptxt distr |    is_lossless dptxt
30                         /\ is_full dptxt
31                         /\ is_uniform dptxt } as dptxt_llfuuni.
32lemma dptxt_ll: is_lossless dptxt by exact/(andWl _ dptxt_llfuuni).
33lemma dptxt_uni: is_uniform dptxt by have [#]:= dptxt_llfuuni.
34lemma dptxt_fu: is_full dptxt by have [#]:= dptxt_llfuuni.
35lemma dptxt_funi: is_funiform dptxt
36by exact/(is_full_funiform dptxt_fu dptxt_uni).
37
38(* A set `rand` of nonces, equipped with                                *)
39(*                               a lossless, uniform distribution drand *)
40type rand.
41op drand: { rand distr |    is_lossless drand
42                         /\ is_uniform drand } as drand_lluni.
43lemma drand_ll: is_lossless drand by exact/(andWl _ drand_lluni).
44lemma drand_uni: is_uniform drand by exact/(andWr _ drand_lluni).
45
46(* A set `ctxt` of ciphertexts defined as                               *)
47(*                           the cartesian product of `rand` and `ptxt` *)
48type ctxt = rand * ptxt.
49
50(* A set `pkey * skey` of keypairs, equipped with                       *)
51(*                         a lossless, full, uniform distribution dkeys *)
52type pkey, skey.
53op dkeys: { (pkey * skey) distr |    is_lossless dkeys
54                                  /\ is_funiform dkeys } as dkeys_llfuni.
55lemma dkeys_ll: is_lossless dkeys by exact/(andWl _ dkeys_llfuni).
56lemma dkeys_funi: is_funiform dkeys by exact/(andWr _ dkeys_llfuni).
57
58(* A family `f` of trapdoor permutations over `rand`,                   *)
59(*        indexed by `pkey`, with inverse family `fi` indexed by `skey` *)
60op f : pkey -> rand -> rand.
61op fi: skey -> rand -> rand.
62axiom fK pk sk x: (pk,sk) \in dkeys => fi sk (f pk x) = x.
63
64lemma fI pk x y: (exists sk, (pk,sk) \in dkeys) =>
65  f pk x = f pk y => x = y.
66proof. by move=> [sk] + fx_eq_fy - /fK ^ /(_ x) <- /(_ y) <-; congr. qed.
67
68(* A random oracle from `rand` to `ptxt`, modelling a hash function H   *)
69clone import ROM.Lazy as H with
70  type from  <- rand,
71  type to    <- ptxt,
72  op dsample <- fun _ => dptxt.
73import Types.
74
75(* We can define the Bellare-Rogaway 93 PKE Scheme                      *)
76module BR93(H:Oracle) = {
77  proc keygen() = {
78    var kp;
79
80    kp <$ dkeys;
81    return kp;
82  }
83
84  proc enc(pk, m) = {
85    var r, h;
86
87    r <$ drand;
88    h <@ H.o(r);
89    return (f pk r,h +^ m);
90  }
91
92  proc dec(sk, c) = {
93    var r, h, m;
94
95    (r,m) <- c;
96    r     <- fi sk r;
97    h     <@ H.o(r);
98    return h +^ m;
99  }
100}.
101
102(* And we can quickly prove it correct                                  *)
103section Correctness.
104local module Correctness = {
105  proc main(m) = {
106    var pk, sk, c, m';
107
108    (pk,sk) <@ BR93(RO).keygen();
109    c       <@ BR93(RO).enc(pk,m);
110    m'      <@ BR93(RO).dec(sk,c);
111    return (m = m');
112  }
113}.
114
115local lemma BR93_correct &m m: Pr[Correctness.main(m) @ &m: res] = 1%r.
116proof.
117(** EX: Reach the qed. **)
118admit.
119qed.
120end section Correctness.
121
122(* However, what we are really interested in is proving that it is      *)
123(* IND-CPA secure if `f` is a one-way trapdoor permutation.             *)
124
125(* We use cloning to get definitions for OWTP security                  *)
126clone import OW as OW_rand with
127  type D           <- rand,
128  type R           <- rand,
129  type pkey        <- pkey,
130  type skey        <- skey,
131  op   dkeys       <- dkeys,
132  op   challenge _ <- drand,
133  op   f           <- f,
134  op   finv        <- fi
135proof dkeys_ll, finvof, challenge_ll, challenge_uni.
136realize dkeys_ll by exact/dkeys_ll.
137realize challenge_ll by move=> _ _; exact/drand_ll.
138realize challenge_uni by move=> _ _; exact/drand_uni.
139realize finvof by move=> pk sk x /fK ->.
140
141(* But we can't do it (yet) for IND-CPA because of the random oracle    *)
142(*             Instead, we define CPA for BR93 with that particular RO. *)
143module type Adv (ARO: ARO)  = {
144  proc a1(p:pkey): (ptxt * ptxt)
145  proc a2(c:ctxt): bool
146}.
147
148(* We need to log the random oracle queries made to the adversary       *)
149(*                               in order to express the final theorem. *)
150module Log (H:Oracle) = {
151  var qs: rand list
152
153  proc init() = {
154    qs <- [];
155          H.init();
156  }
157
158  proc o(x) = {
159    var r;
160
161    qs <- x::qs;
162    r  <@ H.o(x);
163    return r;
164  }
165}.
166
167module BR93_CPA(A:Adv) = {
168  proc main(): bool = {
169    var pk, sk, m0, m1, c, b, b';
170
171                Log(RO).init();
172    (pk,sk)  <@ BR93(RO).keygen();
173    (m0,m1)  <@ A(Log(RO)).a1(pk);
174    b        <$ {0,1};
175    c        <@ BR93(RO).enc(pk,b?m0:m1);
176    b'       <@ A(Log(RO)).a2(c);
177    return b' = b;
178  }
179}.
180
181(* EX: Modularise BR93_CPA further so that you have a definition of     *)
182(* the IND-CPA game parameterised by RO, scheme and adversary that can  *)
183(*                                         be reused for other schemes. *)
184(* Keep BR93_CPA as it is to avoid difficulties in the proof below.     *)
185
186(* We want to prove the following:                                      *)
187(*   forall (valid) CPA adversary A which makes at most q queries to H, *)
188(*     there exists a OW adversary I such that                          *)
189(*          `|Pr[BR_CPA(A): res] - 1/2| <= Pr[OW_f(I): res]             *)
190(* We construct I as follows, using A.a1 and A.a2 as black boxes        *)
191module I(A:Adv): Inverter = {
192  var x:rand
193
194  proc invert(pk:pkey,y:rand): rand = {
195    var m0, m1, h, b;
196
197               Log(RO).init();
198    (m0,m1) <@ A(Log(RO)).a1(pk);
199    h       <$ dptxt;
200    b       <@ A(Log(RO)).a2(y,h);
201    x       <- nth witness Log.qs (find (fun p => f pk p = y) Log.qs);
202
203    return x;
204  }
205}.
206
207(* We now prove the result using a sequence of games                    *)
208section.
209(* All lemmas in this section hold for all (valid) CPA adversary A      *)
210declare module A : Adv { RO, Log }.
211
212axiom A_a1_ll (O <: ARO {A}): islossless O.o => islossless A(O).a1.
213axiom A_a2_ll (O <: ARO {A}): islossless O.o => islossless A(O).a2.
214
215(* Step 1: replace RO call with random sampling                         *)
216local module Game1 = {
217  var r: rand
218
219  proc main() = {
220    var pk, sk, m0, m1, b, h, c, b';
221                Log(RO).init();
222    (pk,sk)  <$ dkeys;
223    (m0,m1)  <@ A(Log(RO)).a1(pk);
224    b        <$ {0,1};
225
226    r        <$ drand;
227    h        <$ dptxt;
228    c        <- ((f pk r),h +^ (b?m0:m1));
229
230    b'       <@ A(Log(RO)).a2(c);
231    return b' = b;
232  }
233}.
234
235local lemma pr_Game0_Game1 &m:
236     Pr[BR93_CPA(A).main() @ &m: res]
237  <=   Pr[Game1.main() @ &m: res]
238     + Pr[Game1.main() @ &m: Game1.r \in Log.qs].
239proof.
240byequiv=> //; proc.
241inline BR93(RO).enc BR93(RO).keygen.
242(* Until the replaced RO call, the two games are in sync.               *)
243(*        In addition, the log's contents coincide with the RO queries. *)
244seq  8  5: (   ={glob A, glob RO, glob Log, pk, sk, b}
245            /\ pk0{1} = pk{2}
246            /\ m{1} = (b?m0:m1){2}
247            /\ r{1} = Game1.r{2}
248            /\ (forall x, x \in Log.qs{1} <=> x \in (dom RO.m){1})).
249+ (* EX: Prove it. *) admit.
250(* We now deal with everything that happens after the programs differ: *)
251(*   - until r gets queried to the random oracle by the adversary      *)
252(*     (and if it wasn't already queried by a1), we guarantee that the *)
253(*     random oracles agree except on r                                *)
254(*   - if the adversary queries r to the random oracle (or if it has   *)
255(*     already done so in a1), we give up                              *)
256(* Because we reason up to bad, we need to prove that bad is stable    *)
257(* and that the adversary and its oracles are lossless                 *)
258call (_: Game1.r \in Log.qs,
259         eq_except RO.m{1} RO.m{2} (pred1 Game1.r{2})).
260+ (* EX: Prove losslessness of the adversary. *) admit.
261+ (* EX: Prove up to bad equivalence of oracles. *) admit.
262+ (* EX: Prove losslessness of o on the left. *) admit.
263+ (* EX: Prove that o on the right preserves bad with probability 1 *) admit.
264  (* EX: Do it again, using conseq to separate losslessness from monotonicity. *)
265inline RO.o; case: ((r \in (dom RO.m)){1}).
266+ (* EX: Oh no! Bad has occurred! Finish the proof! *) admit.
267(* EX: The good news? Bad has not occurred. The bad news? You've got to prove more things! *) admit.
268qed.
269
270(* Step 2: replace h ^ m with h in the challenge encryption            *)
271local module Game2 = {
272  var r: rand
273
274  proc main() = {
275    var pk, sk, m0, m1, b, h, c, b';
276                Log(RO).init();
277    (pk,sk)  <$ dkeys;
278    (m0,m1)  <@ A(Log(RO)).a1(pk);
279    b        <$ {0,1};
280
281    r        <$ drand;
282    h        <$ dptxt;
283    c        <- ((f pk r),h);
284
285    b'       <@ A(Log(RO)).a2(c);
286    return b' = b;
287  }
288}.
289
290local equiv eq_Game1_Game2: Game1.main ~ Game2.main:
291  ={glob A} ==> ={glob Log, res} /\ Game1.r{1} = Game2.r{2}.
292proof.
293(* EX: Prove it! You will need to use `rnd` in a clever way! *) admit.
294qed.
295
296local lemma pr_Game1_Game2 &m:
297  Pr[Game1.main() @ &m: res] = Pr[Game2.main() @ &m: res].
298proof. (* EX: Prove it. *) admit. qed.
299
300local lemma pr_bad_Game1_Game2 &m:
301    Pr[Game1.main() @ &m: Game1.r \in Log.qs]
302  = Pr[Game2.main() @ &m: Game2.r \in Log.qs].
303proof. (* EX: Prove it. *) admit. qed.
304
305local lemma pr_Game2 &m: Pr[Game2.main() @ &m: res] = 1%r / 2%r.
306proof.
307(* EX: Prove it. *) admit.
308qed.
309
310(* Step 3: The reduction step -- if A queries the RO with the randomness *)
311(*     used to encrypt the challenge, then I(A) inverts the OW challenge *)
312(* We need a version of the one-way game where the challenge is a global *)
313local module OWr (I : Inverter) = {
314  var x : rand
315
316  proc main() : bool = {
317    var x', pk, sk;
318
319    (pk,sk) <$ dkeys;
320    x       <$ drand;
321    x'      <@ I.invert(pk,f pk x);
322    return (x = x');
323  }
324}.
325
326(* We can easily prove that it is strictly equivalent to OW              *)
327local lemma OW_OWr &m (I <: Inverter {OWr}):
328  Pr[OW(I).main() @ &m: res]
329  = Pr[OWr(I).main() @ &m: res].
330proof. by byequiv=> //=; sim. qed.
331
332local lemma pr_Game2_OW &m:
333  Pr[Game2.main() @ &m: Game2.r \in Log.qs]
334  <= Pr[OW(I(A)).main() @ &m: res].
335proof.
336rewrite (OW_OWr &m (I(A))). (* Note: we proved it forall (abstract) I    *)
337byequiv => //=; proc; inline *; wp.
338conseq
339  (_ : _ ==>
340       support dkeys (pk0{2}, sk{2}) /\
341       Game2.r{1} = OWr.x{2} /\ Log.qs{1} = Log.qs{2} /\
342       y{2} = f pk0{2} Game2.r{1}).
343+ move=> /> qs x pk sk vk x_in_qs; pose P := fun p => f _ p = _.
344  have h := nth_find witness P qs _.
345  + by rewrite hasP; exists x.
346  apply/(fI pk).
347  + by exists sk.
348  by rewrite h.
349(* rest of proof *)
350call (: ={glob Log, glob RO}); 1: by sim.
351swap{1} 6 -2.
352auto; call (: ={glob Log, glob RO}); 1: by sim.
353by auto=> /> [pk sk] ->; rewrite dbool_ll.
354qed.
355
356lemma Reduction &m:
357  Pr[BR93_CPA(A).main() @ &m : res] - 1%r/2%r
358  <= Pr[OW(I(A)).main() @ &m: res].
359proof.
360smt(pr_Game0_Game1 pr_Game1_Game2 pr_bad_Game1_Game2 pr_Game2 pr_Game2_OW).
361qed.
362end section.
363end BR93.
364
365(* We now consider a concrete instance:                                 *)
366(*   - plaintexts are bitstrings of length k > 0                        *)
367(*   - nonces are bitstrings of length l > 0                            *)
368(*   - ciphertexts are bitstrings of length n = k + l                   *)
369
370(* Plaintexts                                                           *)
371op k : { int | 0 < k } as gt0_k.
372
373clone import BitWord as Plaintext with
374  op n <- k
375proof gt0_n by exact/gt0_k
376rename
377  "word" as "ptxt"
378  "dunifin" as "dptxt".
379import DWord.
380
381(* Nonces                                                               *)
382op l : { int | 0 < l } as gt0_l.
383
384clone import BitWord as Randomness with
385  op n <- l
386proof gt0_n by exact/gt0_l
387rename
388  "word" as "rand"
389  "dunifin" as "drand".
390import DWord.
391
392(* Ciphertexts                                                          *)
393op n = l + k.
394lemma gt0_n: 0 < n by smt(gt0_k gt0_l).
395
396clone import BitWord as Ciphertext with
397  op n <- n
398proof gt0_n by exact/Self.gt0_n
399rename "word" as "ctxt".
400
401(* Parsing and Formatting                                               *)
402op (||) (r:rand) (p:ptxt) : ctxt = mkctxt ((ofrand r) ++ (ofptxt p)).
403op parse (c:ctxt): rand * ptxt =
404  (mkrand (take l (ofctxt c)),mkptxt (drop l (ofctxt c))).
405
406lemma parseK r p: parse (r || p) = (r,p).
407proof.
408rewrite /parse /(||) ofctxtK 1:size_cat 1:size_rand 1:size_ptxt //=.
409by rewrite take_cat drop_cat size_rand take0 drop0 cats0 mkrandK mkptxtK.
410qed.
411
412lemma formatI (r : rand) (p : ptxt) r' p':
413  (r || p) = (r' || p') => (r,p) = (r',p').
414proof. by move=> h; rewrite -(@parseK r p) -(@parseK r' p') h. qed.
415
416(* A set `pkey * skey` of keypairs, equipped with                       *)
417(*                         a lossless, full, uniform distribution dkeys *)
418type pkey, skey.
419op dkeys: { (pkey * skey) distr |    is_lossless dkeys
420                                  /\ is_funiform dkeys } as dkeys_llfuni.
421
422(* A family `f` of trapdoor permutations over `rand`,                   *)
423(*        indexed by `pkey`, with inverse family `fi` indexed by `skey` *)
424op f : pkey -> rand -> rand.
425op fi: skey -> rand -> rand.
426axiom fK pk sk x: (pk,sk) \in dkeys => fi sk (f pk x) = x.
427
428(* Random Oracle                                                        *)
429clone import ROM.Lazy as H with
430  type from      <- rand,
431  type to        <- ptxt,
432  op   dsample _ <- dptxt.
433
434(* A Definition for OWTP Security                                       *)
435module type Inverter = {
436  proc invert(pk:pkey, x:rand): rand
437}.
438
439module Exp_OW (I : Inverter) = {
440  proc main(): bool = {
441    var pk, sk, x, x';
442
443    (pk,sk) <$ dkeys;
444    x       <$ drand;
445    x'      <@ I.invert(pk,f pk x);
446    return (x = x');
447  }
448}.
449
450(* A Definition for CPA Security                                        *)
451module type Scheme (RO : Oracle) = {
452  proc keygen(): (pkey * skey)
453  proc enc(pk:pkey, m:ptxt): ctxt
454}.
455
456module type Adv (ARO : ARO)  = {
457  proc a1(p:pkey): (ptxt * ptxt)
458  proc a2(c:ctxt): bool
459}.
460
461module CPA (O : Oracle) (S:Scheme) (A:Adv) = {
462  proc main(): bool = {
463    var pk, sk, m0, m1, c, b, b';
464
465               O.init();
466    (pk,sk) <@ S(O).keygen();
467    (m0,m1) <@ A(O).a1(pk);
468    b       <$ {0,1};
469    c       <@ S(O).enc(pk,b?m0:m1);
470    b'      <@ A(O).a2(c);
471    return b' = b;
472  }
473}.
474
475(* And a definition for the concrete Bellare-Rogaway Scheme             *)
476module (BR : Scheme) (H : Oracle) = {
477  proc keygen():(pkey * skey) = {
478    var pk, sk;
479
480    (pk,sk) <$ dkeys;
481    return (pk,sk);
482  }
483
484  proc enc(pk:pkey, m:ptxt): ctxt = {
485    var h, r;
486
487    r <$ drand;
488    h <@ H.o(r);
489    return ((f pk r) || m +^ h);
490  }
491
492  proc dec(sk:skey, c:ctxt): ptxt = {
493    var r, p, h;
494
495    (r,p) <- parse c;
496    r     <- fi sk r;
497    h     <@ H.o(r);
498    return p +^ h;
499  }
500}.
501
502(* And our inverter                                                     *)
503module I (A:Adv) (H : Oracle) = {
504  var qs : rand list
505
506  module QRO = {
507    proc o(x:rand) = {
508      var r;
509
510      qs <- x::qs;
511      r  <@ H.o(x);
512      return r;
513    }
514  }
515
516  proc invert(pk:pkey,y:rand): rand = {
517    var x, m0, m1, h, b;
518
519    qs      <- [];
520               H.init();
521    (m0,m1) <@ A(QRO).a1(pk);
522    h       <$ dptxt;
523    b       <@ A(QRO).a2(y || h);
524    x       <- nth witness qs (find (fun p => f pk p = y) qs);
525
526    return x;
527  }
528}.
529
530(* We will need to turn a concrete CPA adversary into an abstract one.  *)
531(*      We do not need to do it for the inverter as the types coincide. *)
532module A_CPA (A : Adv) (H : ARO) = {
533  proc a1 = A(H).a1
534
535  proc a2(c:rand * ptxt): bool = {
536    var b;
537
538    b <@ A(H).a2(c.`1 || c.`2);
539    return b;
540  }
541}.
542
543section.
544declare module A : Adv { RO, I }.
545
546axiom A_a1_ll (O <: ARO {A}): islossless O.o => islossless A(O).a1.
547axiom A_a2_ll (O <: ARO {A}): islossless O.o => islossless A(O).a2.
548
549local clone import BR93 as Instance with
550  type pkey  <- pkey,
551  type skey  <- skey,
552  op   dkeys <- dkeys,
553  op   f     <- f,
554  op   fi    <- fi,
555  type ptxt  <- ptxt,
556  op   (+^)  <- Plaintext.(+^),
557  op   dptxt <- dptxt,
558  type rand  <- rand,
559  op   drand <- drand
560proof addA, addC, addKp, dptxt_llfuuni, drand_lluni, dkeys_llfuni, fK.
561realize addA          by move=> p1 p2 p3; algebra.
562realize addC          by move=> p1 p2; algebra.
563realize addKp         by move=> p1 p2; algebra.
564realize dptxt_llfuuni by smt(@Plaintext.DWord).
565realize drand_lluni   by smt(@Randomness.DWord).
566realize dkeys_llfuni  by exact/dkeys_llfuni.
567realize fK            by exact/fK.
568
569lemma Reduction &m:
570     Pr[CPA(RO, BR, A).main() @ &m : res] - 1%r / 2%r
571  <= Pr[Exp_OW(Self.I(A, RO)).main() @ &m : res].
572proof.
573have <-:   Pr[BR93_CPA(A_CPA(A)).main() @ &m: res]
574         = Pr[CPA(RO,BR,A).main() @ &m: res].
575+ (* EX: Wait, what? Prove it! *) admit.
576have <-:   Pr[OW_rand.OW(I(A_CPA(A))).main() @ &m: res]
577         = Pr[Exp_OW(Self.I(A,RO)).main() @ &m: res].
578+ (* EX: Prove it. *) admit.
579apply/(Reduction (A_CPA(A)) _ _ &m).
580+ (* EX: discharge both losslessness conditions *) admit.
581admit.
582qed.
583end section.