-
Notifications
You must be signed in to change notification settings - Fork 0
/
MultipleTimeConstruction.ec
423 lines (354 loc) · 14.2 KB
/
MultipleTimeConstruction.ec
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
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
require import Distr DInterval AllCore List BasicProps SmtMap.
(* The main goal of this development is to implement a multiple-time
forward-resistant tag system based on authentication paths.
Here, the main results are:
# tagGen - tag generation function
# tagVer - tag verification function
# multTagsCorrect - proof that tag verification agrees with tag generation
*)
(* Parameters: types *)
type Time = int.
type pkey, skey, sig.
type message = int * (pkey option) * (pkey option).
type tag = (int * message * sig) list.
(* Parameters: one-time signature scheme *)
op otsSig : skey -> message -> sig.
op otsVer : pkey option -> message -> sig -> bool.
op otsKey : int -> pkey * skey.
op sk2pk : skey -> pkey.
axiom otsCorrect rs pk sk m : (pk, sk) = otsKey rs => otsVer (Some pk) m (otsSig sk m) = true.
axiom sk2pkLaw rs pk sk : (pk, sk) = otsKey rs => pk = sk2pk sk.
axiom L_pl0: forall (m : message) (s : sig), otsVer None m s = false.
(* Parameters: positive expiration date *)
op EXP : Time.
axiom Npos : 1 <= EXP.
op dR : int distr = dinter 1 (2^512).
op tdistr : Time distr = dinter 1 EXP.
(* CONSTRUCTION: Tag Generation *)
op msg : (Time -> pkey option) -> Time -> message = fun pkf i => (i, pkf (2*i), pkf (2*i + 1)).
op tagGen' (pkf : Time -> pkey option) (skf : Time -> skey option) (xs : Time list) : tag
= foldr (fun n r =>
(n, (msg pkf n), otsSig (oget (skf n)) (msg pkf n)) :: r) [] xs.
op tagGen : (Time -> skey option) -> Time -> tag option
= fun skf i => if i <= 0 then None else Some
(tagGen' (fun i => omap sk2pk (skf i)) skf (binRec i)).
(* CONSTRUCTION: Tag Verification *)
op tag2list : (Time * tag option) -> (Time * message * sig) list
= fun (x : int * tag option) => if x.`2 = None then [] else oget x.`2.
op msg2key : message -> Time -> pkey option
= fun (m: message) i => if i = 2 * m.`1 then m.`2 else if i = 2 * m.`1 + 1 then m.`3 else None.
op checkPair : (Time * message * sig) -> (Time * message * sig) -> bool
= fun (x x' : Time * message * sig) => otsVer (msg2key x'.`2 x.`1) x.`2 x.`3 .
op checkChain (tl : (Time * message * sig) list) : bool =
with tl = [] => true
with tl = x :: xs =>
(if xs = [] then true else checkPair (head witness xs) x) /\ checkChain xs.
op tagVerH (pk : pkey) (i : Time) (tl : (Time * message * sig) list) : bool =
with tl = [] => false
with tl = x :: xs => x.`1 = 1
/\ (last x tl).`1 = i
/\ otsVer (Some pk) x.`2 x.`3
/\ all (fun (e : int * message * sig) => e.`1 <= i /\ 0 < e.`1) tl
/\ checkChain tl.
op tagVer (pk : pkey) (i : Time) (to : tag option) : bool
= tagVerH pk i (tag2list (i, to)).
(* Correctness and Properties *)
lemma L_pl11: forall (pk : pkey) (i : int) (tg : tag option) (e : int *
message * sig) (es : (int * message * sig) list),
tagVer pk i tg = true =>
tag2list (i, tg) = e :: es => e.`1 = 1.
proof. smt. qed.
lemma L_pl4: forall (pk : pkey) (itg : int * tag option),
tagVer pk itg.`1 itg.`2 = true =>
exists (q1 : (int * message * sig) list) (m : message)
(s : sig), tag2list itg = q1 ++ [(itg.`1, m, s)].
proof. move => pk itg.
case (tag2list (itg.`1, itg.`2) = []).
smt.
move => h1.
have : exists q qs, tag2list (itg.`1, itg.`2) = q :: qs.
smt (oa2).
elim. move => q qs h2.
simplify tagVer. rewrite h2. simplify tagVerH.
have : exists z zs, q :: qs = zs ++ z :: [].
smt (oa3).
elim. move => z zs h4.
have : (last q qs) = z. smt (oa4).
move => h5.
rewrite h5.
move => h6.
exists zs z.`2 z.`3. smt.
qed.
lemma L_pl9: forall (pk : pkey) (i : int) (tg : tag option) (q : (int *
message * sig) list) (e : int * message * sig),
tagVer pk i tg =>
tag2list (i, tg) = e :: q =>
otsVer (Some pk) e.`2 e.`3 = true.
proof. smt. qed.
lemma L_pl7': forall (pk : pkey) (i : int) (tg : tag option) (q1 : (int *
message * sig) list) (e e' : int * message * sig)
(q2 : (int * message * sig) list),
checkChain (q1 ++ e :: e' :: q2) =>
otsVer (msg2key e.`2 e'.`1) e'.`2 e'.`3 = true.
proof. move => pk i tg.
elim. simplify checkChain. simplify msg2key. smt.
smt.
qed.
lemma L_pl7: forall (pk : pkey) (i : int) (tg : tag option) (q1 : (int *
message * sig) list) (e e' : int * message * sig)
(q2 : (int * message * sig) list),
tagVer pk i tg =>
tag2list (i, tg) = (q1 ++ e :: e' :: q2) =>
otsVer (msg2key e.`2 e'.`1) e'.`2 e'.`3 = true.
proof. smt (L_pl7').
qed.
lemma L_pl8': forall (pk : pkey) (i : int) (tg : tag option) (e : int *
message * sig),
tagVer pk i tg = true =>
e \in tag2list (i, tg) => e.`1 <= i /\ 0 < e.`1.
proof. move => pk i tg e. simplify tagVer.
case ((tag2list (i, tg)) = []).
smt.
move => h.
have : exists x xs, tag2list (i, tg) = x::xs. smt (oa2).
elim. move => x xs.
move => h2. rewrite h2.
simplify tagVerH.
simplify checkPair. smt.
qed.
op infoAhead : int -> int = fun x => if x <= 0 then 0 else 2*x + 1.
op M : int = infoAhead EXP.
lemma MNn : infoAhead EXP = M by auto.
lemma infoAheadP i : 0 <= i => i <= infoAhead i by smt.
lemma infoAheadM (i : int) j : 0 <= i => i <= j => infoAhead i <= infoAhead j by smt.
lemma infoAheadEXP (i : int) : i <= 0 => infoAhead i = 0 by smt.
lemma tdAx : forall (i : int), (i \in tdistr) => 0 < i by smt.
lemma Mpos : 1 <= M by smt.
lemma MEXP : EXP <= M by smt.
lemma dR_ll : is_lossless dR by smt.
lemma td_ll : is_lossless tdistr by smt.
lemma L_a5'': forall (sk1 sk2 : int -> skey option) (pk1 pk2 : int -> pkey option)
(i : int) (xs : int list),
(forall (j : int), j <= infoAhead i => sk1 j = sk2 j) =>
(forall (j : int), j <= infoAhead i => pk1 j = pk2 j) =>
(forall j, j \in xs => j <= i) =>
0 < i => tagGen' pk1 sk1 xs = tagGen' pk2 sk2 xs.
proof. move => sk1 sk2 pk1 pk2 i. elim. move => h1 h2 h3.
move => g. simplify delta. auto.
move => x l h1 h2 h3 j g.
simplify delta.
have : ((pk1 (2 * x) = pk2 (2 * x) /\ pk1 (2 * x + 1) = pk2 (2 * x + 1)) /\
otsSig (odflt witness (sk1 x)) (x, pk1 (2 * x), pk1 (2 * x + 1)) =
otsSig (odflt witness (sk2 x)) (x, pk2 (2 * x), pk2 (2 * x + 1))).
have : 2 * x + 1 <= infoAhead i. simplify infoAhead. timeout 20. smt.
smt.
move => k. rewrite k.
simplify.
apply h1.
smt. smt.
progress. apply j. smt. auto.
qed.
lemma L_a5': forall (sk1 sk2 : int -> skey option) (i : int) ,
(forall (j : int), j <= infoAhead i => sk1 j = sk2 j) =>
tagGen sk1 i = tagGen sk2 i.
proof. simplify tagGen. move => sk1 sk2 i a1.
case (i <= 0). auto.
move => q. congr.
apply (L_a5'' sk1 sk2 (fun (i0 : int) => omap sk2pk (sk1 i0))
(fun (i0 : int) => omap sk2pk (sk2 i0)) i).
apply a1. smt. smt. smt.
qed.
lemma L_a5: forall (sk1 sk2 : int -> skey option) (i : int),
(forall (j : int), j <= infoAhead i => sk1 j = sk2 j) =>
tagGen sk1 i = tagGen sk2 i.
proof. move => sk1 sk2 i p. simplify tagGen. apply (L_a5' sk1 sk2 i).
assumption.
qed.
lemma L_pl5: forall (pkf : int -> pkey option)(i e : int) (pk : pkey),
msg2key (msg pkf i) e = Some pk => Some pk = pkf e.
proof. simplify msg2key. simplify msg. smt. qed.
lemma tagGenChainCorr3' skf i: forall (xs : int list) r1 r2,
xs <> []
=> last r2 xs = i
=> (last r1 (tagGen' (fun (i0 : int) => omap sk2pk (skf i0)) skf xs)).`1 = i.
proof. elim. smt.
move => x1 l hyp r1 r2 p1 p2.
case (l = []). move => q. rewrite q.
have : x1 = i. smt.
move => p. rewrite p. simplify tagGen'. simplify. trivial.
simplify tagGen'. move => q.
apply (hyp ((x1, msg (fun (i0 : int) => omap sk2pk (skf i0)) x1,
otsSig (oget (skf x1))
(msg (fun (i0 : int) => omap sk2pk (skf i0)) x1))) x1 q p2) .
qed.
lemma tagGenChainCorr3 skf i: 0 < i =>
(last witness (tagGen' (fun (i0 : int) => omap sk2pk (skf i0)) skf (binRec i))).`1 = i.
proof. move => q.
apply (tagGenChainCorr3' skf i (binRec i) witness witness).
smt. smt.
qed.
lemma tagGenChainCorr2' skf i: forall (xs : int list),
(forall x, x \in xs => x <= i /\ 0 < x)
=> all (fun (e : int * message * sig) => e.`1 <= i /\ 0 < e.`1)
(tagGen' (fun (i0 : int) => omap sk2pk (skf i0)) skf xs).
proof. elim. simplify. smt.
simplify. move => n p1 p2 p3.
simplify tagGen'. simplify.
have : (n <= i /\ 0 < n) = true.
have : (n <= i /\ 0 < n). apply (p3 n). smt.
move => q. rewrite q. simplify. auto.
progress. smt. smt. apply p2. smt.
qed.
lemma tagGenChainCorr2 skf i:
all (fun (e : int * message * sig) => e.`1 <= i /\ 0 < e.`1)
(tagGen' (fun (i0 : int) => omap sk2pk (skf i0)) skf (binRec i)).
proof. apply tagGenChainCorr2'. apply (br3).
qed.
lemma tagGenChainCorr1 pkf skf :
forall (xs : int list),
(forall j, exists pk sk rs, pkf j = Some pk /\ skf j = Some sk /\ (pk, sk) = otsKey rs)
=> (forall xs1 xs2 e e', xs = xs1 ++ e :: e' :: xs2 => e = div e' 2) =>
checkChain (tagGen' pkf skf xs) = true.
elim. smt.
move => x. elim.
move =>_ _ _. simplify delta. simplify. trivial.
move => h1 h2 h3 h4 h5 h6.
simplify tagGen'. simplify.
have : ((foldr
(fun (n : int) (r : (int * (int * pkey option * pkey option) *
sig) list) => (n, msg pkf n, otsSig (oget (skf n)) (msg pkf n)) :: r)
[] h2 <>
[] =>
checkPair
(head witness
(foldr
(fun (n : int) (r : (int * (int * pkey option * pkey option) *
sig) list) =>
(n, msg pkf n, otsSig (oget (skf n)) (msg pkf n)) :: r) [] h2))
(h1, msg pkf h1, otsSig (oget (skf h1)) (msg pkf h1))) /\
checkChain
(foldr
(fun (n : int) (r : (int * (int * pkey option * pkey option) *
sig) list) => (n, msg pkf n, otsSig (oget (skf n)) (msg pkf n)) :: r)
[] h2)) = checkChain (tagGen' pkf skf (h1 :: h2)).
simplify tagGen'. auto.
move => qq.
rewrite qq.
have : checkChain (tagGen' pkf skf (h1 :: h2)) = true.
apply h4. smt. move => xs1 xs2 e e' o.
case (xs1 = []).
move => q.
apply (h6 (x :: []) xs2). smt.
move => q.
apply (h6 (x :: xs1) xs2). smt.
move => hz. rewrite hz. simplify.
simplify delta.
have : x = div h1 2. apply (h6 [] h2). auto.
move => z. rewrite z.
case (h1 = (2 * (div h1 2) + 1)).
move => w. rewrite w.
rewrite (div3 (div h1 2)).
simplify.
have : (2 * div h1 2 + 1 = 2 * div h1 2) = false. smt.
move => oo. rewrite oo. simplify.
have : exists pk sk rs, pkf (2 * div h1 2 + 1) = Some pk /\ skf (2 * div h1 2 + 1) = Some sk
/\ (pk, sk) = otsKey rs.
apply h5.
elim.
move => pk sk rs.
elim. move => e1. elim. move => e2 e3.
rewrite e1 e2. simplify.
apply (otsCorrect rs pk sk). apply e3.
move => u.
have : (h1 = (2 * (div h1 2))). apply div4. apply u.
move => q. rewrite q.
rewrite (div2 (div h1 2)).
have : (2 * div h1 2 = 2 * div h1 2) = true. reflexivity.
move => qc. rewrite qc. simplify.
have : exists pk sk rs, pkf (2 * div h1 2) = Some pk
/\ skf (2 * div h1 2) = Some sk /\ (pk, sk) = otsKey rs.
apply h5.
elim.
move => pk sk rs.
elim. move => e1. elim. move => e2 e3.
rewrite e1 e2. simplify.
apply (otsCorrect rs pk sk). apply e3.
qed.
op tagGenS : (int -> pkey option) -> (int, sig) fmap -> int list -> tag =
fun pkf skf xs => foldr (fun n r =>
(n, (msg pkf n), oget skf.[n]) :: r) [] xs.
lemma zup pkf skf fm : forall (xs : int list),
(forall j, j \in xs => otsSig (oget (skf j)) (msg pkf j) = (oget fm.[j]))
=> tagGen' pkf skf xs = tagGenS pkf fm xs.
proof. elim.
smt.
move => x l hyp h.
simplify tagGen' tagGenS.
have : (otsSig (oget (skf x)) (msg pkf x) = oget fm.[x]) = true.
smt.
move => q. rewrite q. simplify.
apply hyp. smt.
qed.
lemma multTagsCorrect skf :
(forall j, exists pk sk rs, omap sk2pk (skf j) = Some pk
/\ skf j = Some sk /\ (pk, sk) = otsKey rs) =>
forall i, 0 < i => tagVer (oget (omap sk2pk (skf 1))) i (tagGen skf i).
move => jp i p.
simplify tagVer .
have : i <= 0 = false. smt. move => co.
have : ((tag2list (i, tagGen skf i)) <> []).
simplify tagGen. rewrite co. simplify. simplify tag2list oget.
have : exists xs, (binRec i) = (1 :: xs). apply br4. apply p.
elim. move => xs pq. rewrite pq. simplify tagGen'. auto.
move => h.
have : exists x xs, (tag2list (i, tagGen skf i)) = x::xs. smt (oa2).
elim. move => x xs.
move => h1.
rewrite h1.
simplify .
have : ((xs <> [] => checkPair (head witness xs) x) /\ checkChain xs) = checkChain (x::xs). smt.
move => g.
rewrite g.
rewrite - h1.
have : ((x.`1 <= i /\ 0 < x.`1) /\
all (fun (e : int * message * sig) => e.`1 <= i /\ 0 < e.`1) xs)
= all (fun (e : int * message * sig) => e.`1 <= i /\ 0 < e.`1)
(tag2list (i, tagGen skf i)).
smt. move => ol. rewrite ol.
have : x.`1 = 1.
have : x = head witness (tag2list (i, tagGen skf i)). smt.
move => zo. rewrite zo.
simplify tag2list. simplify tagGen.
rewrite co. simplify. simplify oget.
have : exists xs, (binRec i) = (1 :: xs). apply br4. apply p.
elim. move => zs pq. rewrite pq. simplify tagGen'. auto.
have : (last witness (tag2list (i, tagGen skf i))).`1 = i.
simplify tag2list. simplify tagGen.
rewrite co. simplify. simplify oget. apply tagGenChainCorr3. smt.
move => ff. progress.
have : (last x xs) = last witness (tag2list (i, tagGen skf i)). smt.
move => zo. rewrite zo.
apply ff.
have : head witness (tag2list (i, tagGen skf i)) = (1, (msg (fun (i0 : int)
=> omap sk2pk (skf i0)) 1), otsSig (oget (skf 1))
(msg (fun (i0 : int) => omap sk2pk (skf i0)) 1)).
simplify tag2list. simplify tagGen. rewrite co. simplify. simplify oget.
have : exists xs, (binRec i) = (1 :: xs). apply br4. apply p.
elim. move => xss pq. rewrite pq. simplify tagGen'. auto.
move => qp.
have : x = (1, (msg (fun (i0 : int) => omap sk2pk (skf i0)) 1),
otsSig (oget (skf 1)) (msg (fun (i0 : int) => omap sk2pk (skf i0)) 1)). smt.
move => qp1. rewrite qp1. simplify delta.
have : exists (pk : pkey) (sk : skey) (rs : int),
(fun (i0 : int) => omap sk2pk (skf i0)) 1 = Some pk
/\ skf 1 = Some sk /\ (pk, sk) = otsKey rs. apply (jp 1). elim.
move => pk sk rs p1. smt.
simplify tag2list tagGen. rewrite co. simplify. simplify oget.
apply tagGenChainCorr2.
simplify tag2list. simplify tagGen. rewrite co. simplify. simplify oget.
have : checkChain
(tagGen' (fun (i0 : int) => omap sk2pk (skf i0)) skf (binRec i)) = true.
apply (tagGenChainCorr1 (fun i => omap sk2pk (skf i)) skf (binRec i)).
smt. apply br5.
smt. smt.
qed.