SchoolUMD2015: BR93_filled.ec

File BR93_filled.ec, 9.4 KB (added by François Dupressoir, 2 years ago)

Filled in proofs for BR93.

Line 
1require import Fun Bool Int Real Distr List FSet Array FMap.
2require (*--*) AWord ROM.
3
4(** We consider three lengths of bitstrings **)
5op k : { int | 0 < k } as k_pos. (* size of message *)
6op l : { int | 0 < l } as l_pos. (* size of randomness *)
7op n : { int | 0 < n } as n_pos. (* size of cipher *)
8
9axiom sizes : k + l = n.
10
11clone import AWord as Plaintext with
12  op length = k
13proof leq0_length by smt.
14
15clone import AWord as Ciphertext with
16  op length = n
17proof leq0_length by smt.
18
19clone import AWord as Randomness with
20  op length = l
21proof leq0_length by smt.
22
23type plaintext = Plaintext.word.
24type ciphertext = Ciphertext.word.
25type randomness = Randomness.word.
26
27(* We only need distributions on plaintexts and nonces *)
28op uniform      = Plaintext.Dword.dword.
29op uniform_rand = Randomness.Dword.dword.
30
31(* We have operators that combine them *)
32op (||) (x:randomness) (y:plaintext):ciphertext =
33 Ciphertext.from_bits ((to_bits x) || (to_bits y)).
34
35(** Please ignore **)
36lemma find_unique x' (p: 'a -> bool) (xs : 'a list):
37  (forall (x : 'a), p x => x = x') =>
38  mem x' xs => p x' => find p xs = Some x'.
39proof.
40  move=> p_unique x'_in_m p_x'.
41  case {-1}(find p xs) (Logic.eq_refl (find p xs))=> //=.
42    smt.
43    by move=> x /List.find_cor [] _ /p_unique.
44qed.
45
46(*** One way trapdoor permutation (pre-instantiated) ***)
47(**  [See theory OW.ec] **)
48theory OWTP.
49  type pkey, skey.
50
51  op keypairs: (pkey * skey) distr.
52  axiom keypair_lossless : is_lossless keypairs.
53
54  op f       : pkey -> randomness -> randomness.
55  op finv    : skey -> randomness -> randomness.
56
57  axiom finvof pk sk x:
58   support keypairs (pk,sk) =>
59   finv sk (f pk x) = x.
60
61  axiom fofinv pk sk x:
62   support keypairs (pk,sk) =>
63   f pk (finv sk x) = x.
64
65  lemma f_injective sk pk x y:
66    support keypairs (pk,sk) =>
67    f pk x = f pk y =>
68    x = y.
69  proof.
70    move=> Hsupp Heqf.
71    by rewrite -(finvof pk sk) // Heqf finvof.
72  qed.
73
74  module type Inverter = {
75    proc i(pk:pkey,y:randomness): randomness
76  }.
77
78  module OW(I:Inverter) = {
79    var r:randomness
80
81    proc main(): bool = {
82      var x', pk, sk;
83
84      (pk,sk) = $keypairs;
85      r       = $uniform_rand;
86      x'      = I.i(pk,f pk r);
87      return (r = x');
88    }
89  }.
90
91  (** f is a secure OWTP if, for any inverter I,
92        Adv^{OW}^f(I) = Pr[OW(I).main() @ &m: res]
93      is small. **)
94end OWTP.
95import OWTP.
96
97(*** We make use of a hash function (ROM) from randomness to
98     plaintext. We let the adversary query it qH times at most. ***)
99op qH : { int | 0 < qH } as qH_pos.
100
101clone import ROM.ListLog as RandOrcl_BR with
102  type from  <- randomness, 
103  type to    <- plaintext,
104  op dsample <- fun (x:randomness) => uniform,
105  op qH      <- qH.
106import Lazy.
107import Types.
108
109(*** We can now define what it means to be a CPA-secure public-key encryption scheme ***)
110(**  [See theory PKE.ec] **)
111module type Scheme(RO : Oracle) = {
112  proc kg(): (pkey * skey)
113  proc enc(pk:pkey, m:plaintext): ciphertext
114}.
115
116module type Adv(ARO: ARO)  = {
117  proc a1(p:pkey)      : (plaintext * plaintext)
118  proc a2(c:ciphertext): bool
119}.
120
121module CPA(S:Scheme, A:Adv) = {
122  module ARO = Log(RO)
123  module A = A(ARO)
124  module SO = S(RO)
125
126  proc main(): bool = {
127    var pk, sk, m0, m1, c, b, b';
128
129    ARO.init();
130    (pk,sk)  = SO.kg();
131    (m0,m1)  = A.a1(pk);
132    b = ${0,1}; 
133    c  = SO.enc(pk,b?m0:m1);
134    b' = A.a2(c);
135    return b' = b;
136  } 
137}.
138
139(** A Scheme E is IND-CPA secure if, for any A,
140      Adv^{CPA}_{S}(A) = `|Pr[CPA(S,A).main() @ &m: res] - 1/2|
141    is small. **)
142
143module BR(R:Oracle): Scheme(R) = {
144  proc kg():(pkey * skey) = {
145    var pk, sk;
146
147    (pk,sk) = $keypairs;
148    return (pk,sk);
149  }
150 
151  proc enc(pk:pkey, m:plaintext): ciphertext = {
152    var h, r;
153
154    r = $uniform_rand; 
155    h = R.o(r);
156    return ((f pk r) ||   m ^ h);
157  }
158}.
159
160(** Given a CPA adversary A, we construct a OW inverter **)
161module BR_OW(A:Adv): Inverter = {
162  module ARO = Log(RO)
163  module A = A(ARO)
164
165  var x:randomness
166
167  proc i(pk:pkey,y:randomness): randomness = {
168    var m0,m1,h,b;
169
170    ARO.init();
171    (m0,m1) = A.a1(pk);
172    h = $uniform; 
173    b = A.a2(y || h);
174    x = oget (find (fun p => f pk p = y) ARO.qs);
175    return x;
176  }
177}.
178
179(** such that Adv^{CPA}_{S}(A) <= Adv^{OW}^{f}(I(A)).
180    We now prove this bound. **)
181lemma lossless_ARO_init: islossless Log(RO).init.
182proof. by apply/(Log_init_ll RO)/RO_init_ll. qed.
183
184lemma lossless_ARO_o : islossless Log(RO).o.
185proof. by apply/(Log_o_ll RO)/RO_o_ll/Plaintext.Dword.lossless. qed.
186
187section.
188  (* Forall CPA adversary A whose memory footprint is disjoint from that of RO, Log and OW *)
189  declare module A : Adv {RO,Log,OW}.
190
191  (* and whose two procedures as lossless provided the random oracle is *)
192  axiom a1_ll (O <: ARO{A}): islossless O.o => islossless A(O).a1.
193  axiom a2_ll (O <: ARO{A}): islossless O.o => islossless A(O).a2.
194
195  (* the following lemmas hold on the following constructions *)
196
197  (** Step 1: replace RO call with random sampling **)
198  local module BR1(R:Oracle): Scheme(R) = {
199    var r:randomness
200
201    proc kg = BR(R).kg
202
203    proc enc(pk:pkey, m:plaintext): ciphertext = {
204      var h;
205
206      r = $uniform_rand;
207      h = $uniform;
208      return ((f pk r) || m ^ h);
209    }
210  }.
211
212  (** The success probability of A in CPA(BR) is bounded by
213      the success probability of A in CPA(BR1) plus the probability
214      of the adversary querying the RO with the randomness used in
215      the challenge encryption. **)
216  local lemma BR_BR1 &m:
217    Pr[CPA(BR,A).main() @ &m: res]
218    <= Pr[CPA(BR1,A).main() @ &m: res]
219       + Pr[CPA(BR1,A).main() @ &m: mem BR1.r Log.qs].
220  proof.
221    byequiv=> //.
222    proc. inline CPA(BR,A).SO.enc CPA(BR1,A).SO.enc.
223    (* Until the adversary queries the ROM with r, knowing that
224       the two ROMs agree on all points except r is sufficient
225       to prove the equivalence of the adversary's views        *)
226     inline RO.o.
227     call (_: mem BR1.r Log.qs,
228                 eq_except RO.m{1} RO.m{2} BR1.r{2}
229              /\ (forall x, mem x Log.qs{2} <=> mem x (dom RO.m){2})).
230       exact/a2_ll.
231       proc. inline *.
232       wp. rnd. wp. skip. smt.
233       move=> &2 _; proc. inline *. auto. smt.
234       move=> &1. proc. inline *. auto. smt.
235     wp. rnd. wp. rnd.
236     wp. rnd.
237     call (_:    ={RO.m}
238              /\ (forall x, mem x Log.qs{2} <=> mem x (dom RO.m){2})).
239       proc. inline *. auto. smt.
240     inline*. auto. smt.
241  qed.
242
243  (** Step 2: replace h ^ m with h in challenge encryption **)
244  local module BR2(R:Oracle): Scheme(R) = {
245    var r:randomness
246
247    proc kg():(pkey * skey) = {
248      var pk, sk;
249
250      (pk,sk) = $keypairs;
251      return (pk,sk);
252    }
253
254    proc enc(pk:pkey, m:plaintext): ciphertext = {
255      var h;
256
257      r = $uniform_rand; 
258      h = $uniform; 
259      return ((f pk r) || h);
260    }
261  }.
262
263  local equiv eq_BR1_BR2:
264    CPA(BR1,A).main ~ CPA(BR2,A).main:
265      ={glob A} ==> ={res, Log.qs} /\ BR1.r{1} = BR2.r{2}.
266   proof.
267    proc. inline *.
268    seq 9 9: (={glob A, Log.qs, RO.m, pk1, b} /\ BR1.r{1} = BR2.r{2}).
269      sim.
270    call (_: ={RO.m, Log.qs}).
271      proc. inline *. auto.
272    wp. rnd (fun x => m{1} ^ x).
273    auto. progress; smt.
274  qed.
275
276  (* The success probabilities in both games are the same *)
277  local lemma BR1_BR2 &m:
278    Pr[CPA(BR1,A).main() @ &m: res]
279    = Pr[CPA(BR2,A).main() @ &m: res].
280  proof. by byequiv eq_BR1_BR2. qed.
281(*    byequiv=> //.
282    proc. inline *.
283    seq 9 9: (={glob A, RO.m, pk1, b} /\ BR1.r{1} = BR2.r{2}).
284      sim.
285    call (_: ={RO.m}).
286      proc. inline *. auto.
287    wp. rnd (fun x => m{1} ^ x).
288    auto. progress; smt.
289*)
290
291  (** Exercise: What single "equiv" lemma could be used to prove both
292      BR1_BR2 and BR1_BR2_bad in one? Prove it and use it to prove
293      BR1_BR2_bad and BR1_BR2. **)
294
295  (* The probability of the failure event is the same in both games *)
296  local lemma BR1_BR2_bad &m:
297    Pr[CPA(BR1,A).main() @ &m: mem BR1.r Log.qs]
298    = Pr[CPA(BR2,A).main() @ &m: mem BR2.r Log.qs].
299  proof. by byequiv eq_BR1_BR2. qed.
300
301  (** We can now prove that the success probability of A in CPA(BR2) is exactly 1/2 **)
302  local lemma pr_BR2_res &m: Pr[CPA(BR2,A).main() @ &m: res] = 1%r / 2%r.
303  proof.
304    byphoare=> //.
305    proc.
306    inline CPA(BR2,A).SO.enc.
307    swap 6 4. wp.
308    swap 4 5. rnd.
309    conseq (_: _ ==> true).
310      progress. have ->: (fun x => b'{hr} = x) = pred1 b'{hr}.
311        by rewrite pred1E; apply fun_ext=> x.
312      smt.
313    call (a2_ll (Log(RO)) lossless_ARO_o).
314    auto.
315    call (a1_ll (Log(RO)) lossless_ARO_o).
316    inline *; auto.
317    smt.
318  qed.
319
320  local lemma pr_BR_BR2 &m:
321    Pr[CPA(BR,A).main() @ &m: res] - 1%r/2%r
322    <= Pr[CPA(BR2,A).main() @ &m: mem BR2.r Log.qs].
323  proof. smt. qed.
324
325  (** Step 3: Finally, we can do the reduction and prove that whenever
326      A queries the RO with the randomness used in the challenge
327      encryption, BR_OW(A) inverts the OW challenge. **)
328  local lemma BR2_OW &m:
329    Pr[CPA(BR2,A).main() @ &m: mem BR2.r Log.qs]
330    <= Pr[OW(BR_OW(A)).main() @ &m: res].
331  proof.
332    byequiv=> //.
333    proc. inline *.
334    wp. call(_: ={RO.m, Log.qs}).
335      sim.
336    wp. rnd.
337    swap{1} 9 -5.
338    wp. rnd{1}. call(_: ={RO.m, Log.qs}).
339      sim.
340    auto.
341    progress.
342      smt.
343      have ->: (fun p => f pk0sk0L.`1 p = f pk0sk0L.`1 rL) = (fun p => p = rL).
344         apply fun_ext=> x; rewrite eq_iff; split=> //.
345          apply (f_injective pk0sk0L.`2). smt.
346        rewrite (find_unique rL) //.
347  qed.
348
349  lemma Reduction &m:
350    Pr[CPA(BR,A).main() @ &m : res] - 1%r/2%r
351    <= Pr[OW(BR_OW(A)).main() @ &m: res].
352  proof. smt. qed.
353end section.