~/bend-docscommunity

proof/AES_TagRejectProof.bend checks

raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/AES_TagRejectProof.bend as AES_TagRejectProof

4 imports
import Base
import ../libs/AES256GCM.bend as AES
import ../libs/AES256GCMCore.bend as Core
import ./AES_TagCompareProof.bend as Compare

Definitions

def rejects_comparison source · line 6 · raw

@+words:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+supplied:List<&2, U32> -> @+expected:List<&2, U32> -> @changed:(@_:{supplied == expected : List<&2, U32>} -> Empty) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_auth_result(words, envelope, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.bytes_equal_full_scan(supplied, expected)) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def rejects_tag source · line 20 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+tag:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Tag -> @+original:List<&2, U32> -> @canonical:{original == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(words, nonce, aad, ciphertext)) : List<&2, U32>} -> @changed:(@_:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(tag) == original : List<&2, U32>} -> Empty) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_authenticated_tag(words, nonce, aad, ciphertext, envelope, tag) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}