forked from PrincetonUniversity/VST
-
Notifications
You must be signed in to change notification settings - Fork 0
/
HMAC_PRF.v
255 lines (216 loc) · 6.14 KB
/
HMAC_PRF.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
(* Copyright 2012-2015 by Adam Petcher. *
* Use of this source code is governed by the license described *
* in the LICENSE file at the root of the source tree. *)
Set Implicit Arguments.
Require Import fcf.FCF.
Require Import hmacfcf.HMAC_spec.
Require Import fcf.PRF.
Require Import hmacfcf.NMAC_to_HMAC.
Require Import hmacfcf.hF.
Require Import hmacfcf.GHMAC_PRF.
Section HMAC_PRF.
Variable c p : nat.
Definition b := @b c p.
Variable h : Bvector c -> Bvector b -> Bvector c.
Variable iv : Bvector c.
Variable Message : Set.
Hypothesis Message_EqDec : EqDec Message.
Variable splitAndPad : Message -> list (Bvector b).
Hypothesis splitAndPad_1_1 :
forall b1 b2,
splitAndPad b1 = splitAndPad b2 ->
b1 = b2.
Variable fpad : Bvector c -> Bvector p.
Definition h_star_pad := h_star_pad h fpad.
Variable opad ipad : Bvector b.
Hypothesis opad_ne_ipad : opad <> ipad.
Section h_star_WCR.
Definition h_star := h_star _ h.
Variable Z : OracleComp (list (Bvector (HMAC_spec.b c p))) (Bvector (HMAC_spec.b c p))
(list (Bvector (HMAC_spec.b c p)) * list (Bvector (HMAC_spec.b c p))).
Definition Y : OracleComp (list (Bvector (HMAC_spec.b c p))) (Bvector c)
(list (Bvector (HMAC_spec.b c p)) * list (Bvector (HMAC_spec.b c p))) :=
[x, _] <--$2 OC_Run _ _ _ Z (fun _ d => r <--$ OC_Query _ d; $ ret ((app_fpad fpad r), tt)) tt;
$ ret x.
Theorem WCR_h_star_pad_impl_h_star :
cAU.Adv_WCR _ _ h_star_pad
({ 0 , 1 }^c) Z <=
cAU.Adv_WCR _ _ h_star
({ 0 , 1 }^c) Y.
unfold cAU.Adv_WCR, cAU.Adv_WCR_G.
comp_skip.
unfold Y.
eapply comp_spec_impl_le.
simpl.
inline_first.
comp_skip.
eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => fst b = a)).
trivial.
intuition.
subst.
unfold cAU.WCR_Oracle.
inline_first.
comp_simp.
inline_first.
comp_simp.
simpl.
eapply comp_spec_ret.
intuition.
simpl in *.
intuition.
destruct b2.
simpl in *.
subst.
comp_simp.
simpl.
comp_simp.
inline_first.
comp_simp.
eapply comp_spec_ret.
intuition.
unfold h_star_pad in *.
case_eq (eqb a b1); intuition;
rewrite H3 in H2;
simpl in *.
discriminate.
apply eqbBvector_sound in H2.
unfold HMAC_spec.h_star_pad, HMAC_spec.app_fpad in *.
Theorem Vector_append_inj_first :
forall (A : Set)(a : nat)(a1 a2 : Vector.t A a)(b : nat)(b1 b2 : Vector.t A b),
Vector.append a1 b1 = Vector.append a2 b2 ->
a1 = a2.
induction a1; intuition.
rewrite vector_0 in *.
trivial.
destruct (vector_S a2).
destruct H2.
subst.
repeat rewrite <- splitVector.Vector_cons_app_assoc in H.
inversion H.
apply vector_cons_eq in H.
f_equal.
eapply IHa1.
eauto.
Qed.
eapply Vector_append_inj_first in H2.
unfold h_star, NMAC_to_HMAC.h_star.
rewrite H2.
eapply eqbBvector_complete.
Qed.
End h_star_WCR.
Definition HMAC := HMAC h iv splitAndPad fpad opad ipad.
Definition GHMAC := GHMAC h iv fpad opad ipad.
Variable A : OracleComp Message (Bvector c) bool.
Hypothesis A_wf : well_formed_oc A.
Definition A_GHMAC : OracleComp (list (Bvector b)) (Bvector c) bool :=
[b, _] <--$2 OC_Run _ _ _ A
(fun _ q =>
ls <- splitAndPad q;
r <--$ OC_Query _ ls;
$ ret (r, tt)) tt;
$ ret b.
Theorem GHMAC_to_HMAC :
PRF_Advantage (Rnd b) (Rnd c) HMAC _ _ A ==
PRF_Advantage (Rnd b) (Rnd c) GHMAC _ _ A_GHMAC.
unfold PRF_Advantage.
eapply ratDistance_eqRat_compat.
unfold PRF_G_A, HMAC, HMAC_spec.HMAC, GHMAC, NMAC_to_HMAC.GHMAC.
comp_skip.
unfold A_GHMAC.
eapply comp_spec_eq_impl_eq.
simpl.
inline_first.
comp_skip.
eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => True)); intuition.
unfold f_oracle.
unfold HMAC_2K, HMAC_spec.GHMAC.
inline_first.
comp_simp.
inline_first.
comp_simp.
simpl.
eapply comp_spec_ret; intuition.
simpl in *.
comp_simp.
simpl.
inline_first.
comp_simp.
intuition; subst.
eapply comp_spec_eq_refl.
unfold PRF_G_B, A_GHMAC.
eapply comp_spec_eq_impl_eq.
simpl.
inline_first.
comp_skip.
eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _
(fun a b => forall x, arrayLookup _ (snd b) (splitAndPad x) = arrayLookup _ a x)).
intuition.
intuition.
inline_first.
unfold RndR_func, randomFunc.
rewrite H.
case_eq ( arrayLookup Message_EqDec x1 a ); intuition.
comp_simp.
inline_first.
comp_simp.
simpl.
eapply comp_spec_ret; intuition.
inline_first.
comp_skip.
comp_simp.
inline_first.
comp_simp.
simpl.
eapply comp_spec_ret; intuition.
simpl.
case_eq (eqb x a); intuition.
rewrite eqb_leibniz in H5.
subst.
rewrite eqb_refl.
trivial.
case_eq (eqb (splitAndPad x) (splitAndPad a)); intuition.
rewrite eqb_leibniz in H6.
apply splitAndPad_1_1 in H6.
subst.
rewrite eqb_refl in H5.
discriminate.
simpl in *.
intuition; subst.
comp_simp.
simpl.
inline_first.
comp_simp.
eapply comp_spec_eq_refl.
Qed.
Theorem HMAC_PRF:
PRF_Advantage (Rnd b) (Rnd c) HMAC _ _ A <=
RKA_Advantage _ _ _ ({ 0 , 1 }^b)
({ 0 , 1 }^c) (dual_f h) (BVxor b)
(HMAC_RKA_A h iv fpad opad ipad A_GHMAC) +
(PRF_Advantage ({ 0 , 1 }^c) ({ 0 , 1 }^c) h _ _
(PRF_h_A h_star_pad A_GHMAC) +
cAU.Adv_WCR _ _ h_star
({ 0 , 1 }^c) (Y (au_F_A A_GHMAC))).
rewrite GHMAC_to_HMAC.
eapply leRat_trans.
apply GHMAC_PRF.
trivial.
unfold A_GHMAC.
econstructor.
econstructor.
trivial.
intuition.
econstructor.
econstructor.
intuition.
econstructor.
wftac.
intuition.
econstructor.
wftac.
eapply ratAdd_leRat_compat; try reflexivity.
eapply ratAdd_leRat_compat; try reflexivity.
eapply WCR_h_star_pad_impl_h_star.
Qed.
Print Assumptions HMAC_PRF.
End HMAC_PRF.