~/bend-docscommunity

proof/AES_TamperProof.bend checks

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

5 imports
import Base
import ../libs/AES256GCM.bend as AES
import ../libs/AES256GCMCore.bend as Core
import ./AES_EncryptProof.bend as Encrypt
import ./AES_TagRejectProof.bend as Reject

Definitions

def canonical_for_equal_envelope source · line 7 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+tampered_nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+ciphertext:List<&2, U32> -> @+tampered_ciphertext:List<&2, U32> -> @+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>} -> @same_nonce:{tampered_nonce == nonce : List<&2, U32>} -> @same_ciphertext:{tampered_ciphertext == ciphertext : List<&2, U32>} -> {original == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(words, tampered_nonce, aad, tampered_ciphertext)) : List<&2, U32>}

def reject_authenticated source · line 38 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+tampered:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @canonical:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(envelope)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key)), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope)), aad, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope))) : List<&2, U32>} -> @same_nonce:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(tampered)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope)) : List<&2, U32>} -> @same_ciphertext:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(tampered) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope) : List<&2, U32>} -> @changed_tag:(@_:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(tampered)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(envelope)) : List<&2, U32>} -> Empty) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_authenticated(key, aad, tampered) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def rejects_changed_tag source · line 69 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+tampered:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+encrypted:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext) == Done{envelope} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope>} -> @same_nonce:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(tampered)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope)) : List<&2, U32>} -> @+same_ciphertext:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(tampered) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope) : List<&2, U32>} -> @changed_tag:(@_:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(tampered)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_tag(envelope)) : List<&2, U32>} -> Empty) -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(key, aad, tampered) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}