1	import Base
2	import ../../../src/crypto/aes/types.bend as T
3	import ../../../src/crypto/aes/sbox.bend as B
4	import ../../../src/crypto/aes/aes.bend as A
5	import ../../../src/crypto/aes/gcm.bend as GI
6	import ../../../src/crypto/aesgcm.bend as GCM
7	import ../../../spec/crypto/aes/aes.bend as S
8	import ../../../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).
17	def 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).
25	def 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	
32	def 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.
43	law 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".
50	law 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	
55	law 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.
60	law 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).
69	law 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).
92	law 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	
97	law 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	
102	law 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.
111	law 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	
131	law 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.
153	law 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	
162	law 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	
190	law 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	
209	law 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).
229	law 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.
249	law 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.
286	law 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	
294	law 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.
303	law 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	
311	law 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	
321	law 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	
340	law 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).
360	law 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.
380	law 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.
417	law 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	
425	law 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.
434	law 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	
442	law 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>>}