def rejects_tag

qasim-bend-kit@0.1.0.2 · proof/AES_TagRejectProof.bend:20

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

20def rejects_tag(+words: List<&2, U32>, +nonce: List<&2, U32>,
21    +aad: List<&2, U32>, +ciphertext: List<&2, U32>,
22    +envelope: AES.Envelope, +tag: AES.Tag,
23    +original: List<&2, U32>,
24    canonical: {original == Core.gcm_tag_bytes(Core.gcm_tag_output(
25        words, nonce, aad, ciphertext)) : List<&2, U32>},
26    changed: {AES.tag_bytes(tag) != original : List<&2, U32>}) ->
27    {AES.decrypt_authenticated_tag(words, nonce, aad, ciphertext, envelope,
28        tag) == Fail{AES.AuthenticationFailed{}} :
29        Result<&2, &2, AES.Error, List<&2, U32>>}:
30    match tag:
31        case AES.Tag{bytes, size, valid}:
32            rejects_comparison(words, envelope, bytes,
33                Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad,
34                    ciphertext)),
35                same => changed(Equal.trans(List<&2, U32>, bytes,
36                    Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce,
37                        aad, ciphertext)), original, same,
38                    Equal.sym(List<&2, U32>, original,
39                        Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce,
40                            aad, ciphertext)), canonical))))