1	import Base
2	import ../../lib/logic.bend as L
3	import ../../../src/crypto/aes/types.bend as T
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	import ./laws.bend as Laws
10	import ./sbox.bend as SB
11	import ./inverse.bend as INV
12	import ./cipher.bend as C
13	import ./gcm.bend as GP
14	import ./aead.bend as AD
15	import ./api.bend as API
16	
17	# Generated by tools/generators/aes/proof.py.
18	
19	# Gate for AES and AES-GCM: `bend proofs/crypto/aes/proof.bend` checks every
20	# clause of laws.bend, for every input:
21	#   sbox.bend    the S-box circuit and the doublings, on all 256 bytes
22	#   cipher.bend  SubBytes .. AddRoundKey, the rounds, KeyExpansion, Cipher
23	#   gf.bend      polynomial product mod m == Algorithm 1 (any modulus)
24	#   ghash*.bend  the word-level GHASH == SP 800-38D's GHASH
25	#   gcm.bend     GCTR, the tag, GCM-AE and GCM-AD == SP 800-38D
26	#   aead.bend    open(seal(x)) == Some(x); a wrong tag gives None
27	# The key size stays symbolic (Nk = length/4) so that no key expansion is
28	# ever unfolded at a concrete size.
29	
30	# A nonce that is not 12 bytes long: None.
31	def seal_nonce_bad(+sched: A.Schedule, +nonce: List<&2, U32>, +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}, +aad: List<&2, U32>, +pt: List<&2, U32>) -> {GI.seal_nonce(sched, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}:
32	  match nonce:
33	    case Nil{}:
34	      {==}
35	    case n0 <> Nil{}:
36	      {==}
37	    case n0 <> n1 <> Nil{}:
38	      {==}
39	    case n0 <> n1 <> n2 <> Nil{}:
40	      {==}
41	    case n0 <> n1 <> n2 <> n3 <> Nil{}:
42	      {==}
43	    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}:
44	      {==}
45	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}:
46	      {==}
47	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}:
48	      {==}
49	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}:
50	      {==}
51	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}:
52	      {==}
53	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}:
54	      {==}
55	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}:
56	      {==}
57	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}:
58	      Empty.absurd({GI.seal_nonce(sched, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt) == None{} : Maybe<&2, List<&2, U32>>}, L.true_false(h))
59	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> n12 <> rest:
60	      {==}
61	
62	def open_nonce_bad(+sched: A.Schedule, +nonce: List<&2, U32>, +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}, +aad: List<&2, U32>, +ct: List<&2, U32>) -> {GI.open_nonce(sched, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}:
63	  match nonce:
64	    case Nil{}:
65	      {==}
66	    case n0 <> Nil{}:
67	      {==}
68	    case n0 <> n1 <> Nil{}:
69	      {==}
70	    case n0 <> n1 <> n2 <> Nil{}:
71	      {==}
72	    case n0 <> n1 <> n2 <> n3 <> Nil{}:
73	      {==}
74	    case n0 <> n1 <> n2 <> n3 <> n4 <> Nil{}:
75	      {==}
76	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> Nil{}:
77	      {==}
78	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> Nil{}:
79	      {==}
80	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> Nil{}:
81	      {==}
82	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> Nil{}:
83	      {==}
84	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> Nil{}:
85	      {==}
86	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> Nil{}:
87	      {==}
88	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> Nil{}:
89	      Empty.absurd({GI.open_nonce(sched, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, ct) == None{} : Maybe<&2, List<&2, U32>>}, L.true_false(h))
90	    case n0 <> n1 <> n2 <> n3 <> n4 <> n5 <> n6 <> n7 <> n8 <> n9 <> n10 <> n11 <> n12 <> rest:
91	      {==}
92	
93	def seal_key_bad(+m: Maybe<&2, A.Schedule>, +nonce: List<&2, U32>, +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}, +aad: List<&2, U32>, +pt: List<&2, U32>) -> {GI.seal_key(m, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}:
94	  match m:
95	    case None{}:
96	      {==}
97	    case Some{s}:
98	      seal_nonce_bad(s, nonce, h, aad, pt)
99	
100	def open_key_bad(+m: Maybe<&2, A.Schedule>, +nonce: List<&2, U32>, +h: {Nat.is_eq(List.length(&2, U32, nonce), 12n) == False{} : Bool}, +aad: List<&2, U32>, +ct: List<&2, U32>) -> {GI.open_key(m, nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}:
101	  match m:
102	    case None{}:
103	      {==}
104	    case Some{s}:
105	      open_nonce_bad(s, nonce, h, aad, ct)
106	
107	# A key of w bytes, w one of 16, 24, 32, passes the length check.
108	def valid_of(+key: List<&2, U32>, +w: Nat, +h: {List.length(&2, U32, key) == w : Nat}, +v: {A.valid_length(w) == True{} : Bool}) -> {A.valid_length(List.length(&2, U32, key)) == True{} : Bool}:
109	  %Equal.sym(Nat, List.length(&2, U32, key), w, h) : {A.valid_length(_) == True{} : Bool}
110	  v
111	
112	def Laws.Sbox.value(x):
113	  SB.sbox_ok(x)
114	
115	def Laws.Inverse.unit(x, h):
116	  INV.inverse_unit(x, h)
117	
118	def Laws.Inverse.zero():
119	  INV.inverse_zero()
120	
121	def Laws.Cipher.value(nk, nr, key, s):
122	  C.encrypt_ok(nk, nr, key, s)
123	
124	def Laws.Block.value(key, h, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15):
125	  %Equal.sym(Bool, A.valid_length(List.length(&2, U32, key)), True{}, h) : {Laws.block_with(A.schedule_if(_, Nat.div(List.length(&2, U32, key), 4n), 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>>}
126	  %C.encrypt_ok(S.nk(key), S.nr(key), key, T.S{T.W{b0, b1, b2, b3}, T.W{b4, b5, b6, b7}, T.W{b8, b9, b10, b11}, T.W{b12, b13, b14, b15}}) : {Laws.block_with(A.schedule_if(True{}, Nat.div(List.length(&2, U32, key), 4n), key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{S.bytes_of(_)} : Maybe<&2, List<&2, U32>>}
127	  %GP.bytes_of_ok(A.encrypt(S.nk(key), S.nr(key), key, T.S{T.W{b0, b1, b2, b3}, T.W{b4, b5, b6, b7}, T.W{b8, b9, b10, b11}, T.W{b12, b13, b14, b15}})) : {Laws.block_with(A.schedule_if(True{}, Nat.div(List.length(&2, U32, key), 4n), key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{_} : Maybe<&2, List<&2, U32>>}
128	  {==}
129	
130	def Laws.Block.aes128(key, h):
131	  %Equal.sym(Nat, List.length(&2, U32, key), 16n, h) : {Nat.div(_, 4n) == 4n : Nat}
132	  {==}
133	
134	def Laws.Block.aes192(key, h):
135	  %Equal.sym(Nat, List.length(&2, U32, key), 24n, h) : {Nat.div(_, 4n) == 6n : Nat}
136	  {==}
137	
138	def Laws.Block.aes256(key, h):
139	  %Equal.sym(Nat, List.length(&2, U32, key), 32n, h) : {Nat.div(_, 4n) == 8n : Nat}
140	  {==}
141	
142	def Laws.Gcm.seal(nk, nr, key, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
143	  GP.seal_ok(nk, nr, key, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, pt)
144	
145	def Laws.Gcm.open(nk, nr, key, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, input):
146	  GP.open_ok(nk, nr, key, T.W{n0, n1, n2, n3}, T.W{n4, n5, n6, n7}, T.W{n8, n9, n10, n11}, aad, input)
147	
148	def Laws.Aead.roundtrip(nk, nr, key, iv, aad, pt):
149	  AD.roundtrip(nk, nr, key, iv, aad, pt)
150	
151	def Laws.Aead.forgery(nk, nr, key, iv, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne):
152	  AD.forgery(nk, nr, key, iv, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)
153	
154	def Laws.Api128.encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
155	  API.aes128_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)
156	
157	def Laws.Api128.decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct):
158	  API.aes128_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct)
159	
160	law open128_same:
161	  for +key: List<&2, U32>
162	  for +nonce: List<&2, U32>
163	  for +aad: List<&2, U32>
164	  for +m: Maybe<&2, List<&2, U32>>
165	  {Laws.open128(key, nonce, aad, m) == API.open128(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}
166	
167	def open128_same(key, nonce, aad, m):
168	  match m:
169	    case None{}: {==}
170	    case Some{c}: {==}
171	
172	def Laws.Api128.roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
173	  +m = GCM.aes128_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)
174	  Equal.trans(Maybe<&2, List<&2, U32>>, Laws.open128(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.open128(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), Some{pt}, open128_same(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.aes128_roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt))
175	
176	def Laws.Api128.forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne):
177	  API.aes128_forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)
178	
179	def Laws.Api128.bad_key(key, h, nonce, aad, pt):
180	  %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 16n), False{}, h) : {GI.seal_key(GI.schedule_if(_, key), nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
181	  {==}
182	
183	def Laws.Api128.bad_key_open(key, h, nonce, aad, ct):
184	  %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 16n), False{}, h) : {GI.open_key(GI.schedule_if(_, key), nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}
185	  {==}
186	
187	def Laws.Api128.bad_nonce(key, nonce, h, aad, pt):
188	  seal_key_bad(GI.schedule_of(16n, key), nonce, h, aad, pt)
189	
190	def Laws.Api128.bad_nonce_open(key, nonce, h, aad, ct):
191	  open_key_bad(GI.schedule_of(16n, key), nonce, h, aad, ct)
192	
193	def Laws.Api256.encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
194	  API.aes256_encrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt)
195	
196	def Laws.Api256.decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct):
197	  API.aes256_decrypt(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, ct)
198	
199	law open256_same:
200	  for +key: List<&2, U32>
201	  for +nonce: List<&2, U32>
202	  for +aad: List<&2, U32>
203	  for +m: Maybe<&2, List<&2, U32>>
204	  {Laws.open256(key, nonce, aad, m) == API.open256(key, nonce, aad, m) : Maybe<&2, List<&2, U32>>}
205	
206	def open256_same(key, nonce, aad, m):
207	  match m:
208	    case None{}: {==}
209	    case Some{c}: {==}
210	
211	def Laws.Api256.roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt):
212	  +m = GCM.aes256_gcm_encrypt(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, pt)
213	  Equal.trans(Maybe<&2, List<&2, U32>>, Laws.open256(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.open256(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), Some{pt}, open256_same(key, [n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11], aad, m), API.aes256_roundtrip(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, pt))
214	
215	def Laws.Api256.forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne):
216	  API.aes256_forgery(key, h, n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, aad, c, t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, ne)
217	
218	def Laws.Api256.bad_key(key, h, nonce, aad, pt):
219	  %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 32n), False{}, h) : {GI.seal_key(GI.schedule_if(_, key), nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
220	  {==}
221	
222	def Laws.Api256.bad_key_open(key, h, nonce, aad, ct):
223	  %Equal.sym(Bool, Nat.is_eq(List.length(&2, U32, key), 32n), False{}, h) : {GI.open_key(GI.schedule_if(_, key), nonce, aad, ct) == None{} : Maybe<&2, List<&2, U32>>}
224	  {==}
225	
226	def Laws.Api256.bad_nonce(key, nonce, h, aad, pt):
227	  seal_key_bad(GI.schedule_of(32n, key), nonce, h, aad, pt)
228	
229	def Laws.Api256.bad_nonce_open(key, nonce, h, aad, ct):
230	  open_key_bad(GI.schedule_of(32n, key), nonce, h, aad, ct)
231