proofs/crypto/aes/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 448 lines · 31 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/sbox.bend as B
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as A
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as GI
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/aesgcm.bend as GCM
7import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
8import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
9
10# Generated by tools/generators/aes/laws.py.
11
12# The clauses of the AES / AES-GCM contract (docs/CRYPTO_CONTRACTS.md),
13# stated over the public functions and the executable specifications
14# spec/crypto/aes/{aes,gcm}.bend. Proved in proof.bend.
15
16# One block with an optional expanded key (the byte API in one call).
17def block_with(m: Maybe<&2, A.Schedule>, block: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
18  match m:
19    case None{}:
20      None{}
21    case Some{s}:
22      A.encrypt_block(s, block)
23
24# Decrypt what an encryption returned (None stays None).
25def open128(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
26  match m:
27    case None{}:
28      None{}
29    case Some{ct}:
30      GCM.aes128_gcm_decrypt(key, nonce, aad, ct)
31
32def open256(+key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
33  match m:
34    case None{}:
35      None{}
36    case Some{ct}:
37      GCM.aes256_gcm_decrypt(key, nonce, aad, ct)
38
39# ---- AES (FIPS 197) ----
40
41# The constant-time S-box circuit is FIPS 197's S-box (the inverse in
42# GF(2^8), {00} to {00}, then the affine map), on every input.
43law Sbox.value:
44  for +x: U32
45  {B.sbox(x) == S.sbox(x) : U32}
46
47# The specification's inverse (a^254) is the multiplicative inverse of
48# FIPS 197 section 4.4: a * a^-1 = {01} for every nonzero byte, and {00}
49# goes to {00} (5.1.1); so S.sbox is "inverse, then affine map".
50law Inverse.unit:
51  for +x: U32
52  for +h: {U32.is_eq(U32.and(255, x), 0) == False{} : Bool}
53  {S.mul(x, S.inverse(x)) == 1 : U32}
54
55law Inverse.zero:
56  {S.inverse(0) == 0 : U32}
57
58# The implementation's cipher with its expanded key is FIPS 197's Cipher
59# with KeyExpansion, for every Nk, Nr, key and state.
60law Cipher.value:
61  for +nk: Nat
62  for +nr: Nat
63  for +key: List<&2, U32>
64  for +s: T.State
65  {A.encrypt(nk, nr, key, s) == S.encrypt(nk, nr, key, s) : T.State}
66
67# The byte API: a key of 16, 24 or 32 bytes encrypts a 16-byte block with
68# AES under the key's Nk = length/4 and Nr = Nk + 6 (FIPS 197 Figure 4).
69law Block.value:
70  for +key: List<&2, U32>
71  for +h: {A.valid_length(List.length(&2, U32, key)) == True{} : Bool}
72  for +b0: U32
73  for +b1: U32
74  for +b2: U32
75  for +b3: U32
76  for +b4: U32
77  for +b5: U32
78  for +b6: U32
79  for +b7: U32
80  for +b8: U32
81  for +b9: U32
82  for +b10: U32
83  for +b11: U32
84  for +b12: U32
85  for +b13: U32
86  for +b14: U32
87  for +b15: U32
88  {block_with(A.expand_key(key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{S.bytes_of(S.aes(key, S.state_of([b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15])))} : Maybe<&2, List<&2, U32>>}
89
90# A 16-, 24-, 32-byte key is AES-128 (Nk = 4, Nr = 10), AES-192 (6, 12),
91# AES-256 (8, 14).
92law Block.aes128:
93  for +key: List<&2, U32>
94  for +h: {List.length(&2, U32, key) == 16n : Nat}
95  {S.nk(key) == 4n : Nat}
96
97law Block.aes192:
98  for +key: List<&2, U32>
99  for +h: {List.length(&2, U32, key) == 24n : Nat}
100  {S.nk(key) == 6n : Nat}
101
102law Block.aes256:
103  for +key: List<&2, U32>
104  for +h: {List.length(&2, U32, key) == 32n : Nat}
105  {S.nk(key) == 8n : Nat}
106
107# ---- GCM (SP 800-38D) ----
108
109# The implementation's GCM-AE / GCM-AD, for every expanded key, 96-bit
110# nonce, AAD and input.
111law Gcm.seal:
112  for +nk: Nat
113  for +nr: Nat
114  for +key: List<&2, U32>
115  for +n0: U32
116  for +n1: U32
117  for +n2: U32
118  for +n3: U32
119  for +n4: U32
120  for +n5: U32
121  for +n6: U32
122  for +n7: U32
123  for +n8: U32
124  for +n9: U32
125  for +n10: U32
126  for +n11: U32
127  for +aad: List<&2, U32>
128  for +pt: List<&2, U32>
129  {GI.seal_core(A.Schedule{nr, A.expand(nk, nr, key)}, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, pt) == G.seal(nk, nr, key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) : List<&2, U32>}
130
131law Gcm.open:
132  for +nk: Nat
133  for +nr: Nat
134  for +key: List<&2, U32>
135  for +n0: U32
136  for +n1: U32
137  for +n2: U32
138  for +n3: U32
139  for +n4: U32
140  for +n5: U32
141  for +n6: U32
142  for +n7: U32
143  for +n8: U32
144  for +n9: U32
145  for +n10: U32
146  for +n11: U32
147  for +aad: List<&2, U32>
148  for +input: List<&2, U32>
149  {GI.open_core(A.Schedule{nr, A.expand(nk, nr, key)}, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, input) == G.open(nk, nr, key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, input) : Maybe<&2, List<&2, U32>>}
150
151# AEAD correctness of the specification: opening the sealed message gives
152# it back; C || T with T other than the tag of C is rejected.
153law Aead.roundtrip:
154  for +nk: Nat
155  for +nr: Nat
156  for +key: List<&2, U32>
157  for +iv: List<&2, U32>
158  for +aad: List<&2, U32>
159  for +pt: List<&2, U32>
160  {G.open(nk, nr, key, iv, aad, G.seal(nk, nr, key, iv, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
161
162law Aead.forgery:
163  for +nk: Nat
164  for +nr: Nat
165  for +key: List<&2, U32>
166  for +iv: List<&2, U32>
167  for +aad: List<&2, U32>
168  for +c: List<&2, U32>
169  for +t0: U32
170  for +t1: U32
171  for +t2: U32
172  for +t3: U32
173  for +t4: U32
174  for +t5: U32
175  for +t6: U32
176  for +t7: U32
177  for +t8: U32
178  for +t9: U32
179  for +t10: U32
180  for +t11: U32
181  for +t12: U32
182  for +t13: U32
183  for +t14: U32
184  for +t15: U32
185  for ne: {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15] != G.tag(nk, nr, key, iv, aad, c) : List<&2, U32>}
186  {G.open(nk, nr, key, iv, aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])) == None{} : Maybe<&2, List<&2, U32>>}
187
188# ---- the AES-128-GCM API (src/crypto/aesgcm.bend) ----
189
190law Api128.encrypt:
191  for +key: List<&2, U32>
192  for +h: {List.length(&2, U32, key) == 16n : Nat}
193  for +n0: U32
194  for +n1: U32
195  for +n2: U32
196  for +n3: U32
197  for +n4: U32
198  for +n5: U32
199  for +n6: U32
200  for +n7: U32
201  for +n8: U32
202  for +n9: U32
203  for +n10: U32
204  for +n11: U32
205  for +aad: List<&2, U32>
206  for +pt: List<&2, U32>
207  {GCM.aes128_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == Some{G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)} : Maybe<&2, List<&2, U32>>}
208
209law Api128.decrypt:
210  for +key: List<&2, U32>
211  for +h: {List.length(&2, U32, key) == 16n : Nat}
212  for +n0: U32
213  for +n1: U32
214  for +n2: U32
215  for +n3: U32
216  for +n4: U32
217  for +n5: U32
218  for +n6: U32
219  for +n7: U32
220  for +n8: U32
221  for +n9: U32
222  for +n10: U32
223  for +n11: U32
224  for +aad: List<&2, U32>
225  for +ct: List<&2, U32>
226  {GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) : Maybe<&2, List<&2, U32>>}
227
228# decrypt(encrypt(x)) == Some(x).
229law Api128.roundtrip:
230  for +key: List<&2, U32>
231  for +h: {List.length(&2, U32, key) == 16n : Nat}
232  for +n0: U32
233  for +n1: U32
234  for +n2: U32
235  for +n3: U32
236  for +n4: U32
237  for +n5: U32
238  for +n6: U32
239  for +n7: U32
240  for +n8: U32
241  for +n9: U32
242  for +n10: U32
243  for +n11: U32
244  for +aad: List<&2, U32>
245  for +pt: List<&2, U32>
246  {open128(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, GCM.aes128_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
247
248# A wrong tag gives None.
249law Api128.forgery:
250  for +key: List<&2, U32>
251  for +h: {List.length(&2, U32, key) == 16n : Nat}
252  for +n0: U32
253  for +n1: U32
254  for +n2: U32
255  for +n3: U32
256  for +n4: U32
257  for +n5: U32
258  for +n6: U32
259  for +n7: U32
260  for +n8: U32
261  for +n9: U32
262  for +n10: U32
263  for +n11: U32
264  for +aad: List<&2, U32>
265  for +c: List<&2, U32>
266  for +t0: U32
267  for +t1: U32
268  for +t2: U32
269  for +t3: U32
270  for +t4: U32
271  for +t5: U32
272  for +t6: U32
273  for +t7: U32
274  for +t8: U32
275  for +t9: U32
276  for +t10: U32
277  for +t11: U32
278  for +t12: U32
279  for +t13: U32
280  for +t14: U32
281  for +t15: U32
282  for ne: {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15] != G.aes_tag(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c) : List<&2, U32>}
283  {GCM.aes128_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])) == None{} : Maybe<&2, List<&2, U32>>}
284
285# A key of another length is rejected.
286law Api128.bad_key:
287  for +key: List<&2, U32>
288  for +h: {Nat.is_eq(List.length(&2, U32, key), 16n) == False{} : Bool}
289  for +nonce: List<&2, U32>
290  for +aad: List<&2, U32>
291  for +pt: List<&2, U32>
292  {GCM.aes128_gcm_encrypt(key, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
293
294law Api128.bad_key_open:
295  for +key: List<&2, U32>
296  for +h: {Nat.is_eq(List.length(&2, U32, key), 16n) == False{} : Bool}
297  for +nonce: List<&2, U32>
298  for +aad: List<&2, U32>
299  for +ct: List<&2, U32>
300  {GCM.aes128_gcm_decrypt(key, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}
301
302# A nonce other than 12 bytes is rejected.
303law Api128.bad_nonce:
304  for +key: List<&2, U32>
305  for +nonce: List<&2, U32>
306  for +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}
307  for +aad: List<&2, U32>
308  for +pt: List<&2, U32>
309  {GCM.aes128_gcm_encrypt(key, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
310
311law Api128.bad_nonce_open:
312  for +key: List<&2, U32>
313  for +nonce: List<&2, U32>
314  for +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}
315  for +aad: List<&2, U32>
316  for +ct: List<&2, U32>
317  {GCM.aes128_gcm_decrypt(key, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}
318
319# ---- the AES-256-GCM API (src/crypto/aesgcm.bend) ----
320
321law Api256.encrypt:
322  for +key: List<&2, U32>
323  for +h: {List.length(&2, U32, key) == 32n : Nat}
324  for +n0: U32
325  for +n1: U32
326  for +n2: U32
327  for +n3: U32
328  for +n4: U32
329  for +n5: U32
330  for +n6: U32
331  for +n7: U32
332  for +n8: U32
333  for +n9: U32
334  for +n10: U32
335  for +n11: U32
336  for +aad: List<&2, U32>
337  for +pt: List<&2, U32>
338  {GCM.aes256_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == Some{G.aes_seal(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)} : Maybe<&2, List<&2, U32>>}
339
340law Api256.decrypt:
341  for +key: List<&2, U32>
342  for +h: {List.length(&2, U32, key) == 32n : Nat}
343  for +n0: U32
344  for +n1: U32
345  for +n2: U32
346  for +n3: U32
347  for +n4: U32
348  for +n5: U32
349  for +n6: U32
350  for +n7: U32
351  for +n8: U32
352  for +n9: U32
353  for +n10: U32
354  for +n11: U32
355  for +aad: List<&2, U32>
356  for +ct: List<&2, U32>
357  {GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == G.aes_open(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) : Maybe<&2, List<&2, U32>>}
358
359# decrypt(encrypt(x)) == Some(x).
360law Api256.roundtrip:
361  for +key: List<&2, U32>
362  for +h: {List.length(&2, U32, key) == 32n : Nat}
363  for +n0: U32
364  for +n1: U32
365  for +n2: U32
366  for +n3: U32
367  for +n4: U32
368  for +n5: U32
369  for +n6: U32
370  for +n7: U32
371  for +n8: U32
372  for +n9: U32
373  for +n10: U32
374  for +n11: U32
375  for +aad: List<&2, U32>
376  for +pt: List<&2, U32>
377  {open256(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, GCM.aes256_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
378
379# A wrong tag gives None.
380law Api256.forgery:
381  for +key: List<&2, U32>
382  for +h: {List.length(&2, U32, key) == 32n : Nat}
383  for +n0: U32
384  for +n1: U32
385  for +n2: U32
386  for +n3: U32
387  for +n4: U32
388  for +n5: U32
389  for +n6: U32
390  for +n7: U32
391  for +n8: U32
392  for +n9: U32
393  for +n10: U32
394  for +n11: U32
395  for +aad: List<&2, U32>
396  for +c: List<&2, U32>
397  for +t0: U32
398  for +t1: U32
399  for +t2: U32
400  for +t3: U32
401  for +t4: U32
402  for +t5: U32
403  for +t6: U32
404  for +t7: U32
405  for +t8: U32
406  for +t9: U32
407  for +t10: U32
408  for +t11: U32
409  for +t12: U32
410  for +t13: U32
411  for +t14: U32
412  for +t15: U32
413  for ne: {[t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15] != G.aes_tag(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, c) : List<&2, U32>}
414  {GCM.aes256_gcm_decrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, List.append(&2, U32, c, [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15])) == None{} : Maybe<&2, List<&2, U32>>}
415
416# A key of another length is rejected.
417law Api256.bad_key:
418  for +key: List<&2, U32>
419  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == False{} : Bool}
420  for +nonce: List<&2, U32>
421  for +aad: List<&2, U32>
422  for +pt: List<&2, U32>
423  {GCM.aes256_gcm_encrypt(key, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
424
425law Api256.bad_key_open:
426  for +key: List<&2, U32>
427  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == False{} : Bool}
428  for +nonce: List<&2, U32>
429  for +aad: List<&2, U32>
430  for +ct: List<&2, U32>
431  {GCM.aes256_gcm_decrypt(key, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}
432
433# A nonce other than 12 bytes is rejected.
434law Api256.bad_nonce:
435  for +key: List<&2, U32>
436  for +nonce: List<&2, U32>
437  for +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}
438  for +aad: List<&2, U32>
439  for +pt: List<&2, U32>
440  {GCM.aes256_gcm_encrypt(key, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
441
442law Api256.bad_nonce_open:
443  for +key: List<&2, U32>
444  for +nonce: List<&2, U32>
445  for +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}
446  for +aad: List<&2, U32>
447  for +ct: List<&2, U32>
448  {GCM.aes256_gcm_decrypt(key, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}