proof/AES_MaskedXorProof.bend
qasim-bend-kit@0.1.0.2 · 360 lines · 14 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
3import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
4import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as ZipLengthProof
5import qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend as LengthLimitProof
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as HubU32
7
8def bool_mask_xor_inv(+mask: Bool, +x: Bool, +y: Bool) ->
9 {Bool.and(mask,
10 Bool.xor(Bool.and(mask, Bool.xor(x, y)), y)) ==
11 Bool.and(mask, x) : Bool}:
12 match mask x y:
13 case False{} False{} False{}: {==}
14 case False{} False{} True{}: {==}
15 case False{} True{} False{}: {==}
16 case False{} True{} True{}: {==}
17 case True{} False{} False{}: {==}
18 case True{} False{} True{}: {==}
19 case True{} True{} False{}: {==}
20 case True{} True{} True{}: {==}
21
22def word_mask_xor_inv(+n: Nat, +mask: Word(n), +x: Word(n), +y: Word(n)) ->
23 {Word.and(n, mask,
24 Word.xor(n, Word.and(n, mask, Word.xor(n, x, y)), y)) ==
25 Word.and(n, mask, x) : Word(n)}:
26 match n mask x y:
27 case 0n WNil{} WNil{} WNil{}: {==}
28 case 1n+p WCon{m, mt} WCon{xb, xt} WCon{yb, yt}:
29 head = bool_mask_xor_inv(m, xb, yb)
30 tail = word_mask_xor_inv(p, mt, xt, yt)
31 Equal.trans(Word(1n+p),
32 Word.and(1n+p, WCon{m, mt},
33 Word.xor(1n+p,
34 Word.and(1n+p, WCon{m, mt},
35 Word.xor(1n+p, WCon{xb, xt}, WCon{yb, yt})),
36 WCon{yb, yt})),
37 WCon{Bool.and(m,
38 Bool.xor(Bool.and(m, Bool.xor(xb, yb)), yb)),
39 Word.and(p, mt,
40 Word.xor(p, Word.and(p, mt,
41 Word.xor(p, xt, yt)), yt))},
42 WCon{Bool.and(m, xb), Word.and(p, mt, xt)},
43 {==},
44 Equal.trans(Word(1n+p),
45 WCon{Bool.and(m,
46 Bool.xor(Bool.and(m, Bool.xor(xb, yb)), yb)),
47 Word.and(p, mt,
48 Word.xor(p, Word.and(p, mt,
49 Word.xor(p, xt, yt)), yt))},
50 WCon{Bool.and(m, xb),
51 Word.and(p, mt,
52 Word.xor(p, Word.and(p, mt,
53 Word.xor(p, xt, yt)), yt))},
54 WCon{Bool.and(m, xb), Word.and(p, mt, xt)},
55 Equal.cong(Bool, Word(1n+p),
56 bit => WCon{bit,
57 Word.and(p, mt,
58 Word.xor(p, Word.and(p, mt,
59 Word.xor(p, xt, yt)), yt))},
60 Bool.and(m,
61 Bool.xor(Bool.and(m, Bool.xor(xb, yb)), yb)),
62 Bool.and(m, xb), head),
63 Equal.cong(Word(p), Word(1n+p),
64 bits => WCon{Bool.and(m, xb), bits},
65 Word.and(p, mt,
66 Word.xor(p, Word.and(p, mt,
67 Word.xor(p, xt, yt)), yt)),
68 Word.and(p, mt, xt), tail)))
69
70def word_bits(+value: U32) -> Word(32n):
71 match value:
72 case U32{bits}: bits
73
74def gcm_mask_xor_inv(+x: U32, +y: U32) ->
75 {Core.gcm_hex_mask(
76 U32.xor(Core.gcm_hex_mask(U32.xor(x, y), 255), y), 255) ==
77 Core.gcm_hex_mask(x, 255) : U32}:
78 match x y:
79 case U32{xb} U32{yb}:
80 Equal.cong(Word(32n), U32, bits => U32{bits},
81 Word.and(32n, word_bits(255),
82 Word.xor(32n,
83 Word.and(32n, word_bits(255),
84 Word.xor(32n, xb, yb)), yb)),
85 Word.and(32n, word_bits(255), xb),
86 word_mask_xor_inv(32n, word_bits(255), xb, yb))
87
88def bool_and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}:
89 match a b:
90 case False{} False{}: {==}
91 case False{} True{}: {==}
92 case True{} False{}: {==}
93 case True{} True{}: {==}
94
95def word_and_comm(+n: Nat, +x: Word(n), +y: Word(n)) ->
96 {Word.and(n, x, y) == Word.and(n, y, x) : Word(n)}:
97 match n x y:
98 case 0n WNil{} WNil{}: {==}
99 case 1n+p WCon{xb, xt} WCon{yb, yt}:
100 head = bool_and_comm(xb, yb)
101 tail = word_and_comm(p, xt, yt)
102 Equal.trans(Word(1n+p),
103 Word.and(1n+p, WCon{xb, xt}, WCon{yb, yt}),
104 WCon{Bool.and(xb, yb), Word.and(p, xt, yt)},
105 Word.and(1n+p, WCon{yb, yt}, WCon{xb, xt}),
106 {==},
107 Equal.trans(Word(1n+p),
108 WCon{Bool.and(xb, yb), Word.and(p, xt, yt)},
109 WCon{Bool.and(yb, xb), Word.and(p, xt, yt)},
110 WCon{Bool.and(yb, xb), Word.and(p, yt, xt)},
111 Equal.cong(Bool, Word(1n+p),
112 bit => WCon{bit, Word.and(p, xt, yt)},
113 Bool.and(xb, yb), Bool.and(yb, xb), head),
114 Equal.cong(Word(p), Word(1n+p),
115 bits => WCon{Bool.and(yb, xb), bits},
116 Word.and(p, xt, yt), Word.and(p, yt, xt), tail)))
117
118def byte_mask_identity(+value: U32,
119 below_256: {U32.is_lt(value, 256) == True{} : Bool}) ->
120 {Core.gcm_hex_mask(value, 255) == value : U32}:
121 match value:
122 case U32{bits}:
123 nat_below = Equal.trans(Bool,
124 Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)),
125 U32.is_lt(U32{bits}, 256),
126 True{},
127 Equal.sym(Bool,
128 U32.is_lt(U32{bits}, 256),
129 Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)),
130 HubU32.is_lt_nat(U32{bits}, 256)),
131 below_256)
132 scaled_below = Equal.trans(Bool,
133 Nat.is_lt(U32.to_nat(U32{bits}), U32.to_nat(256)),
134 Nat.is_lt(U32.to_nat(U32{bits}), 256n),
135 True{},
136 Equal.cong(Nat, Bool,
137 bound => Nat.is_lt(U32.to_nat(U32{bits}), bound),
138 U32.to_nat(256), 256n, {==}),
139 nat_below)
140 masked = HubU32.mask_word(U32{bits}, 255, 8n,
141 {==}, scaled_below)
142 Equal.trans(U32,
143 Core.gcm_hex_mask(U32{bits}, 255),
144 U32.and(255, U32{bits}),
145 U32{bits}, {==},
146 Equal.trans(U32,
147 U32.and(255, U32{bits}),
148 U32.and(U32{bits}, 255),
149 U32{bits},
150 Equal.cong(Word(32n), U32, w => U32{w},
151 Word.and(32n, word_bits(255), bits),
152 Word.and(32n, bits, word_bits(255)),
153 word_and_comm(32n, word_bits(255), bits)),
154 masked))
155
156def bool_and_true_left(+a: Bool, +b: Bool,
157 both: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
158 match a b:
159 case False{} False{}:
160 Empty.absurd({False{} == True{} : Bool},
161 ZipLengthProof.false_true(both))
162 case False{} True{}:
163 Empty.absurd({False{} == True{} : Bool},
164 ZipLengthProof.false_true(both))
165 case True{} False{}: {==}
166 case True{} True{}: {==}
167
168def bool_and_true_right(+a: Bool, +b: Bool,
169 both: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
170 match a b:
171 case False{} False{}:
172 Empty.absurd({False{} == True{} : Bool},
173 ZipLengthProof.false_true(both))
174 case False{} True{}: {==}
175 case True{} False{}:
176 Empty.absurd({False{} == True{} : Bool},
177 ZipLengthProof.false_true(both))
178 case True{} True{}: {==}
179
180def mask_bytes_identity(+bytes: List<&2, U32>,
181 +valid: {Core.gcm_bytes_valid(bytes) == True{} : Bool}) ->
182 {Core.gcm_mask_bytes(bytes) == bytes : List<&2, U32>}:
183 match bytes:
184 case Nil{}: {==}
185 case byte <> tail:
186 head_valid = bool_and_true_left(U32.is_lt(byte, 256),
187 Core.gcm_bytes_valid(tail), valid)
188 tail_valid = bool_and_true_right(U32.is_lt(byte, 256),
189 Core.gcm_bytes_valid(tail), valid)
190 recursive = mask_bytes_identity(tail, tail_valid)
191 Equal.trans(List<&2, U32>,
192 Core.gcm_mask_bytes(byte <> tail),
193 byte <> Core.gcm_mask_bytes(tail),
194 byte <> tail,
195 Equal.cong(U32, List<&2, U32>,
196 head => head <> Core.gcm_mask_bytes(tail),
197 Core.gcm_hex_mask(byte, 255), byte,
198 byte_mask_identity(byte, head_valid)),
199 Equal.cong(List<&2, U32>, List<&2, U32>,
200 rest => byte <> rest,
201 Core.gcm_mask_bytes(tail), tail, recursive))
202
203def predecessor(n: Nat) -> Nat:
204 match n:
205 case 0n: 0n
206 case 1n+p: p
207
208def zip_xor_involution(+bytes: List<&2, U32>,
209 +stream: List<&2, U32>,
210 same_length: {List.length(&2, U32, bytes) ==
211 List.length(&2, U32, stream) : Nat}) ->
212 {Core.gcm_zip_xor(Core.gcm_zip_xor(bytes, stream), stream) ==
213 Core.gcm_mask_bytes(bytes) : List<&2, U32>}:
214 match bytes stream:
215 case Nil{} _:
216 +inner = Core.gcm_zip_xor_nil_left(stream)
217 Equal.trans(List<&2, U32>,
218 Core.gcm_zip_xor(Core.gcm_zip_xor(Nil{}, stream), stream),
219 Core.gcm_zip_xor(Nil{}, stream), Nil{},
220 Equal.cong(List<&2, U32>, List<&2, U32>,
221 xs => Core.gcm_zip_xor(xs, stream),
222 Core.gcm_zip_xor(Nil{}, stream), Nil{}, inner),
223 inner)
224 case _ <> _ Nil{}:
225 unequal = Equal.cong(Nat, Bool,
226 n => Nat.is_eq(n, 0n),
227 List.length(&2, U32, bytes),
228 List.length(&2, U32, Nil{}), same_length)
229 Empty.absurd(
230 {Core.gcm_zip_xor(Core.gcm_zip_xor(bytes, Nil{}), Nil{}) ==
231 Core.gcm_mask_bytes(bytes) : List<&2, U32>},
232 ZipLengthProof.false_true(unequal))
233 case byte <> tail stream_byte <> stream_tail:
234 tail_length = Equal.cong(Nat, Nat, predecessor,
235 List.length(&2, U32, byte <> tail),
236 List.length(&2, U32, stream_byte <> stream_tail),
237 same_length)
238 recursive = zip_xor_involution(tail, stream_tail, tail_length)
239 Equal.trans(List<&2, U32>,
240 Core.gcm_zip_xor(
241 Core.gcm_zip_xor(byte <> tail,
242 stream_byte <> stream_tail),
243 stream_byte <> stream_tail),
244 Core.gcm_hex_mask(U32.xor(
245 Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255),
246 stream_byte), 255) <>
247 Core.gcm_zip_xor(
248 Core.gcm_zip_xor(tail, stream_tail), stream_tail),
249 Core.gcm_mask_bytes(byte <> tail),
250 {==},
251 Equal.trans(List<&2, U32>,
252 Core.gcm_hex_mask(U32.xor(
253 Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255),
254 stream_byte), 255) <>
255 Core.gcm_zip_xor(
256 Core.gcm_zip_xor(tail, stream_tail), stream_tail),
257 Core.gcm_hex_mask(byte, 255) <>
258 Core.gcm_zip_xor(
259 Core.gcm_zip_xor(tail, stream_tail), stream_tail),
260 Core.gcm_mask_bytes(byte <> tail),
261 Equal.cong(U32, List<&2, U32>,
262 head => head <>
263 Core.gcm_zip_xor(
264 Core.gcm_zip_xor(tail, stream_tail), stream_tail),
265 Core.gcm_hex_mask(U32.xor(
266 Core.gcm_hex_mask(U32.xor(byte, stream_byte), 255),
267 stream_byte), 255),
268 Core.gcm_hex_mask(byte, 255),
269 gcm_mask_xor_inv(byte, stream_byte)),
270 Equal.cong(List<&2, U32>, List<&2, U32>,
271 rest => Core.gcm_hex_mask(byte, 255) <> rest,
272 Core.gcm_zip_xor(
273 Core.gcm_zip_xor(tail, stream_tail), stream_tail),
274 Core.gcm_mask_bytes(tail), recursive)))
275
276def ctr_decrypt_ciphertext_roundtrip(+words: List<&2, U32>,
277 +nonce: List<&2, U32>, +plaintext: List<&2, U32>,
278 +valid: {Core.gcm_bytes_valid(plaintext) == True{} : Bool}) ->
279 {Core.gcm_decrypt_expanded(words, nonce,
280 Core.gcm_zip_xor(plaintext,
281 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
282 words, Core.gcm_inc32(Core.gcm_j0(nonce))))) ==
283 plaintext : List<&2, U32>}:
284 +start = Core.gcm_inc32(Core.gcm_j0(nonce))
285 +stream = Core.gcm_ctr_stream_exact(
286 List.length(&2, U32, plaintext), words, start)
287 +same_length = Equal.sym(Nat,
288 List.length(&2, U32, stream),
289 List.length(&2, U32, plaintext),
290 ZipLengthProof.ctr_stream_exact_length(
291 List.length(&2, U32, plaintext), words, start))
292 cipher_length = ZipLengthProof.zip_length_equal(plaintext, stream,
293 same_length)
294 decrypt_stream = Equal.cong(Nat, List<&2, U32>,
295 fuel => Core.gcm_ctr_stream_exact(fuel, words, start),
296 List.length(&2, U32,
297 Core.gcm_zip_xor(plaintext, stream)),
298 List.length(&2, U32, plaintext), cipher_length)
299 Equal.trans(List<&2, U32>,
300 Core.gcm_decrypt_expanded(words, nonce,
301 Core.gcm_zip_xor(plaintext, stream)),
302 Core.gcm_zip_xor(Core.gcm_zip_xor(plaintext, stream), stream),
303 plaintext,
304 Equal.cong(List<&2, U32>, List<&2, U32>,
305 stream2 => Core.gcm_zip_xor(
306 Core.gcm_zip_xor(plaintext, stream), stream2),
307 Core.gcm_ctr_stream_exact(
308 List.length(&2, U32,
309 Core.gcm_zip_xor(plaintext, stream)), words, start),
310 stream, decrypt_stream),
311 Equal.trans(List<&2, U32>,
312 Core.gcm_zip_xor(Core.gcm_zip_xor(plaintext, stream), stream),
313 Core.gcm_mask_bytes(plaintext), plaintext,
314 zip_xor_involution(plaintext, stream, same_length),
315 mask_bytes_identity(plaintext, valid)))
316
317def ctr_ciphertext_plaintext_valid(+plaintext: List<&2, U32>,
318 +stream: List<&2, U32>,
319 same_length: {List.length(&2, U32, plaintext) ==
320 List.length(&2, U32, stream) : Nat},
321 +plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}) ->
322 {AES.plaintext_valid(Core.gcm_zip_xor(plaintext, stream)) ==
323 True{} : Bool}:
324 +ciphertext = Core.gcm_zip_xor(plaintext, stream)
325 cipher_length = ZipLengthProof.zip_length_equal(plaintext, stream,
326 same_length)
327 output_bytes_ok = AES.core_bytes_valid_proof(ciphertext,
328 Core.gcm_zip_xor_valid(plaintext, stream))
329 plaintext_limit_ok = bool_and_true_right(AES.bytes_valid(plaintext),
330 AES.bytes_length_limit(plaintext, 4294967264, 15), plaintext_ok)
331 output_limit_eq = LengthLimitProof.bytes_length_limit_same(plaintext,
332 ciphertext, 4294967264, 15, Equal.sym(Nat,
333 List.length(&2, U32, ciphertext),
334 List.length(&2, U32, plaintext), cipher_length))
335 output_limit_ok = Equal.trans(Bool,
336 AES.bytes_length_limit(ciphertext, 4294967264, 15),
337 AES.bytes_length_limit(plaintext, 4294967264, 15),
338 True{}, Equal.sym(Bool,
339 AES.bytes_length_limit(plaintext, 4294967264, 15),
340 AES.bytes_length_limit(ciphertext, 4294967264, 15),
341 output_limit_eq), plaintext_limit_ok)
342 Equal.trans(Bool, AES.plaintext_valid(ciphertext),
343 Bool.and(AES.bytes_valid(ciphertext),
344 AES.bytes_length_limit(ciphertext, 4294967264, 15)),
345 True{}, {==},
346 Equal.trans(Bool,
347 Bool.and(AES.bytes_valid(ciphertext),
348 AES.bytes_length_limit(ciphertext, 4294967264, 15)),
349 Bool.and(True{},
350 AES.bytes_length_limit(ciphertext, 4294967264, 15)),
351 True{},
352 Equal.cong(Bool, Bool,
353 byte_ok => Bool.and(byte_ok,
354 AES.bytes_length_limit(ciphertext, 4294967264, 15)),
355 AES.bytes_valid(ciphertext), True{}, output_bytes_ok),
356 Equal.trans(Bool,
357 Bool.and(True{},
358 AES.bytes_length_limit(ciphertext, 4294967264, 15)),
359 AES.bytes_length_limit(ciphertext, 4294967264, 15),
360 True{}, {==}, output_limit_ok)))