def successful_encrypt_ctr_decrypts

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

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_MaskedXorProof.bend as MaskedXorProof

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