def successful_encrypt_tag_canonical

qasim-bend-kit@0.1.0.2 · proof/AES_EncryptProof.bend:282

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
import qasim-bend-kit@0.1.0.2/proof/AES_CoreTagProof.bend as CoreTagProof

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))