def reject_authenticated

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

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_TagRejectProof.bend as Reject

38def reject_authenticated(+key: AES.SecretKey, +aad: List<&2, U32>,
39    +envelope: AES.Envelope, +tampered: AES.Envelope,
40    canonical: {AES.tag_bytes(AES.envelope_tag(envelope)) ==
41        Core.gcm_tag_bytes(Core.gcm_tag_output(
42            Core.aes256_expand(AES.secret_key_bytes(key)),
43            AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), aad,
44            AES.ciphertext(envelope))) : List<&2, U32>},
45    same_nonce: {AES.raw_nonce_bytes(AES.envelope_nonce(tampered)) ==
46        AES.raw_nonce_bytes(AES.envelope_nonce(envelope)) : List<&2, U32>},
47    same_ciphertext: {AES.ciphertext(tampered) == AES.ciphertext(envelope) :
48        List<&2, U32>},
49    changed_tag: {AES.tag_bytes(AES.envelope_tag(tampered)) !=
50        AES.tag_bytes(AES.envelope_tag(envelope)) : List<&2, U32>}) ->
51    {AES.decrypt_authenticated(key, aad, tampered) ==
52     Fail{AES.AuthenticationFailed{}} :
53        Result<&2, &2, AES.Error, List<&2, U32>>}:
54    match key envelope tampered:
55        case AES.SecretKey{+key_bytes, _, _}
56             AES.Envelope{nonce, ciphertext, tag, _}
57             AES.Envelope{tampered_nonce, tampered_ciphertext, tampered_tag, _}:
58            +words = Core.aes256_expand(key_bytes)
59            +tampered_nonce_bytes = AES.raw_nonce_bytes(tampered_nonce)
60            +original = AES.tag_bytes(tag)
61            canonical_tampered = canonical_for_equal_envelope(words,
62                AES.raw_nonce_bytes(nonce), tampered_nonce_bytes, aad,
63                ciphertext, tampered_ciphertext, original, canonical,
64                same_nonce, same_ciphertext)
65            Reject.rejects_tag(words, tampered_nonce_bytes, aad,
66                tampered_ciphertext, tampered, tampered_tag, original,
67                canonical_tampered, changed_tag)