proofs/crypto/kdf/okm.bend

bend-collections-laws-crypto@1.0.0.0 · 283 lines · 16 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/kdf.bend as KDF
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/mac.bend as MAC
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hkdf.bend as Spec
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as HMAC
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/hmac.bend as MacP
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
9
10# HKDF-SHA256: the implementation src/crypto/kdf.bend equals the RFC 5869
11# specification spec/crypto/hkdf.bend for every salt, key material, info
12# and length (the statement of HACL*'s Hacl.HKDF against Spec.HKDF); the
13# output has the requested length and a shorter output is a prefix of a
14# longer one. HMAC enters only through MacP.sign_correct.
15
16# ---- lists ----
17
18def take_zero(+xs: List<&2, U32>) -> {List.take(&2, U32, xs, 0n) == Nil{} : List<&2, U32>}:
19  match xs:
20    case Nil{}:
21      {==}
22    case x <> rest:
23      {==}
24
25def take_append_short(+xs: List<&2, U32>, +ys: List<&2, U32>, +n: Nat, +h: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}) -> {List.take(&2, U32, List.append(&2, U32, xs, ys), n) == List.take(&2, U32, xs, n) : List<&2, U32>}:
26  match xs n:
27    case Nil{} 0n:
28      take_zero(ys)
29    case Nil{} 1n+p:
30      Empty.absurd({List.take(&2, U32, ys, 1n+p) == Nil{} : List<&2, U32>}, L.false_true(h))
31    case x <> rest 0n:
32      {==}
33    case +x <> +rest 1n+ +p:
34      %take_append_short(rest, ys, p, h) : {x <> List.take(&2, U32, List.append(&2, U32, rest, ys), p) == x <> _ : List<&2, U32>}
35      {==}
36
37def take_append_len(+xs: List<&2, U32>, +ys: List<&2, U32>, +k: Nat) -> {List.take(&2, U32, List.append(&2, U32, xs, ys), Nat.add(List.length(&2, U32, xs), k)) == List.append(&2, U32, xs, List.take(&2, U32, ys, k)) : List<&2, U32>}:
38  match xs:
39    case Nil{}:
40      {==}
41    case +x <> +rest:
42      %take_append_len(rest, ys, k) : {x <> List.take(&2, U32, List.append(&2, U32, rest, ys), Nat.add(List.length(&2, U32, rest), k)) == x <> _ : List<&2, U32>}
43      {==}
44
45def take_take(+xs: List<&2, U32>, +a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {List.take(&2, U32, List.take(&2, U32, xs, b), a) == List.take(&2, U32, xs, a) : List<&2, U32>}:
46  match xs a b:
47    case Nil{} _ _:
48      {==}
49    case +x <> +rest 0n _:
50      take_zero(List.take(&2, U32, x <> rest, b))
51    case x <> rest 1n+p 0n:
52      Empty.absurd({List.take(&2, U32, List.take(&2, U32, x <> rest, 0n), 1n+p) == List.take(&2, U32, x <> rest, 1n+p) : List<&2, U32>}, L.false_true(h))
53    case +x <> +rest 1n+ +p 1n+ +q:
54      %take_take(rest, p, q, h) : {x <> List.take(&2, U32, List.take(&2, U32, rest, q), p) == x <> _ : List<&2, U32>}
55      {==}
56
57def length_take(+xs: List<&2, U32>, +n: Nat, +h: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}) -> {List.length(&2, U32, List.take(&2, U32, xs, n)) == n : Nat}:
58  match xs n:
59    case Nil{} 0n:
60      {==}
61    case Nil{} 1n+p:
62      Empty.absurd({0n == 1n+p : Nat}, L.false_true(h))
63    case x <> rest 0n:
64      {==}
65    case +x <> +rest 1n+ +p:
66      %length_take(rest, p, h) : {1n+List.length(&2, U32, List.take(&2, U32, rest, p)) == 1n+_ : Nat}
67      {==}
68
69def length_append(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}:
70  match xs:
71    case Nil{}:
72      {==}
73    case +x <> +rest:
74      %length_append(rest, ys) : {1n+List.length(&2, U32, List.append(&2, U32, rest, ys)) == 1n+_ : Nat}
75      {==}
76
77def le_len(+xs: List<&2, U32>, +k: Nat, +e: {List.length(&2, U32, xs) == 32n : Nat}, +h: {Nat.is_le(k, 32n) == True{} : Bool}) -> {Nat.is_le(k, List.length(&2, U32, xs)) == True{} : Bool}:
78  %Equal.sym(Nat, List.length(&2, U32, xs), 32n, e) : {Nat.is_le(k, _) == True{} : Bool}
79  h
80
81# ---- N = ceil(L/32) covers L ----
82
83def peel32(+q: Nat) -> {Nat.divmod.go(Nat.add(32n+q, 31n), 31n, 0n, 0n) == Nat.divmod.go(Nat.add(q, 31n), 31n, 1n, 0n) : Nat & Nat}:
84  {==}
85
86def div_step(+q: Nat) -> {Nat.div(Nat.add(32n+q, 31n), 32n) == 1n+Nat.div(Nat.add(q, 31n), 32n) : Nat}:
87  Equal.trans(Nat, Pair.fst(Nat, Nat, Nat.divmod.go(Nat.add(32n+q, 31n), 31n, 0n, 0n)), Pair.fst(Nat, Nat, N.bump2(Nat.divmod.go(Nat.add(q, 31n), 31n, 0n, 0n))), 1n+Pair.fst(Nat, Nat, Nat.divmod.go(Nat.add(q, 31n), 31n, 0n, 0n)),
88    Equal.cong(Nat & Nat, Nat, (p => Pair.fst(Nat, Nat, p)), Nat.divmod.go(Nat.add(32n+q, 31n), 31n, 0n, 0n), N.bump2(Nat.divmod.go(Nat.add(q, 31n), 31n, 0n, 0n)),
89      Equal.trans(Nat & Nat, Nat.divmod.go(Nat.add(32n+q, 31n), 31n, 0n, 0n), Nat.divmod.go(Nat.add(q, 31n), 31n, 1n, 0n), N.bump2(Nat.divmod.go(Nat.add(q, 31n), 31n, 0n, 0n)),
90        peel32(q), N.acc2(Nat.add(q, 31n), 31n, 0n, 0n))),
91    N.fst_bump2(Nat.divmod.go(Nat.add(q, 31n), 31n, 0n, 0n)))
92
93def ceil_ok(len: Nat) -> {Nat.is_le(len, Nat.mul(Spec.block_count(len), 32n)) == True{} : Bool}:
94  match len:
95    case 0n:
96      {==}
97    case 1n:
98      {==}
99    case 2n:
100      {==}
101    case 3n:
102      {==}
103    case 4n:
104      {==}
105    case 5n:
106      {==}
107    case 6n:
108      {==}
109    case 7n:
110      {==}
111    case 8n:
112      {==}
113    case 9n:
114      {==}
115    case 10n:
116      {==}
117    case 11n:
118      {==}
119    case 12n:
120      {==}
121    case 13n:
122      {==}
123    case 14n:
124      {==}
125    case 15n:
126      {==}
127    case 16n:
128      {==}
129    case 17n:
130      {==}
131    case 18n:
132      {==}
133    case 19n:
134      {==}
135    case 20n:
136      {==}
137    case 21n:
138      {==}
139    case 22n:
140      {==}
141    case 23n:
142      {==}
143    case 24n:
144      {==}
145    case 25n:
146      {==}
147    case 26n:
148      {==}
149    case 27n:
150      {==}
151    case 28n:
152      {==}
153    case 29n:
154      {==}
155    case 30n:
156      {==}
157    case 31n:
158      {==}
159    case 32n+ +q:
160      %Equal.sym(Nat, Nat.div(Nat.add(32n+q, 31n), 32n), 1n+Nat.div(Nat.add(q, 31n), 32n), div_step(q)) : {Nat.is_le(32n+q, Nat.mul(_, 32n)) == True{} : Bool}
161      ceil_ok(q)
162
163# ---- the block chain ----
164
165# A last, partial block: 1+p <= 32 bytes of T(i+1).
166def short_case(+p: Nat, n: Nat, +prk: List<&2, U32>, +info: List<&2, U32>, +prev: List<&2, U32>, +i: Nat, +hp: {Nat.is_le(1n+p, 32n) == True{} : Bool}, +h: {Nat.is_le(1n+p, Nat.mul(n, 32n)) == True{} : Bool}) -> {List.take(&2, U32, MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), 1n+p) == List.take(&2, U32, Spec.t_blocks(n, prk, info, prev, i), 1n+p) : List<&2, U32>}:
167  match n:
168    case 0n:
169      Empty.absurd({List.take(&2, U32, MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), 1n+p) == List.take(&2, U32, Spec.t_blocks(0n, prk, info, prev, i), 1n+p) : List<&2, U32>}, L.false_true(h))
170    case 1n+ +m:
171      %MacP.sign_correct(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))) : {List.take(&2, U32, MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), 1n+p) == List.take(&2, U32, List.append(&2, U32, _, Spec.t_blocks(m, prk, info, _, 1n+i)), 1n+p) : List<&2, U32>}
172      Equal.sym(List<&2, U32>, List.take(&2, U32, List.append(&2, U32, MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), Spec.t_blocks(m, prk, info, MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), 1n+i)), 1n+p), List.take(&2, U32, MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), 1n+p),
173        take_append_short(MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), Spec.t_blocks(m, prk, info, MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), 1n+i), 1n+p, le_len(MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), 1n+p, MacP.sign_len(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))), hp)))
174
175# The implementation's stream of blocks, cut to rem bytes, is the first rem
176# bytes of RFC 5869's T(i+1) | ... | T(i+n), whenever those have rem bytes.
177def go_chain(rem: Nat, n: Nat, +prk: List<&2, U32>, +info: List<&2, U32>, +prev: List<&2, U32>, +i: Nat, +h: {Nat.is_le(rem, Nat.mul(n, 32n)) == True{} : Bool}) -> {KDF.blocks(rem, prk, info, prev, U32.from_nat(1n+i)) == List.take(&2, U32, Spec.t_blocks(n, prk, info, prev, i), rem) : List<&2, U32>}:
178  match rem n:
179    case 0n _:
180      Equal.sym(List<&2, U32>, List.take(&2, U32, Spec.t_blocks(n, prk, info, prev, i), 0n), Nil{}, take_zero(Spec.t_blocks(n, prk, info, prev, i)))
181    case 1n _:
182      short_case(0n, n, prk, info, prev, i, {==}, h)
183    case 2n _:
184      short_case(1n, n, prk, info, prev, i, {==}, h)
185    case 3n _:
186      short_case(2n, n, prk, info, prev, i, {==}, h)
187    case 4n _:
188      short_case(3n, n, prk, info, prev, i, {==}, h)
189    case 5n _:
190      short_case(4n, n, prk, info, prev, i, {==}, h)
191    case 6n _:
192      short_case(5n, n, prk, info, prev, i, {==}, h)
193    case 7n _:
194      short_case(6n, n, prk, info, prev, i, {==}, h)
195    case 8n _:
196      short_case(7n, n, prk, info, prev, i, {==}, h)
197    case 9n _:
198      short_case(8n, n, prk, info, prev, i, {==}, h)
199    case 10n _:
200      short_case(9n, n, prk, info, prev, i, {==}, h)
201    case 11n _:
202      short_case(10n, n, prk, info, prev, i, {==}, h)
203    case 12n _:
204      short_case(11n, n, prk, info, prev, i, {==}, h)
205    case 13n _:
206      short_case(12n, n, prk, info, prev, i, {==}, h)
207    case 14n _:
208      short_case(13n, n, prk, info, prev, i, {==}, h)
209    case 15n _:
210      short_case(14n, n, prk, info, prev, i, {==}, h)
211    case 16n _:
212      short_case(15n, n, prk, info, prev, i, {==}, h)
213    case 17n _:
214      short_case(16n, n, prk, info, prev, i, {==}, h)
215    case 18n _:
216      short_case(17n, n, prk, info, prev, i, {==}, h)
217    case 19n _:
218      short_case(18n, n, prk, info, prev, i, {==}, h)
219    case 20n _:
220      short_case(19n, n, prk, info, prev, i, {==}, h)
221    case 21n _:
222      short_case(20n, n, prk, info, prev, i, {==}, h)
223    case 22n _:
224      short_case(21n, n, prk, info, prev, i, {==}, h)
225    case 23n _:
226      short_case(22n, n, prk, info, prev, i, {==}, h)
227    case 24n _:
228      short_case(23n, n, prk, info, prev, i, {==}, h)
229    case 25n _:
230      short_case(24n, n, prk, info, prev, i, {==}, h)
231    case 26n _:
232      short_case(25n, n, prk, info, prev, i, {==}, h)
233    case 27n _:
234      short_case(26n, n, prk, info, prev, i, {==}, h)
235    case 28n _:
236      short_case(27n, n, prk, info, prev, i, {==}, h)
237    case 29n _:
238      short_case(28n, n, prk, info, prev, i, {==}, h)
239    case 30n _:
240      short_case(29n, n, prk, info, prev, i, {==}, h)
241    case 31n _:
242      short_case(30n, n, prk, info, prev, i, {==}, h)
243    case 32n+r 0n:
244      Empty.absurd({KDF.blocks(32n+r, prk, info, prev, U32.from_nat(1n+i)) == List.take(&2, U32, Spec.t_blocks(0n, prk, info, prev, i), 32n+r) : List<&2, U32>}, L.false_true(h))
245    case 32n+ +r 1n+ +m:
246      +t = MAC.sign(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)])))
247      +tb = Spec.t_blocks(m, prk, info, t, 1n+i)
248      %MacP.sign_correct(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))) : {List.append(&2, U32, t, KDF.blocks(r, prk, info, t, U32.from_nat(1n+(1n+i)))) == List.take(&2, U32, List.append(&2, U32, _, Spec.t_blocks(m, prk, info, _, 1n+i)), 32n+r) : List<&2, U32>}
249      %MacP.sign_len(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)]))) : {List.append(&2, U32, t, KDF.blocks(r, prk, info, t, U32.from_nat(1n+(1n+i)))) == List.take(&2, U32, List.append(&2, U32, t, tb), Nat.add(_, r)) : List<&2, U32>}
250      %Equal.sym(List<&2, U32>, List.take(&2, U32, List.append(&2, U32, t, tb), Nat.add(List.length(&2, U32, t), r)), List.append(&2, U32, t, List.take(&2, U32, tb, r)), take_append_len(t, tb, r)) : {List.append(&2, U32, t, KDF.blocks(r, prk, info, t, U32.from_nat(1n+(1n+i)))) == _ : List<&2, U32>}
251      %go_chain(r, m, prk, info, t, 1n+i, h) : {List.append(&2, U32, t, KDF.blocks(r, prk, info, t, U32.from_nat(1n+(1n+i)))) == List.append(&2, U32, t, _) : List<&2, U32>}
252      {==}
253
254# RFC 5869's T(1) | ... | T(n) has 32n bytes.
255def blocks_len(n: Nat, +prk: List<&2, U32>, +info: List<&2, U32>, +prev: List<&2, U32>, +i: Nat) -> {List.length(&2, U32, Spec.t_blocks(n, prk, info, prev, i)) == Nat.mul(n, 32n) : Nat}:
256  match n:
257    case 0n:
258      {==}
259    case 1n+ +m:
260      +s = HMAC.hmac(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)])))
261      +tb = Spec.t_blocks(m, prk, info, s, 1n+i)
262      %Equal.sym(Nat, List.length(&2, U32, List.append(&2, U32, s, tb)), Nat.add(List.length(&2, U32, s), List.length(&2, U32, tb)), length_append(s, tb)) : {_ == Nat.mul(1n+m, 32n) : Nat}
263      %Equal.sym(Nat, List.length(&2, U32, s), 32n, MacP.hmac_len(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)])))) : {Nat.add(_, List.length(&2, U32, tb)) == Nat.mul(1n+m, 32n) : Nat}
264      %Equal.sym(Nat, List.length(&2, U32, tb), Nat.mul(m, 32n), blocks_len(m, prk, info, s, 1n+i)) : {Nat.add(32n, _) == Nat.mul(1n+m, 32n) : Nat}
265      {==}
266
267# ---- OKM ----
268
269def okm_correct(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> {KDF.blocks(len, prk, info, Nil{}, 1) == Spec.okm(prk, info, len) : List<&2, U32>}:
270  go_chain(len, Spec.block_count(len), prk, info, Nil{}, 0n, ceil_ok(len))
271
272def okm_length(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> {List.length(&2, U32, Spec.okm(prk, info, len)) == len : Nat}:
273  +tb = Spec.t_blocks(Spec.block_count(len), prk, info, Nil{}, 0n)
274  length_take(tb, len, %Equal.sym(Nat, List.length(&2, U32, tb), Nat.mul(Spec.block_count(len), 32n), blocks_len(Spec.block_count(len), prk, info, Nil{}, 0n)) : {Nat.is_le(len, _) == True{} : Bool}; ceil_ok(len))
275
276def okm_prefix(+prk: List<&2, U32>, +info: List<&2, U32>, +a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Spec.okm(prk, info, a) == List.take(&2, U32, Spec.okm(prk, info, b), a) : List<&2, U32>}:
277  +x = KDF.blocks(a, prk, info, Nil{}, 1)
278  +tb = Spec.t_blocks(Spec.block_count(b), prk, info, Nil{}, 0n)
279  Equal.trans(List<&2, U32>, Spec.okm(prk, info, a), x, List.take(&2, U32, Spec.okm(prk, info, b), a),
280    Equal.sym(List<&2, U32>, x, Spec.okm(prk, info, a), okm_correct(prk, info, a)),
281    Equal.trans(List<&2, U32>, x, List.take(&2, U32, tb, a), List.take(&2, U32, Spec.okm(prk, info, b), a),
282      go_chain(a, Spec.block_count(b), prk, info, Nil{}, 0n, N.le_trans(a, b, Nat.mul(Spec.block_count(b), 32n), h, ceil_ok(b))),
283      Equal.sym(List<&2, U32>, List.take(&2, U32, List.take(&2, U32, tb, b), a), List.take(&2, U32, tb, a), take_take(tb, a, b, h))))