~/jendhub

proofs/crypto/aes/proof.bend

bend-collections-laws-crypto@1.0.0.0 · 231 lines · 7 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
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
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/laws.bend as Laws
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/sbox.bend as SB
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/inverse.bend as INV
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend as C
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gcm.bend as GP
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend as AD
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/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.
31def 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
62def 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
93def 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
100def 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.
108def 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
112def Laws.Sbox.value(x):
113  SB.sbox_ok(x)
114
115def Laws.Inverse.unit(x, h):
116  INV.inverse_unit(x, h)
117
118def Laws.Inverse.zero():
119  INV.inverse_zero()
120
121def Laws.Cipher.value(nk, nr, key, s):
122  C.encrypt_ok(nk, nr, key, s)
123
124def 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
130def Laws.Block.aes128(key, h):
131  %Equal.sym(Nat, List.length(&2, U32, key), 16n, h) : {Nat.div(_, 4n) == 4n : Nat}
132  {==}
133
134def Laws.Block.aes192(key, h):
135  %Equal.sym(Nat, List.length(&2, U32, key), 24n, h) : {Nat.div(_, 4n) == 6n : Nat}
136  {==}
137
138def Laws.Block.aes256(key, h):
139  %Equal.sym(Nat, List.length(&2, U32, key), 32n, h) : {Nat.div(_, 4n) == 8n : Nat}
140  {==}
141
142def 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
145def 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
148def Laws.Aead.roundtrip(nk, nr, key, iv, aad, pt):
149  AD.roundtrip(nk, nr, key, iv, aad, pt)
150
151def 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
154def 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
157def 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
160law 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
167def open128_same(key, nonce, aad, m):
168  match m:
169    case None{}: {==}
170    case Some{c}: {==}
171
172def 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
176def 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
179def 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
183def 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
187def Laws.Api128.bad_nonce(key, nonce, h, aad, pt):
188  seal_key_bad(GI.schedule_of(16n, key), nonce, h, aad, pt)
189
190def Laws.Api128.bad_nonce_open(key, nonce, h, aad, ct):
191  open_key_bad(GI.schedule_of(16n, key), nonce, h, aad, ct)
192
193def 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
196def 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
199law 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
206def open256_same(key, nonce, aad, m):
207  match m:
208    case None{}: {==}
209    case Some{c}: {==}
210
211def 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
215def 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
218def 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
222def 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
226def Laws.Api256.bad_nonce(key, nonce, h, aad, pt):
227  seal_key_bad(GI.schedule_of(32n, key), nonce, h, aad, pt)
228
229def Laws.Api256.bad_nonce_open(key, nonce, h, aad, ct):
230  open_key_bad(GI.schedule_of(32n, key), nonce, h, aad, ct)
231