proof/AES_EncryptProof.bend
qasim-bend-kit@0.1.0.2 · 654 lines · 32 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_CoreTagProof.bend as CoreTagProof
6import qasim-bend-kit@0.1.0.2/proof/AES_MaskedXorProof.bend as MaskedXorProof
7import qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend as LengthLimitProof
8import qasim-bend-kit@0.1.0.2/proof/AES_TagCompareProof.bend as TagCompareProof
9
10type TagContext is Data:
11 TagContext{
12 words: List<&2, U32>,
13 nonce: List<&2, U32>,
14 aad: List<&2, U32>,
15 ciphertext: List<&2, U32>
16 }
17
18def result_ciphertext(fallback: List<&2, U32>,
19 result: Result<&2, &2, AES.Error, AES.Envelope>) -> List<&2, U32>:
20 match result:
21 case Fail{error}: fallback
22 case Done{envelope}: AES.ciphertext(envelope)
23
24def output_tag_context(output: Core.GcmOutput) -> TagContext:
25 match output:
26 case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
27 tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
28 TagContext{tag_words, tag_nonce, tag_aad, ciphertext}
29
30def tag_for_context(context: TagContext) -> List<&2, U32>:
31 match context:
32 case TagContext{words, nonce, aad, ciphertext}:
33 Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad,
34 ciphertext))
35
36def output_tag_matches_context(+output: Core.GcmOutput) ->
37 {CoreTagProof.output_tag(output) ==
38 tag_for_context(output_tag_context(output)) : List<&2, U32>}:
39 match output:
40 case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
41 tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
42 tag_matches
43
44def raw_output_tag_canonical(+key: List<&2, U32>,
45 +nonce: List<&2, U32>, +aad: List<&2, U32>,
46 +plaintext: List<&2, U32>) ->
47 {CoreTagProof.output_tag(Core.gcm_encrypt_raw(key, nonce, aad,
48 plaintext)) == Core.gcm_tag_bytes(Core.gcm_tag_output(
49 Core.aes256_expand(key), nonce, aad,
50 CoreTagProof.output_ciphertext(Core.gcm_encrypt_raw(key, nonce,
51 aad, plaintext)))) : List<&2, U32>}:
52 +output = Core.gcm_encrypt_raw(key, nonce, aad, plaintext)
53 +context = output_tag_context(output)
54 +expected_context = {TagContext{Core.aes256_expand(key), nonce, aad,
55 CoreTagProof.output_ciphertext(output)} : TagContext}
56 context_eq: {context == expected_context : TagContext} = {==}
57 Equal.trans(List<&2, U32>, CoreTagProof.output_tag(output),
58 tag_for_context(context), tag_for_context(expected_context),
59 output_tag_matches_context(output),
60 Equal.cong(TagContext, List<&2, U32>, tag_for_context,
61 context, expected_context, context_eq))
62
63def result_tag_bytes(fallback: List<&2, U32>,
64 result: Result<&2, &2, AES.Error, AES.Envelope>) -> List<&2, U32>:
65 match result:
66 case Fail{error}: fallback
67 case Done{envelope}: AES.tag_bytes(AES.envelope_tag(envelope))
68
69def valid_output_ciphertext_length(+key: AES.SecretKey,
70 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>) ->
71 {List.length(&2, U32,
72 AES.ciphertext(AES.envelope_from_gcm_checked(nonce,
73 AES.encrypt_valid_output(key, nonce, aad, plaintext)))) ==
74 List.length(&2, U32, plaintext) : Nat}:
75 ZipLengthProof.ctr_encrypt_ciphertext_length(
76 Core.aes256_expand(AES.secret_key_bytes(key)),
77 AES.raw_nonce_bytes(nonce), plaintext)
78
79def encrypt_checked_with_flags(+key: AES.SecretKey, +nonce: AES.Nonce,
80 +aad: List<&2, U32>, +plaintext: List<&2, U32>,
81 +aad_flag: Bool, +plaintext_flag: Bool,
82 aad_ok: {AES.aad_valid(aad) == aad_flag : Bool},
83 plaintext_ok: {AES.plaintext_valid(plaintext) == plaintext_flag : Bool},
84 +envelope: AES.Envelope,
85 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
86 Result<&2, &2, AES.Error, AES.Envelope>}) ->
87 {AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
88 plaintext_flag) == Done{envelope} :
89 Result<&2, &2, AES.Error, AES.Envelope>}:
90 changed_flags = Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
91 AES.encrypt(key, nonce, aad, plaintext),
92 AES.encrypt_checked(key, nonce, aad, plaintext,
93 AES.aad_valid(aad), AES.plaintext_valid(plaintext)),
94 AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
95 plaintext_flag), {==},
96 Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
97 AES.encrypt_checked(key, nonce, aad, plaintext,
98 AES.aad_valid(aad), AES.plaintext_valid(plaintext)),
99 AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
100 AES.plaintext_valid(plaintext)),
101 AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
102 plaintext_flag),
103 Equal.cong(Bool, Result<&2, &2, AES.Error, AES.Envelope>,
104 flag => AES.encrypt_checked(key, nonce, aad, plaintext,
105 flag, AES.plaintext_valid(plaintext)),
106 AES.aad_valid(aad), aad_flag, aad_ok),
107 Equal.cong(Bool, Result<&2, &2, AES.Error, AES.Envelope>,
108 flag => AES.encrypt_checked(key, nonce, aad, plaintext,
109 aad_flag, flag),
110 AES.plaintext_valid(plaintext), plaintext_flag,
111 plaintext_ok)))
112 Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
113 AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
114 plaintext_flag),
115 AES.encrypt(key, nonce, aad, plaintext),
116 Done{envelope},
117 Equal.sym(Result<&2, &2, AES.Error, AES.Envelope>,
118 AES.encrypt(key, nonce, aad, plaintext),
119 AES.encrypt_checked(key, nonce, aad, plaintext, aad_flag,
120 plaintext_flag), changed_flags),
121 encrypted)
122
123def successful_encrypt_aad_valid(+key: AES.SecretKey,
124 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>,
125 +aad_flag: Bool, +plaintext_flag: Bool,
126 aad_ok: {AES.aad_valid(aad) == aad_flag : Bool},
127 plaintext_ok: {AES.plaintext_valid(plaintext) == plaintext_flag : Bool},
128 +envelope: AES.Envelope,
129 encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
130 Result<&2, &2, AES.Error, AES.Envelope>}) ->
131 {aad_flag == True{} : Bool}:
132 match aad_flag:
133 case True{}: {==}
134 case False{}:
135 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext,
136 aad_flag, plaintext_flag, aad_ok, plaintext_ok, envelope,
137 encrypted)
138 Equal.trans(Bool, False{},
139 Result.is_done(&2, &2, AES.Error, AES.Envelope,
140 AES.encrypt_checked(key, nonce, aad, plaintext,
141 aad_flag, plaintext_flag)),
142 True{}, {==},
143 Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Bool,
144 result => Result.is_done(&2, &2, AES.Error, AES.Envelope,
145 result),
146 AES.encrypt_checked(key, nonce, aad, plaintext,
147 aad_flag, plaintext_flag), Done{envelope}, checked))
148
149def successful_encrypt_plaintext_valid(+key: AES.SecretKey,
150 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>,
151 +aad_flag: Bool, +plaintext_flag: Bool,
152 aad_ok: {AES.aad_valid(aad) == aad_flag : Bool},
153 plaintext_ok: {AES.plaintext_valid(plaintext) == plaintext_flag : Bool},
154 +envelope: AES.Envelope,
155 encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
156 Result<&2, &2, AES.Error, AES.Envelope>}) ->
157 {plaintext_flag == True{} : Bool}:
158 match aad_flag plaintext_flag:
159 case True{} True{}: {==}
160 case True{} False{}:
161 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext,
162 aad_flag, plaintext_flag, aad_ok, plaintext_ok, envelope,
163 encrypted)
164 Equal.trans(Bool, False{},
165 Result.is_done(&2, &2, AES.Error, AES.Envelope,
166 AES.encrypt_checked(key, nonce, aad, plaintext,
167 aad_flag, plaintext_flag)),
168 True{}, {==},
169 Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Bool,
170 result => Result.is_done(&2, &2, AES.Error, AES.Envelope,
171 result),
172 AES.encrypt_checked(key, nonce, aad, plaintext,
173 aad_flag, plaintext_flag), Done{envelope}, checked))
174 case False{} _:
175 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext,
176 aad_flag, plaintext_flag, aad_ok, plaintext_ok, envelope,
177 encrypted)
178 Empty.absurd({plaintext_flag == True{} : Bool},
179 ZipLengthProof.false_true(Equal.trans(Bool, False{},
180 Result.is_done(&2, &2, AES.Error, AES.Envelope,
181 AES.encrypt_checked(key, nonce, aad, plaintext,
182 aad_flag, plaintext_flag)),
183 True{}, {==},
184 Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Bool,
185 result => Result.is_done(&2, &2, AES.Error, AES.Envelope,
186 result),
187 AES.encrypt_checked(key, nonce, aad, plaintext,
188 aad_flag, plaintext_flag), Done{envelope}, checked))))
189
190def result_ciphertext_length(
191 result: Result<&2, &2, AES.Error, AES.Envelope>) -> Nat:
192 match result:
193 case Fail{error}: 0n
194 case Done{envelope}:
195 List.length(&2, U32, AES.ciphertext(envelope))
196
197def successful_encrypt_preserves_length(+key: AES.SecretKey,
198 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>,
199 +envelope: AES.Envelope,
200 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
201 Result<&2, &2, AES.Error, AES.Envelope>}) ->
202 {List.length(&2, U32, AES.ciphertext(envelope)) ==
203 List.length(&2, U32, plaintext) : Nat}:
204 +aad_flag = AES.aad_valid(aad)
205 +plaintext_flag = AES.plaintext_valid(plaintext)
206 aad_is_true = successful_encrypt_aad_valid(key, nonce, aad, plaintext,
207 aad_flag, plaintext_flag, {==}, {==}, envelope, encrypted)
208 plaintext_is_true = successful_encrypt_plaintext_valid(key, nonce,
209 aad, plaintext, aad_flag, plaintext_flag, {==}, {==},
210 envelope, encrypted)
211 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext,
212 True{}, True{}, aad_is_true, plaintext_is_true, envelope, encrypted)
213 output_length = valid_output_ciphertext_length(key, nonce, aad, plaintext)
214 Equal.trans(Nat,
215 List.length(&2, U32, AES.ciphertext(envelope)),
216 result_ciphertext_length(
217 AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{})),
218 List.length(&2, U32, plaintext),
219 Equal.sym(Nat,
220 result_ciphertext_length(
221 AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{})),
222 result_ciphertext_length(Done{envelope}),
223 Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, Nat,
224 result => result_ciphertext_length(result),
225 AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{}),
226 Done{envelope}, checked)),
227 output_length)
228
229def successful_encrypt_ciphertext_matches_gcm(+key: AES.SecretKey,
230 +nonce: AES.Nonce, +aad: List<&2, U32>,
231 +plaintext: List<&2, U32>, +envelope: AES.Envelope,
232 aad_valid: {AES.aad_valid(aad) == True{} : Bool},
233 plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
234 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
235 Result<&2, &2, AES.Error, AES.Envelope>}) ->
236 {AES.ciphertext(envelope) ==
237 CoreTagProof.output_ciphertext(AES.encrypt_valid_output(key, nonce,
238 aad, plaintext)) : List<&2, U32>}:
239 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext,
240 True{}, True{}, aad_valid, plaintext_valid, envelope, encrypted)
241 +output = AES.encrypt_valid_output(key, nonce, aad, plaintext)
242 constructed_matches = Equal.cong(
243 Result<&2, &2, AES.Error, AES.Envelope>, List<&2, U32>,
244 result => result_ciphertext(AES.ciphertext(envelope), result),
245 AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{}),
246 Done{envelope}, checked)
247 Equal.trans(List<&2, U32>,
248 AES.ciphertext(envelope),
249 AES.ciphertext(AES.envelope_from_gcm_checked(nonce, output)),
250 CoreTagProof.output_ciphertext(output),
251 Equal.sym(List<&2, U32>,
252 AES.ciphertext(AES.envelope_from_gcm_checked(nonce, output)),
253 AES.ciphertext(envelope), constructed_matches),
254 CoreTagProof.envelope_gcm_ciphertext(nonce, output))
255
256def successful_encrypt_tag_matches_gcm(+key: AES.SecretKey,
257 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>,
258 +envelope: AES.Envelope,
259 aad_ok: {AES.aad_valid(aad) == True{} : Bool},
260 plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool},
261 encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
262 Result<&2, &2, AES.Error, AES.Envelope>}) ->
263 {AES.tag_bytes(AES.envelope_tag(envelope)) ==
264 CoreTagProof.output_tag(AES.encrypt_valid_output(key, nonce, aad,
265 plaintext)) : List<&2, U32>}:
266 checked = encrypt_checked_with_flags(key, nonce, aad, plaintext,
267 True{}, True{}, aad_ok, plaintext_ok, envelope, encrypted)
268 +output = AES.encrypt_valid_output(key, nonce, aad, plaintext)
269 constructed_matches = Equal.cong(
270 Result<&2, &2, AES.Error, AES.Envelope>, List<&2, U32>,
271 result => result_tag_bytes([], result),
272 AES.encrypt_checked(key, nonce, aad, plaintext, True{}, True{}),
273 Done{envelope}, checked)
274 Equal.trans(List<&2, U32>, AES.tag_bytes(AES.envelope_tag(envelope)),
275 AES.tag_bytes(AES.envelope_tag(AES.envelope_from_gcm_checked(nonce,
276 output))), CoreTagProof.output_tag(output),
277 Equal.sym(List<&2, U32>,
278 AES.tag_bytes(AES.envelope_tag(AES.envelope_from_gcm_checked(
279 nonce, output))), AES.tag_bytes(AES.envelope_tag(envelope)),
280 constructed_matches), CoreTagProof.envelope_gcm_tag(nonce, output))
281
282def successful_encrypt_tag_canonical(+key: AES.SecretKey,
283 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>,
284 +envelope: AES.Envelope,
285 +aad_ok: {AES.aad_valid(aad) == True{} : Bool},
286 +plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool},
287 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
288 Result<&2, &2, AES.Error, AES.Envelope>}) ->
289 {AES.tag_bytes(AES.envelope_tag(envelope)) == Core.gcm_tag_bytes(
290 Core.gcm_tag_output(Core.aes256_expand(AES.secret_key_bytes(key)),
291 AES.raw_nonce_bytes(nonce), aad, AES.ciphertext(envelope))) :
292 List<&2, U32>}:
293 +output = AES.encrypt_valid_output(key, nonce, aad, plaintext)
294 tag_matches = successful_encrypt_tag_matches_gcm(key, nonce, aad,
295 plaintext, envelope, aad_ok, plaintext_ok, encrypted)
296 ciphertext_matches = successful_encrypt_ciphertext_matches_gcm(key,
297 nonce, aad, plaintext, envelope, aad_ok, plaintext_ok, encrypted)
298 raw_canonical = raw_output_tag_canonical(AES.secret_key_bytes(key),
299 AES.raw_nonce_bytes(nonce), aad, plaintext)
300 current_ciphertext = Equal.cong(List<&2, U32>, List<&2, U32>,
301 value => Core.gcm_tag_bytes(Core.gcm_tag_output(
302 Core.aes256_expand(AES.secret_key_bytes(key)),
303 AES.raw_nonce_bytes(nonce), aad, value)),
304 CoreTagProof.output_ciphertext(output), AES.ciphertext(envelope),
305 Equal.sym(List<&2, U32>, AES.ciphertext(envelope),
306 CoreTagProof.output_ciphertext(output), ciphertext_matches))
307 Equal.trans(List<&2, U32>, AES.tag_bytes(AES.envelope_tag(envelope)),
308 CoreTagProof.output_tag(output),
309 Core.gcm_tag_bytes(Core.gcm_tag_output(
310 Core.aes256_expand(AES.secret_key_bytes(key)),
311 AES.raw_nonce_bytes(nonce), aad, AES.ciphertext(envelope))),
312 tag_matches,
313 Equal.trans(List<&2, U32>, CoreTagProof.output_tag(output),
314 Core.gcm_tag_bytes(Core.gcm_tag_output(
315 Core.aes256_expand(AES.secret_key_bytes(key)),
316 AES.raw_nonce_bytes(nonce), aad,
317 CoreTagProof.output_ciphertext(output))),
318 Core.gcm_tag_bytes(Core.gcm_tag_output(
319 Core.aes256_expand(AES.secret_key_bytes(key)),
320 AES.raw_nonce_bytes(nonce), aad, AES.ciphertext(envelope))),
321 raw_canonical, current_ciphertext))
322
323def successful_encrypt_ciphertext_matches_ctr(+key: AES.SecretKey,
324 +nonce: AES.Nonce, +aad: List<&2, U32>,
325 +plaintext: List<&2, U32>, +envelope: AES.Envelope,
326 aad_valid: {AES.aad_valid(aad) == True{} : Bool},
327 plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
328 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
329 Result<&2, &2, AES.Error, AES.Envelope>}) ->
330 {AES.ciphertext(envelope) ==
331 Core.gcm_zip_xor(plaintext,
332 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
333 Core.aes256_expand(AES.secret_key_bytes(key)),
334 Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(nonce))))) :
335 List<&2, U32>}:
336 Equal.trans(List<&2, U32>,
337 AES.ciphertext(envelope),
338 CoreTagProof.output_ciphertext(AES.encrypt_valid_output(key, nonce,
339 aad, plaintext)),
340 Core.gcm_zip_xor(plaintext,
341 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
342 Core.aes256_expand(AES.secret_key_bytes(key)),
343 Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(nonce))))),
344 successful_encrypt_ciphertext_matches_gcm(key, nonce, aad,
345 plaintext, envelope, aad_valid, plaintext_valid, encrypted),
346 CoreTagProof.raw_encrypt_output_ciphertext(
347 AES.secret_key_bytes(key), AES.raw_nonce_bytes(nonce), aad,
348 plaintext))
349
350def successful_encrypt_ciphertext_valid(+key: AES.SecretKey,
351 +nonce: AES.Nonce, +aad: List<&2, U32>,
352 +plaintext: List<&2, U32>, +envelope: AES.Envelope,
353 aad_valid: {AES.aad_valid(aad) == True{} : Bool},
354 plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
355 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
356 Result<&2, &2, AES.Error, AES.Envelope>}) ->
357 {AES.plaintext_valid(AES.ciphertext(envelope)) == True{} : Bool}:
358 length_eq = successful_encrypt_preserves_length(key, nonce, aad,
359 plaintext, envelope, encrypted)
360 LengthLimitProof.plaintext_valid_same_length(
361 AES.ciphertext(envelope), plaintext,
362 AES.envelope_ciphertext_valid(envelope), plaintext_valid, length_eq)
363
364def successful_encrypt_ctr_decrypts(+key: AES.SecretKey,
365 +nonce: AES.Nonce, +aad: List<&2, U32>,
366 +plaintext: List<&2, U32>, +envelope: AES.Envelope,
367 aad_valid: {AES.aad_valid(aad) == True{} : Bool},
368 +plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
369 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
370 Result<&2, &2, AES.Error, AES.Envelope>}) ->
371 {Core.gcm_decrypt_raw(AES.secret_key_bytes(key),
372 AES.raw_nonce_bytes(nonce), AES.ciphertext(envelope)) ==
373 plaintext : List<&2, U32>}:
374 +words = Core.aes256_expand(AES.secret_key_bytes(key))
375 aes_bytes_valid = MaskedXorProof.bool_and_true_left(
376 AES.bytes_valid(plaintext),
377 AES.bytes_length_limit(plaintext, 4294967264, 15), plaintext_valid)
378 core_bytes_valid = Equal.trans(Bool,
379 Core.gcm_bytes_valid(plaintext), AES.bytes_valid(plaintext), True{},
380 Equal.sym(Bool, AES.bytes_valid(plaintext),
381 Core.gcm_bytes_valid(plaintext),
382 AES.core_bytes_valid_eq(plaintext)), aes_bytes_valid)
383 cipher = successful_encrypt_ciphertext_matches_ctr(key, nonce, aad,
384 plaintext, envelope, aad_valid, plaintext_valid, encrypted)
385 Equal.trans(List<&2, U32>,
386 Core.gcm_decrypt_raw(AES.secret_key_bytes(key),
387 AES.raw_nonce_bytes(nonce), AES.ciphertext(envelope)),
388 Core.gcm_decrypt_raw(AES.secret_key_bytes(key),
389 AES.raw_nonce_bytes(nonce),
390 Core.gcm_zip_xor(plaintext,
391 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
392 words, Core.gcm_inc32(Core.gcm_j0(
393 AES.raw_nonce_bytes(nonce)))))),
394 plaintext,
395 Equal.cong(List<&2, U32>, List<&2, U32>,
396 ciphertext => Core.gcm_decrypt_raw(AES.secret_key_bytes(key),
397 AES.raw_nonce_bytes(nonce), ciphertext),
398 AES.ciphertext(envelope),
399 Core.gcm_zip_xor(plaintext,
400 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
401 words, Core.gcm_inc32(Core.gcm_j0(
402 AES.raw_nonce_bytes(nonce))))), cipher),
403 MaskedXorProof.ctr_decrypt_ciphertext_roundtrip(words,
404 AES.raw_nonce_bytes(nonce), plaintext, core_bytes_valid))
405
406def result_nonce(fallback: AES.Nonce,
407 result: Result<&2, &2, AES.Error, AES.Envelope>) -> AES.Nonce:
408 match result:
409 case Fail{error}: fallback
410 case Done{envelope}: AES.envelope_nonce(envelope)
411
412def output_nonce(+nonce: AES.Nonce, +output: Core.GcmOutput) ->
413 {result_nonce(nonce, AES.encrypt_output_from_gcm(nonce, output)) ==
414 nonce : AES.Nonce}:
415 match output:
416 case Core.GcmOutput{+ciphertext, ciphertext_valid,
417 tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
418 tag_matches}:
419 {==}
420
421def valid_nonce(key: AES.SecretKey, +nonce: AES.Nonce,
422 aad: List<&2, U32>, plaintext: List<&2, U32>) ->
423 {result_nonce(nonce, AES.encrypt_valid(key, nonce, aad, plaintext)) ==
424 nonce : AES.Nonce}:
425 output_nonce(nonce,
426 AES.encrypt_valid_output(key, nonce, aad, plaintext))
427
428def checked_nonce(key: AES.SecretKey, +nonce: AES.Nonce,
429 +aad: List<&2, U32>, +plaintext: List<&2, U32>,
430 aad_ok: Bool, plaintext_ok: Bool) ->
431 {result_nonce(nonce, AES.encrypt_checked(key, nonce, aad, plaintext,
432 aad_ok, plaintext_ok)) == nonce : AES.Nonce}:
433 match aad_ok plaintext_ok:
434 case True{} True{}: valid_nonce(key, nonce, aad, plaintext)
435 case False{} _: {==}
436 case True{} False{}: {==}
437
438def encrypt_nonce(key: AES.SecretKey, +nonce: AES.Nonce,
439 +aad: List<&2, U32>, +plaintext: List<&2, U32>) ->
440 {result_nonce(nonce, AES.encrypt(key, nonce, aad, plaintext)) ==
441 nonce : AES.Nonce}:
442 checked_nonce(key, nonce, aad, plaintext,
443 AES.aad_valid(aad), AES.plaintext_valid(plaintext))
444
445def preserves_nonce(+key: AES.SecretKey, +nonce: AES.Nonce,
446 +aad: List<&2, U32>, +plaintext: List<&2, U32>,
447 +envelope: AES.Envelope,
448 encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
449 Result<&2, &2, AES.Error, AES.Envelope>}) ->
450 {AES.envelope_nonce(envelope) == nonce : AES.Nonce}:
451 Equal.trans(AES.Nonce,
452 result_nonce(nonce, Done{envelope}),
453 result_nonce(nonce, AES.encrypt(key, nonce, aad, plaintext)),
454 nonce,
455 Equal.sym(AES.Nonce,
456 result_nonce(nonce, AES.encrypt(key, nonce, aad, plaintext)),
457 result_nonce(nonce, Done{envelope}),
458 Equal.cong(Result<&2, &2, AES.Error, AES.Envelope>, AES.Nonce,
459 result => result_nonce(nonce, result),
460 AES.encrypt(key, nonce, aad, plaintext), Done{envelope},
461 encrypted)),
462 encrypt_nonce(key, nonce, aad, plaintext))
463
464def successful_encrypt_envelope_tag_canonical(+key: AES.SecretKey,
465 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>,
466 +envelope: AES.Envelope,
467 aad_ok: {AES.aad_valid(aad) == True{} : Bool},
468 plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool},
469 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
470 Result<&2, &2, AES.Error, AES.Envelope>}) ->
471 {AES.tag_bytes(AES.envelope_tag(envelope)) == Core.gcm_tag_bytes(
472 Core.gcm_tag_output(Core.aes256_expand(AES.secret_key_bytes(key)),
473 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), aad,
474 AES.ciphertext(envelope))) : List<&2, U32>}:
475 canonical = successful_encrypt_tag_canonical(key, nonce, aad, plaintext,
476 envelope, aad_ok, plaintext_ok, encrypted)
477 nonce_matches = Equal.cong(AES.Nonce, List<&2, U32>,
478 AES.raw_nonce_bytes, AES.envelope_nonce(envelope), nonce,
479 preserves_nonce(key, nonce, aad, plaintext, envelope, encrypted))
480 nonce_rewrite = Equal.cong(List<&2, U32>, List<&2, U32>,
481 value => Core.gcm_tag_bytes(Core.gcm_tag_output(
482 Core.aes256_expand(AES.secret_key_bytes(key)), value, aad,
483 AES.ciphertext(envelope))), AES.raw_nonce_bytes(nonce),
484 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)),
485 Equal.sym(List<&2, U32>,
486 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)),
487 AES.raw_nonce_bytes(nonce), nonce_matches))
488 Equal.trans(List<&2, U32>, AES.tag_bytes(AES.envelope_tag(envelope)),
489 Core.gcm_tag_bytes(Core.gcm_tag_output(
490 Core.aes256_expand(AES.secret_key_bytes(key)),
491 AES.raw_nonce_bytes(nonce), aad, AES.ciphertext(envelope))),
492 Core.gcm_tag_bytes(Core.gcm_tag_output(
493 Core.aes256_expand(AES.secret_key_bytes(key)),
494 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), aad,
495 AES.ciphertext(envelope))), canonical, nonce_rewrite)
496
497def decrypt_auth_tag_canonical(+words: List<&2, U32>,
498 +nonce: List<&2, U32>, +aad: List<&2, U32>,
499 +ciphertext: List<&2, U32>, +envelope: AES.Envelope, +tag: AES.Tag,
500 canonical: {AES.tag_bytes(tag) == Core.gcm_tag_bytes(
501 Core.gcm_tag_output(words, nonce, aad, ciphertext)) : List<&2, U32>}) ->
502 {AES.decrypt_authenticated_tag(words, nonce, aad, ciphertext, envelope,
503 tag) == AES.decrypt_auth_result(words, envelope, True{}) :
504 Result<&2, &2, AES.Error, List<&2, U32>>}:
505 match tag:
506 case AES.Tag{bytes, size, valid}:
507 Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>,
508 ok => AES.decrypt_auth_result(words, envelope, ok),
509 AES.bytes_equal_full_scan(bytes, Core.gcm_tag_bytes(
510 Core.gcm_tag_output(words, nonce, aad, ciphertext))),
511 True{}, TagCompareProof.equal_of_equal(bytes,
512 Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce,
513 aad, ciphertext)), canonical))
514
515def successful_encrypt_decrypt_authenticated(+key: AES.SecretKey,
516 +nonce: AES.Nonce, +aad: List<&2, U32>, +plaintext: List<&2, U32>,
517 +envelope: AES.Envelope,
518 +aad_ok: {AES.aad_valid(aad) == True{} : Bool},
519 +plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool},
520 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
521 Result<&2, &2, AES.Error, AES.Envelope>}) ->
522 {AES.decrypt_authenticated(key, aad, envelope) == Done{plaintext} :
523 Result<&2, &2, AES.Error, List<&2, U32>>}:
524 match key envelope:
525 case AES.SecretKey{+key_bytes, _, _}
526 AES.Envelope{envelope_nonce, ciphertext, tag, _}:
527 +words = Core.aes256_expand(key_bytes)
528 +nonce_bytes = AES.raw_nonce_bytes(envelope_nonce)
529 canonical = successful_encrypt_envelope_tag_canonical(key,
530 nonce, aad, plaintext, envelope, aad_ok, plaintext_ok,
531 encrypted)
532 authenticated = decrypt_auth_tag_canonical(words, nonce_bytes,
533 aad, ciphertext, envelope, tag, canonical)
534 nonce_matches = Equal.cong(AES.Nonce, List<&2, U32>,
535 AES.raw_nonce_bytes, envelope_nonce, nonce,
536 preserves_nonce(key, nonce, aad, plaintext, envelope,
537 encrypted))
538 ctr_roundtrip = successful_encrypt_ctr_decrypts(key, nonce, aad,
539 plaintext, envelope, aad_ok, plaintext_ok, encrypted)
540 expanded_nonce = Equal.cong(List<&2, U32>, List<&2, U32>,
541 value => Core.gcm_decrypt_expanded(words, value, ciphertext),
542 nonce_bytes, AES.raw_nonce_bytes(nonce), nonce_matches)
543 expanded_to_raw = Equal.trans(List<&2, U32>,
544 Core.gcm_decrypt_expanded(words, nonce_bytes, ciphertext),
545 Core.gcm_decrypt_expanded(words, AES.raw_nonce_bytes(nonce),
546 ciphertext),
547 Core.gcm_decrypt_raw(AES.secret_key_bytes(key),
548 AES.raw_nonce_bytes(nonce), ciphertext),
549 expanded_nonce, {==})
550 expanded_roundtrip = Equal.trans(List<&2, U32>,
551 Core.gcm_decrypt_expanded(words, nonce_bytes, ciphertext),
552 Core.gcm_decrypt_raw(AES.secret_key_bytes(key),
553 AES.raw_nonce_bytes(nonce), ciphertext), plaintext,
554 expanded_to_raw, ctr_roundtrip)
555 payload = Equal.cong(List<&2, U32>,
556 Result<&2, &2, AES.Error, List<&2, U32>>,
557 value => Done{value},
558 Core.gcm_decrypt_expanded(words, nonce_bytes, ciphertext),
559 plaintext, expanded_roundtrip)
560 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
561 AES.decrypt_authenticated(key, aad, envelope),
562 AES.decrypt_auth_result(words, envelope, True{}),
563 Done{plaintext}, authenticated, payload)
564
565def successful_encrypt_decrypt_roundtrip(+key: AES.SecretKey,
566 +nonce: AES.Nonce, +aad: List<&2, U32>,
567 +plaintext: List<&2, U32>, +envelope: AES.Envelope,
568 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
569 Result<&2, &2, AES.Error, AES.Envelope>}) ->
570 {AES.decrypt(key, aad, envelope) == Done{plaintext} :
571 Result<&2, &2, AES.Error, List<&2, U32>>}:
572 +aad_ok = successful_encrypt_aad_valid(key, nonce, aad, plaintext,
573 AES.aad_valid(aad), AES.plaintext_valid(plaintext), {==}, {==},
574 envelope, encrypted)
575 +plaintext_ok = successful_encrypt_plaintext_valid(key, nonce, aad,
576 plaintext, AES.aad_valid(aad), AES.plaintext_valid(plaintext),
577 {==}, {==}, envelope, encrypted)
578 ciphertext_ok = successful_encrypt_ciphertext_valid(key, nonce, aad,
579 plaintext, envelope, aad_ok, plaintext_ok, encrypted)
580 authenticated = successful_encrypt_decrypt_authenticated(key, nonce,
581 aad, plaintext, envelope, aad_ok, plaintext_ok, encrypted)
582 aad_checked = Equal.cong(Bool,
583 Result<&2, &2, AES.Error, List<&2, U32>>,
584 flag => AES.decrypt_checked(key, aad, envelope, flag,
585 AES.plaintext_valid(AES.ciphertext(envelope))),
586 AES.aad_valid(aad), True{}, aad_ok)
587 ciphertext_checked = Equal.cong(Bool,
588 Result<&2, &2, AES.Error, List<&2, U32>>,
589 flag => AES.decrypt_checked(key, aad, envelope, True{}, flag),
590 AES.plaintext_valid(AES.ciphertext(envelope)), True{}, ciphertext_ok)
591 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
592 AES.decrypt(key, aad, envelope),
593 AES.decrypt_checked(key, aad, envelope, True{}, True{}),
594 Done{plaintext},
595 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
596 AES.decrypt(key, aad, envelope),
597 AES.decrypt_checked(key, aad, envelope,
598 AES.aad_valid(aad),
599 AES.plaintext_valid(AES.ciphertext(envelope))),
600 AES.decrypt_checked(key, aad, envelope, True{}, True{}),
601 {==},
602 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
603 AES.decrypt_checked(key, aad, envelope,
604 AES.aad_valid(aad),
605 AES.plaintext_valid(AES.ciphertext(envelope))),
606 AES.decrypt_checked(key, aad, envelope, True{},
607 AES.plaintext_valid(AES.ciphertext(envelope))),
608 AES.decrypt_checked(key, aad, envelope, True{}, True{}),
609 aad_checked, ciphertext_checked)),
610 authenticated)
611
612def output_is_done(+nonce: AES.Nonce, +output: Core.GcmOutput) ->
613 {Result.is_done(&2, &2, AES.Error, AES.Envelope,
614 AES.encrypt_output_from_gcm(nonce, output)) == True{} : Bool}:
615 {==}
616
617def valid_is_done(key: AES.SecretKey, +nonce: AES.Nonce,
618 aad: List<&2, U32>, plaintext: List<&2, U32>) ->
619 {Result.is_done(&2, &2, AES.Error, AES.Envelope,
620 AES.encrypt_valid(key, nonce, aad, plaintext)) == True{} : Bool}:
621 output_is_done(nonce,
622 AES.encrypt_valid_output(key, nonce, aad, plaintext))
623
624def valid_input_is_done(+key: AES.SecretKey, +nonce: AES.Nonce,
625 +aad: List<&2, U32>, +plaintext: List<&2, U32>,
626 aad_ok: {AES.aad_valid(aad) == True{} : Bool},
627 plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}) ->
628 {Result.is_done(&2, &2, AES.Error, AES.Envelope,
629 AES.encrypt(key, nonce, aad, plaintext)) == True{} : Bool}:
630 Equal.trans(Bool,
631 Result.is_done(&2, &2, AES.Error, AES.Envelope,
632 AES.encrypt(key, nonce, aad, plaintext)),
633 Result.is_done(&2, &2, AES.Error, AES.Envelope,
634 AES.encrypt_checked(key, nonce, aad, plaintext,
635 True{}, AES.plaintext_valid(plaintext))),
636 True{},
637 Equal.cong(Bool, Bool,
638 b => Result.is_done(&2, &2, AES.Error, AES.Envelope,
639 AES.encrypt_checked(key, nonce, aad, plaintext,
640 b, AES.plaintext_valid(plaintext))),
641 AES.aad_valid(aad), True{}, aad_ok),
642 Equal.trans(Bool,
643 Result.is_done(&2, &2, AES.Error, AES.Envelope,
644 AES.encrypt_checked(key, nonce, aad, plaintext,
645 True{}, AES.plaintext_valid(plaintext))),
646 Result.is_done(&2, &2, AES.Error, AES.Envelope,
647 AES.encrypt_valid(key, nonce, aad, plaintext)),
648 True{},
649 Equal.cong(Bool, Bool,
650 b => Result.is_done(&2, &2, AES.Error, AES.Envelope,
651 AES.encrypt_checked(key, nonce, aad, plaintext,
652 True{}, b)),
653 AES.plaintext_valid(plaintext), True{}, plaintext_ok),
654 valid_is_done(key, nonce, aad, plaintext)))