1	import Base
2	import ../../../src/crypto/kdf.bend as KDF
3	import ../../../src/crypto/mac.bend as MAC
4	import ../../../spec/crypto/hkdf.bend as Spec
5	import ../../../spec/crypto/hmac.bend as HMAC
6	import ../mac/hmac.bend as MacP
7	import ../../lib/logic.bend as L
8	import ../../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	
18	def 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	
25	def 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	
37	def 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	
45	def 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	
57	def 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	
69	def 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	
77	def 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	
83	def 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	
86	def 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	
93	def 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).
166	def 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.
177	def 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.
255	def 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	
269	def 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	
272	def 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	
276	def 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))))