CoursePisa2014: prhl_basic_clean.ec

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

Exercise sheet 2 for day 3

Line 
1require import Word.
2require import Int.
3require import Array.
4require import Distr.
5require import FMap.
6require import PKE.
7
8theory RandOrcl.
9  type from.
10  type to.
11  op dsample : to distr. (* Distribution to use on the target type *)
12
13  (* A signature for random oracles from "from" to "to". *)
14  module type Oracle =  {
15    proc init():unit
16    proc o(x:from):to
17  }.
18
19  module type AdvRO = { proc o(x:from):to }.
20
21  theory ROM.
22    (* Bare random oracle for use in schemes *)
23    module RO:Oracle = {
24      var m : (from, to) map
25
26      proc init() : unit = {
27        m = FMap.empty;
28      }
29
30      proc o(x:from) : to = {
31        var y : to;
32        y = $dsample;
33        if (!in_dom x m) m.[x] = y;
34        return oget (m.[x]);
35      }
36    }.
37
38    lemma lossless_init: islossless RO.init
39    by (proc; wp; skip=> //).
40
41    lemma lossless_o : mu dsample True = 1%r => islossless RO.o.
42    proof.
43      by move=> Hs; proc; wp=> /=; rnd True.
44    qed.
45  end ROM.
46end RandOrcl.
47
48theory OW.
49
50  type t.
51  op sample_t : t distr.
52
53  type pkey.
54  type skey.
55  op keypairs: (pkey * skey) distr.
56  axiom keypair_lossless : mu keypairs True = 1%r.
57
58  op f : pkey -> t -> t.
59  op finv : skey -> t -> t.
60
61  axiom finvof : forall(pk : pkey, sk : skey, x : t),
62       in_supp (pk,sk) keypairs => finv sk (f pk x) = x.
63
64  axiom fofinv : forall(pk : pkey, sk : skey, x : t),
65     in_supp (pk,sk) keypairs => f pk (finv sk x) = x.
66
67  module type Inverter = {
68    proc inverter(pk : pkey, y : t) : t
69  }.
70
71  module OW(I :Inverter) ={
72    proc main() : bool ={
73      var x,x',y : t;
74      var pk : pkey;
75      var sk : skey;
76      x       = $sample_t;
77      (pk,sk) = $keypairs;
78      x'      = I.inverter(pk,(f pk x));
79      return (x = x');
80    }
81  }.
82
83end OW.
84
85
86theory BR93.
87
88  type randomness.
89  op l : int.
90  op sample_r : randomness distr.
91  clone import Word as Randomness with
92    type word <- randomness, op length = l,  op Dword.dword <- sample_r.
93
94  type ciphertext.
95  op n : int.
96  clone import Word as Ciphertext with type word <- ciphertext, op length <- n.
97
98  type plaintext.
99  op k : int.
100  op sample_p : plaintext distr.
101  clone import Word as Plaintext with
102    type word <- plaintext, op length <- k, op Dword.dword <- sample_p.
103
104  axiom sizes : k + l = n.
105
106  op (||) (x : randomness, y : plaintext) : ciphertext =
107      Ciphertext.from_bits ((to_bits x) || (to_bits y)).
108
109  op projRand(c : ciphertext) : randomness =
110     Randomness.from_bits (sub (to_bits c) 0 l).
111
112  op projPlain(c : ciphertext) : plaintext =
113    Plaintext.from_bits (sub (to_bits c) l k).
114
115  clone export OW with
116     type t <- randomness,
117     op sample_t <- sample_r.
118
119  clone export RandOrcl with
120    type from <- randomness,
121    type to <- plaintext,
122    op dsample <- sample_p.
123
124  import ROM.
125  import Pair.
126
127  clone PKE with
128     type pkey <- pkey,
129     type skey <- skey,
130     type plaintext <- plaintext,
131     type ciphertext <- ciphertext.
132
133  module BR3(R : Oracle) : PKE.Scheme = {
134    proc kg(): pkey * skey = {
135      var pk, sk;
136
137      R.init();
138      (pk,sk) = $keypairs;
139      return (pk,sk);
140    }
141
142    proc enc(pk:pkey, m:plaintext): ciphertext = {
143      var h, r;
144
145      r = $sample_r;
146      h = $sample_p;
147      return ((f pk r) ||   h);
148    }
149
150    proc dec(sk:skey, c : ciphertext) : plaintext option = {
151      var h;
152
153      h = R.o(finv sk (projRand c));
154      return (Some (projPlain c ^^ h));
155    }
156  }.
157
158module CPA' (S: PKE.Scheme, A:PKE.Adversary) = {
159  proc main() : bool = {
160    var pk, sk, m0, m1, c, b, b';
161
162    (pk, sk) = S.kg();
163    (m0, m1) = A.choose(pk);
164    c        = S.enc(pk, m0);
165    b'       = A.guess(c);
166    b        = ${0,1};
167    return (b' = b);
168  }
169}.
170
171(* if the encryption does not depend on the message, the probability
172   of winning the CPA game is equal to the probability of wining in
173   game CPA' *)
174lemma CPA_indep (S <: PKE.Scheme) (A <: PKE.Adversary{S}):
175  equiv [S.enc ~ S.enc : ={pk,glob S} ==> ={res,glob S}] =>
176  equiv [PKE.CPA(S,A).main ~ CPA'(S,A).main : ={glob A, glob S} ==> ={res} ].
177proof.
178(* FILL ME *)
179qed.
180
181lemma CPA_indep_pr &m (S <: PKE.Scheme) (A <: PKE.Adversary{S}):
182  equiv [S.enc ~ S.enc : ={pk,glob S} ==> ={res,glob S}] =>
183  Pr[PKE.CPA(S,A).main() @ &m : res] = Pr[CPA'(S,A).main() @ &m : res].
184proof.
185(* FILL ME *)
186qed.
187
188(* use this result applied to the scheme BR3 *)
189lemma BR3_enc_indep &m (A <: PKE.Adversary {RO}):
190  Pr[PKE.CPA(BR3(RO),A).main() @ &m : res] = Pr[CPA'(BR3(RO),A).main() @ &m : res].
191proof.
192(* FILL ME *)
193qed.
194