SchoolUMD2015: BR93_erased.ec

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

Erased version of 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    (* Until the adversary queries the ROM with r, knowing that
222       the two ROMs agree on all points except r is sufficient
223       to prove the equivalence of the adversary's views        *)
224  qed.
225
226  (** Step 2: replace h ^ m with h in challenge encryption **)
227  local module BR2(R:Oracle): Scheme(R) = {
228    var r:randomness
229
230    proc kg():(pkey * skey) = {
231      var pk, sk;
232
233      (pk,sk) = $keypairs;
234      return (pk,sk);
235    }
236
237    proc enc(pk:pkey, m:plaintext): ciphertext = {
238      var h;
239
240      r = $uniform_rand; 
241      h = $uniform; 
242      return ((f pk r) || h);
243    }
244  }.
245
246  (* The success probabilities in both games are the same *)
247  local lemma BR1_BR2 &m:
248    Pr[CPA(BR1,A).main() @ &m: res]
249    = Pr[CPA(BR2,A).main() @ &m: res].
250  proof.
251  qed.
252
253  (* The probability of the failure event is the same in both games *)
254  local lemma BR1_BR2_bad &m:
255    Pr[CPA(BR1,A).main() @ &m: mem BR1.r Log.qs]
256    = Pr[CPA(BR2,A).main() @ &m: mem BR2.r Log.qs].
257  proof.
258  qed.
259
260  (** Exercise: What single "equiv" lemma could be used to prove both
261      BR1_BR2 and BR1_BR2_bad in one? Prove it and use it to prove
262      BR1_BR2_bad and BR1_BR2. **)
263
264  (** We can now prove that the success probability of A in CPA(BR2) is exactly 1/2 **)
265  local lemma pr_BR2_res &m: Pr[CPA(BR2,A).main() @ &m: res] = 1%r / 2%r.
266  proof.
267  qed.
268
269  local lemma pr_BR_BR2 &m:
270    Pr[CPA(BR,A).main() @ &m: res] - 1%r/2%r
271    <= Pr[CPA(BR2,A).main() @ &m: mem BR2.r Log.qs].
272  proof.
273  qed.
274
275  (** Step 3: Finally, we can do the reduction and prove that whenever
276      A queries the RO with the randomness used in the challenge
277      encryption, BR_OW(A) inverts the OW challenge. **)
278  local lemma BR2_OW &m:
279    Pr[CPA(BR2,A).main() @ &m: mem BR2.r Log.qs]
280    <= Pr[OW(BR_OW(A)).main() @ &m: res].
281  proof.
282  qed.
283
284  lemma Reduction &m:
285    Pr[CPA(BR,A).main() @ &m : res] - 1%r/2%r
286    <= Pr[OW(BR_OW(A)).main() @ &m: res].
287  proof.
288  qed.
289end section.