def successful_encrypt_decrypt_authenticated

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

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

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)