CoursePisa2014: prhl_full_clean.ec

File prhl_full_clean.ec, 8.5 KB (added by François Dupressoir, 3 years ago)

Exercise sheet 4 day 3

Line 
1require import Option.
2require import Real.
3require import Array.
4require import Int.
5require import FMap.
6require import FSet.
7require import Distr.
8require (*--*) Upto.
9require (*--*) Word.
10require (*--*) PKE.
11
12theory OW.
13  type t.
14  op sample_t : t distr.
15
16  type pkey.
17  type skey.
18  op keypairs: (pkey * skey) distr.
19  axiom keypair_lossless : mu keypairs True = 1%r.
20
21  op f : pkey -> t -> t.
22  op finv : skey -> t -> t.
23
24  axiom finvof pk sk x:
25    support keypairs (pk,sk) => finv sk (f pk x) = x.
26
27  axiom fofinv pk sk x:
28     support keypairs (pk,sk) => f pk (finv sk x) = x.
29
30  lemma f_pk_inj x y pk sk: 
31    support keypairs (pk,sk) =>
32    f pk x = f pk y =>
33    x = y.
34  proof.
35    move=> Hsupp Heqf.
36    rewrite -(finvof pk sk _ _);first smt.
37    rewrite -(finvof pk sk y _);first smt.
38    rewrite Heqf;smt.
39  qed.
40
41  module type Inverter = {
42    proc inverter(pk : pkey, y : t) : t
43  }.
44
45  module OW(I :Inverter) ={
46    proc main() : bool ={
47      var x, x', pk, sk;
48
49      x       = $sample_t;
50      (pk,sk) = $keypairs;
51      x'      = I.inverter(pk,(f pk x));
52      return (x = x');
53    }
54  }.
55end OW.
56
57(* Starting br93 *)
58
59theory BR93.
60
61type randomness.
62op l : int. 
63op sample_r : randomness distr.
64clone import Word as Randomness
65with
66  type word <- randomness,
67  op length <- l,
68  op Dword.dword <- sample_r.
69
70type ciphertext.
71op n : int. 
72clone import Word as Ciphertext
73with
74  type word <- ciphertext,
75  op length <- n.
76
77type plaintext. 
78op k : int.
79op sample_p : plaintext distr.
80clone import Word as Plaintext
81with
82  type word <- plaintext,
83  op length <- k,
84  op Dword.dword <- sample_p.
85 
86axiom sizes : k + l = n.
87
88op (||) (x : randomness, y : plaintext) : ciphertext =
89  Ciphertext.from_bits ((to_bits x) || (to_bits y)).
90
91op projRand(c : ciphertext) : randomness =
92  Randomness.from_bits (sub (to_bits c) 0 l).
93
94op projPlain(c : ciphertext) : plaintext =
95  Plaintext.from_bits (sub (to_bits c) l k).
96
97clone export OW
98with
99  type t <- randomness,
100  op sample_t <- sample_r.
101
102clone export Upto
103with
104  type from <- randomness, 
105  type to <- plaintext,
106  op dsample <- sample_p,
107  type ROM.UpTo.result <- bool.
108
109  import ROM. 
110  import Pair.
111
112  (* Try the following command *)
113  print theory Upto.
114
115  clone PKE
116  with
117    type pkey <- pkey,
118    type skey <- skey,
119    type plaintext <- plaintext,
120    type ciphertext <- ciphertext.
121
122  module BR(R : Oracle) : PKE.Scheme = {
123    proc kg(): pkey * skey = {
124      var pk, sk;
125
126      R.init();
127      (pk,sk) = $keypairs;
128      return (pk,sk);
129    }
130 
131    proc enc(pk:pkey, m:plaintext): ciphertext = {
132      var h, r;
133
134      r = $sample_r; 
135      h  = R.o(r);
136      return ((f pk r) ||   m ^^ h);
137    }
138 
139    proc dec(sk:skey, c : ciphertext) : plaintext option = {
140      var h;
141
142      h = R.o(finv sk (projRand c));
143      return (Some (projPlain c ^^ h));
144    }
145  }.
146
147  module BRo = BR(RO).
148  module CPA = PKE.CPA(BRo).
149
150  module type AdversaryRO (R:AdvRO) = { 
151    proc choose(pk:pkey)     : plaintext * plaintext
152    proc guess(c:ciphertext) : bool                 
153  }.
154
155  section.
156    import UpTo. 
157    declare module A : AdversaryRO{RO}.
158
159    local module AR = A(RO). 
160
161    (* Fill the body of the function a2 such that the lemma equiv_CPA_G1
162       become provable *)
163
164    local module G1Adv (R:AdvRO) : UpTo.Adv(R) = { 
165      var pk : pkey
166      var sk : skey
167      var m, m0, m1 : plaintext
168      var c : ciphertext
169      var b, b' : bool
170      var r : randomness
171
172      module AR = A(R)
173
174      proc a1 () : randomness = {
175        (pk, sk) = $keypairs;
176        (m0, m1) = AR.choose(pk);
177        b        = ${0,1};
178        m        = b ? m1 : m0;
179        r        = $sample_r; 
180        return r;
181      }   
182     
183      proc a2 (to: plaintext) : bool = {
184(* FILL ME *)
185        return b' = b;
186      }
187    }.
188
189    local module G1 = Gfail(G1Adv).
190
191    (* prove the following (you can try the eqobs_in tactic) *)
192    local equiv equiv_CPA_G1 : CPA(AR).main ~ G1.main :
193            ={glob A} ==>res{1} = snd res{2}.
194    proof.
195(* FILL ME *)
196    qed.
197
198    local lemma pr1 &m :
199       Pr[ CPA(AR).main() @ &m : res ] = Pr[ G1.main() @ &m : snd res].
200    proof.
201(* FILL ME *)
202    qed.
203
204    local module G1' = Gfail'(G1Adv).
205
206    (* Fill the proof using the lemma "Fail" *)
207    print axiom Fail.
208
209    local lemma equiv_G1_G1' : 
210      (forall (RO <: AdvRO{A}), islossless RO.o => islossless A(RO).guess) =>
211      equiv [ G1.main ~ G1'.main : ={glob G1Adv} ==> 
212               let (fr,xxx) = res{2} in
213               !(mem fr (dom RO.m)){2} => ={res, glob G1Adv} /\ eq_except RO.m{1} RO.m{2} fr].
214    proof.
215(* FILL ME *)
216    qed.
217
218    local lemma pr2 &m :
219      (forall (RO0 <: AdvRO{A}), islossless RO0.o => islossless A(RO0).guess) =>
220      Pr[ G1.main() @ &m : snd res] <= Pr[ G1'.main() @ &m : snd res] +
221                                       Pr[ G1'.main() @ &m : mem (fst res) (dom RO.m)].
222    proof.     
223     intros => ll.
224     apply (Real.Trans _ (Pr[ G1'.main() @ &m : snd res \/ mem (fst res) (dom RO.m)]) _).
225(* FILL ME *)
226    qed.
227
228    local module G2 = {
229      var pk : pkey
230      var sk : skey
231      var m, m0, m1, h: plaintext
232      var c : ciphertext
233      var b, b' : bool
234      var r : randomness
235
236      proc main () : bool =  {
237        RO.init();
238        (pk, sk) = $keypairs;
239        (m0, m1) = AR.choose(pk);
240        r        = $sample_r; 
241        h        = $sample_p;
242        c        = ((f pk r) || h);
243        b'       = AR.guess(c);
244        b        = ${0,1};
245        return b' = b;
246      }
247    }.
248
249    local equiv G1'_G2 : G1'.main ~ G2.main : ={glob A} ==> 
250         ={RO.m} /\ let (r1,res1) = res{1} in
251                 r1 = G2.r{2} /\ res1 = res{2}.
252    proof. 
253(* FILL ME *)
254    qed.
255   
256    local lemma pr3 &m :
257      Pr[ G1'.main() @ &m : snd res] + Pr[ G1'.main() @ &m : mem (fst res) (dom RO.m)] =
258      Pr[ G2.main() @ &m : res]  + Pr[ G2.main() @ &m : mem G2.r (dom RO.m)].
259    proof.
260     by (congr; byequiv G1'_G2 => //; smt).
261    qed.
262   
263    local lemma prob_half &m : 
264      (forall (RO <: AdvRO{A}), islossless RO.o => islossless A(RO).choose) =>
265      (forall (RO <: AdvRO{A}), islossless RO.o => islossless A(RO).guess) =>
266      Pr[G2.main()  @ &m : res] = 1%r / 2%r.
267    proof.
268      admit.
269      (* The proof will be done tomorrow *)
270    qed.
271
272    module Inv(A_ : AdversaryRO) : Inverter = {
273
274      module A = A_(RO)
275
276      proc inverter(pk : pkey,y : randomness) : randomness ={
277        var m0, m1, h, b, x;
278
279        RO.init();
280        (m0,m1)  = A.choose(pk);
281        h = $sample_p;
282        b  = A.guess(y || h);
283        x = oget (find (fun p0 p1,f pk p0 = y) RO.m);
284        return (x);
285      }
286
287    }.
288
289    (* It can help to use f_pk_inj at some point *)
290    local equiv G2_Inv : G2.main ~ OW(Inv(A)).main : 
291      ={glob A} ==> ((mem G2.r (dom RO.m)){1} => res{2}).
292    proof.
293      proc.
294      rnd{1}.
295      conseq (_ : _ ==> mem G2.r{1} (dom RO.m{1}) => x{2} = x'{2}).
296        move=> &1 &2 H; split; [apply Bool.Dbool.lossless | ].
297        move=> ll b b_in_buf; apply H.
298      inline{2} Inv(A).inverter. 
299      wp; conseq (_ : _ ==> 
300                      support keypairs (pk0,sk){2} /\
301                      ={RO.m} /\ y{2} = f pk0{2} x{2} /\
302                      x{2} = G2.r{1}).
303        move=> &1 &2 [H [-> [H1 H2]]] H3.
304        cut xo_construct: forall (xo:randomness option), xo <> None => (exists x, xo = Some x).
305          by elim=> //; smt.
306        cut [x0 x0_find]: exists x0, find (fun p0 (p1:plaintext), f pk0{2} p0 = y{2}) RO.m{2} = Some x0.
307          by apply xo_construct; apply find_in; smt.
308        cut:= find_cor (fun p0 (p1:plaintext), f pk0{2} p0 = y{2}) RO.m{2} x0 _=> //= [[x0_in_m]].
309        by rewrite /oget x0_find H1 /= (eq_sym x{2}); apply (f_pk_inj _ _ _ sk{2}).
310(* FILL ME *)
311   qed.
312 
313   local lemma proba_reduction &m: 
314      Pr[G2.main() @ &m : mem G2.r (dom RO.m)] <=
315      Pr[OW(Inv(A)).main() @ &m : res]
316    by byequiv G2_Inv.
317
318   axiom Lc :
319      forall (RO0 <: AdvRO{A}), islossless RO0.o => islossless A(RO0).choose.
320
321   axiom Lg :
322      forall (RO0 <: AdvRO{A}), islossless RO0.o => islossless A(RO0).guess.
323
324   lemma red_aux &m: 
325     Pr[CPA(A(RO)).main() @ &m : res] <= 
326       1%r /2%r + Pr[OW(Inv(A)).main() @ &m : res].
327   proof.
328    rewrite -(prob_half &m) //. apply Lc.  apply Lg.
329    rewrite (pr1 &m) //.
330    apply (Real.Trans _ (Pr[ G1'.main() @ &m : snd res] +
331                         Pr[ G1'.main() @ &m : mem (fst res) (dom RO.m)])).
332(* FILL ME *)
333   qed.
334
335
336   lemma reduction &m: 
337       exists (I <: Inverter),
338         Pr[CPA(A(RO)).main() @ &m : res] <=  1%r /2%r + Pr[OW(I).main() @ &m : res].
339   proof.
340(* FILL ME *)
341   qed.
342
343end section.
344 
345end BR93.
346
347
348print axiom BR93.reduction. 
349