proof/AES_NistTamperVectorProof.bend timeout
raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/AES_NistTamperVectorProof.bend as AES_NistTamperVectorProof
7 imports
import Base import ../LAWS.bend as L import ../libs/AES256GCM.bend as AES import ../libs/AES256GCMCore.bend as Core import ./AES_NistKeyScheduleProof.bend as Key import ./AES_NistObservationProof.bend as Obs import ./AES_NistVectorProof.bend as V
Definitions
def zero_words source · line 9 · raw
List<&2, U32>
def zero_key source · line 12 · raw
0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey
def checkpoint_zero_key source · line 15 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(zero_key)) == zero_words : List<&2, U32>}
def changed_aad_aad source · line 19 · raw
List<&2, U32>
def changed_aad_computed_tag source · line 22 · raw
List<&2, U32>
def changed_aad_envelope source · line 25 · raw
0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope
def checkpoint_changed_aad_tag source · line 29 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.envelope_tag_computed(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, changed_aad_aad, changed_aad_envelope) == changed_aad_computed_tag : List<&2, U32>}
def checkpoint_changed_aad_rejected source · line 33 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, changed_aad_aad, changed_aad_envelope) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def rejects_changed_aad source · line 39 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, changed_aad_aad, changed_aad_envelope) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def changed_key_aad source · line 44 · raw
List<&2, U32>
def changed_key_computed_tag source · line 47 · raw
List<&2, U32>
def changed_key_envelope source · line 50 · raw
0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope
def checkpoint_changed_key_tag source · line 54 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.envelope_tag_computed(zero_words, changed_key_aad, changed_key_envelope) == changed_key_computed_tag : List<&2, U32>}
def checkpoint_changed_key_rejected source · line 58 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.decrypt_expanded(zero_words, changed_key_aad, changed_key_envelope) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def rejects_changed_key source · line 64 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(zero_key, changed_key_aad, changed_key_envelope) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def changed_nonce_aad source · line 69 · raw
List<&2, U32>
def changed_nonce_computed_tag source · line 72 · raw
List<&2, U32>
def changed_nonce_envelope source · line 75 · raw
0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope
def checkpoint_changed_nonce_tag source · line 79 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.envelope_tag_computed(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, changed_nonce_aad, changed_nonce_envelope) == changed_nonce_computed_tag : List<&2, U32>}
def checkpoint_changed_nonce_rejected source · line 83 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, changed_nonce_aad, changed_nonce_envelope) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def rejects_changed_nonce source · line 89 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, changed_nonce_aad, changed_nonce_envelope) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def changed_ciphertext_aad source · line 94 · raw
List<&2, U32>
def changed_ciphertext_computed_tag source · line 97 · raw
List<&2, U32>
def changed_ciphertext_envelope source · line 100 · raw
0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope
def checkpoint_changed_ciphertext_tag source · line 104 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.envelope_tag_computed(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, changed_ciphertext_aad, changed_ciphertext_envelope) == changed_ciphertext_computed_tag : List<&2, U32>}
def checkpoint_changed_ciphertext_rejected source · line 108 · raw
{0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistObservationProof.decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, changed_ciphertext_aad, changed_ciphertext_envelope) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}
def rejects_changed_ciphertext source · line 114 · raw
{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_key, changed_ciphertext_aad, changed_ciphertext_envelope) == Fail{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.AuthenticationFailed{}} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}