def rejects_changed_tag

qasim-bend-kit@0.1.0.2 · proof/AES_TamperProof.bend:69

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

69def rejects_changed_tag(+key: AES.SecretKey, +nonce: AES.Nonce,
70    +aad: List<&2, U32>, +plaintext: List<&2, U32>,
71    +envelope: AES.Envelope, +tampered: AES.Envelope,
72    +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
73        Result<&2, &2, AES.Error, AES.Envelope>},
74    same_nonce: {AES.raw_nonce_bytes(AES.envelope_nonce(tampered)) ==
75        AES.raw_nonce_bytes(AES.envelope_nonce(envelope)) : List<&2, U32>},
76    +same_ciphertext: {AES.ciphertext(tampered) == AES.ciphertext(envelope) :
77        List<&2, U32>},
78    changed_tag: {AES.tag_bytes(AES.envelope_tag(tampered)) !=
79        AES.tag_bytes(AES.envelope_tag(envelope)) : List<&2, U32>}) ->
80    {AES.decrypt(key, aad, tampered) == Fail{AES.AuthenticationFailed{}} :
81        Result<&2, &2, AES.Error, List<&2, U32>>}:
82    +aad_ok = Encrypt.successful_encrypt_aad_valid(key, nonce, aad,
83        plaintext, AES.aad_valid(aad), AES.plaintext_valid(plaintext),
84        {==}, {==}, envelope, encrypted)
85    +plaintext_ok = Encrypt.successful_encrypt_plaintext_valid(key, nonce,
86        aad, plaintext, AES.aad_valid(aad), AES.plaintext_valid(plaintext),
87        {==}, {==}, envelope, encrypted)
88    ciphertext_ok = Encrypt.successful_encrypt_ciphertext_valid(key, nonce,
89        aad, plaintext, envelope, aad_ok, plaintext_ok, encrypted)
90    tampered_ciphertext_ok = Equal.trans(Bool,
91        AES.plaintext_valid(AES.ciphertext(tampered)),
92        AES.plaintext_valid(AES.ciphertext(envelope)), True{},
93        Equal.cong(List<&2, U32>, Bool, value => AES.plaintext_valid(value),
94            AES.ciphertext(tampered), AES.ciphertext(envelope),
95            same_ciphertext), ciphertext_ok)
96    canonical = Encrypt.successful_encrypt_envelope_tag_canonical(key,
97        nonce, aad, plaintext, envelope, aad_ok, plaintext_ok, encrypted)
98    rejected = reject_authenticated(key, aad, envelope, tampered,
99        canonical, same_nonce, same_ciphertext, changed_tag)
100    aad_checked = Equal.cong(Bool,
101        Result<&2, &2, AES.Error, List<&2, U32>>,
102        flag => AES.decrypt_checked(key, aad, tampered, flag,
103            AES.plaintext_valid(AES.ciphertext(tampered))),
104        AES.aad_valid(aad), True{}, aad_ok)
105    ciphertext_checked = Equal.cong(Bool,
106        Result<&2, &2, AES.Error, List<&2, U32>>,
107        flag => AES.decrypt_checked(key, aad, tampered, True{}, flag),
108        AES.plaintext_valid(AES.ciphertext(tampered)), True{},
109        tampered_ciphertext_ok)
110    Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
111        AES.decrypt(key, aad, tampered),
112        AES.decrypt_checked(key, aad, tampered, True{}, True{}),
113        Fail{AES.AuthenticationFailed{}},
114        Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
115            AES.decrypt(key, aad, tampered),
116            AES.decrypt_checked(key, aad, tampered, True{},
117                AES.plaintext_valid(AES.ciphertext(tampered))),
118            AES.decrypt_checked(key, aad, tampered, True{}, True{}),
119            aad_checked, ciphertext_checked), rejected)