~/bend-docscommunity

proof/AES_NistObservationProof.bend open laws/TODOs

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

4 imports
import Base
import ../LAWS.bend as L
import ../libs/AES256GCM.bend as AES
import ../libs/AES256GCMCore.bend as Core

Definitions

def ciphertext source · line 6 · raw

@output:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmCiphertext -> List<&2, U32>

def schedule_input_matches source · line 10 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+bytes:List<&2, U32> -> @+words:List<&2, U32> -> @input_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key) == bytes : List<&2, U32>} -> @computed:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(bytes) == words : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key)) == words : List<&2, U32>}

def stream_parameters source · line 18 · raw

@+size:Nat -> @+words:List<&2, U32> -> @+start:List<&2, U32> -> @+known_size:Nat -> @+known_start:List<&2, U32> -> @+stream:List<&2, U32> -> @count:{size == known_size : Nat} -> @counter:{start == known_start : List<&2, U32>} -> @computed:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact.go(known_size, words, known_start, []) == stream : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(size, words, start) == stream : List<&2, U32>}

def ciphertext_shape source · line 31 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+input:List<&2, U32> -> {ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_encrypt(words, nonce, input)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_expanded(words, nonce, input) : List<&2, U32>}

def xor_from_stream source · line 35 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+input:List<&2, U32> -> @+stream:List<&2, U32> -> @computed:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(List.length(&2, U32, input), words, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(nonce))) == stream : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_expanded(words, nonce, input) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_zip_xor(input, stream) : List<&2, U32>}

def finish_cipher source · line 41 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+input:List<&2, U32> -> @+stream:List<&2, U32> -> @+output:List<&2, U32> -> @computed:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_stream_exact(List.length(&2, U32, input), words, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_inc32(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(nonce))) == stream : List<&2, U32>} -> @xor_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_zip_xor(input, stream) == output : List<&2, U32>} -> {ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_encrypt(words, nonce, input)) == output : List<&2, U32>}

def parts source · line 50 · raw

@+words:List<&2, U32> -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+bytes:List<&2, U32> -> List<&2, U32>

def expanded source · line 57 · raw

@+words:List<&2, U32> -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> List<&2, U32>

def from_ciphertext source · line 62 · raw

@+words:List<&2, U32> -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+output:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.GcmCiphertext -> {0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_output_from_gcm(nonce, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_output_from_ciphertext(words, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(nonce), aad, output))) == parts(words, nonce, aad, ciphertext(output)) : List<&2, U32>}

def valid_encrypt source · line 70 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> {0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt_valid(key, nonce, aad, plaintext)) == expanded(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key)), nonce, aad, plaintext) : List<&2, U32>}

def checked_encrypt source · line 78 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> {0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext)) == expanded(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key)), nonce, aad, plaintext) : List<&2, U32>}

def finish_encrypt source · line 105 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+nonce:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Nonce -> @+aad:List<&2, U32> -> @+plaintext:List<&2, U32> -> @+words:List<&2, U32> -> @+bytes:List<&2, U32> -> @+tag:List<&2, U32> -> @aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @plaintext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(plaintext) == True{} : Bool} -> @key_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key)) == words : List<&2, U32>} -> @ciphertext_matches:{ciphertext(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_ctr_encrypt(words, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(nonce), plaintext)) == bytes : List<&2, U32>} -> @tag_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(words, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(nonce), aad, bytes)) == tag : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/LAWS.aes256gcm_nist_encrypt_observation(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.encrypt(key, nonce, aad, plaintext)) == List.append(&2, U32, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)) : List<&2, U32>}

def decrypt_expanded source · line 138 · raw

@+words:List<&2, U32> -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>

def decrypt_key_shape source · line 144 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_authenticated(key, aad, envelope) == decrypt_expanded(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key)), aad, envelope) : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def payload_shape source · line 150 · raw

@+words:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_auth_result(words, envelope, True{}) == Done{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_expanded(words, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope)), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope))} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def payload_parameters source · line 156 · raw

@+words:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+nonce:List<&2, U32> -> @+bytes:List<&2, U32> -> @+plaintext:List<&2, U32> -> @nonce_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope)) == nonce : List<&2, U32>} -> @ciphertext_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope) == bytes : List<&2, U32>} -> @computed:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_decrypt_expanded(words, nonce, bytes) == plaintext : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_auth_result(words, envelope, True{}) == Done{plaintext} : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def envelope_tag_computed source · line 177 · raw

@+words:List<&2, U32> -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> List<&2, U32>

def tag_parameters source · line 180 · raw

@+words:List<&2, U32> -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+nonce:List<&2, U32> -> @+bytes:List<&2, U32> -> @+tag:List<&2, U32> -> @nonce_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.raw_nonce_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.envelope_nonce(envelope)) == nonce : List<&2, U32>} -> @ciphertext_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope) == bytes : List<&2, U32>} -> @computed:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(words, nonce, aad, bytes)) == tag : List<&2, U32>} -> {envelope_tag_computed(words, aad, envelope) == tag : List<&2, U32>}

def auth_for_tag source · line 197 · raw

@+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @tag:List<&2, U32> -> Bool

def decrypt_auth_shape source · line 200 · raw

@+words:List<&2, U32> -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> {decrypt_expanded(words, aad, envelope) == 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_auth_result(words, envelope, auth_for_tag(envelope, envelope_tag_computed(words, aad, envelope))) : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def finish_auth source · line 208 · raw

@+words:List<&2, U32> -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+tag:List<&2, U32> -> @+flag:Bool -> @+result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>> -> @tag_matches:{envelope_tag_computed(words, aad, envelope) == tag : List<&2, U32>} -> @compare_matches:{auth_for_tag(envelope, tag) == flag : Bool} -> @branch_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt_auth_result(words, envelope, flag) == result : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>} -> {decrypt_expanded(words, aad, envelope) == result : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}

def finish_decrypt source · line 230 · raw

@+key:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.SecretKey -> @+aad:List<&2, U32> -> @+envelope:0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Envelope -> @+words:List<&2, U32> -> @+result:Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>> -> @aad_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.aad_valid(aad) == True{} : Bool} -> @ciphertext_ok:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.plaintext_valid(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.ciphertext(envelope)) == True{} : Bool} -> @key_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_expand(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.secret_key_bytes(key)) == words : List<&2, U32>} -> @expanded_matches:{decrypt_expanded(words, aad, envelope) == result : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.decrypt(key, aad, envelope) == result : Result<&2, &2, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCM.Error, List<&2, U32>>}