def successful_encrypt_decrypt_roundtrip

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

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

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)