~/bend-docscommunity

proof/AES_NistInputProof.bend open laws/TODOs

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

3 imports
import Base
import ../LAWS.bend as L
import ../libs/AES256GCM.bend as AES

Definitions

def encrypt_inputs source · line 7 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+fixture_aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+fixture_plaintext:List<&2, U32> -> @+expected:List<&2, U32> -> @aad_matches:{aad == fixture_aad : List<&2, U32>} -> @plaintext_matches:{plaintext == fixture_plaintext : List<&2, U32>} -> @computed:{0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, fixture_aad, fixture_plaintext)) == expected : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext)) == expected : List<&2, U32>}

Transport fixture aliases before entering the encryption or decryption code. Equal fixtures must not force a fresh evaluation of the entire cipher.

def decrypt_inputs source · line 28 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+fixture_key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+aad:List<&2, U32> -> @+fixture_aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+fixture_envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+expected:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>> -> @key_matches:{key == fixture_key : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey} -> @aad_matches:{aad == fixture_aad : List<&2, U32>} -> @envelope_matches:{envelope == fixture_envelope : 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope} -> @computed:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(fixture_key, fixture_aad, fixture_envelope) == expected : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(key, aad, envelope) == expected : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}