proof/AES_NistTagProof.bend checks

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

7 imports

import Base
import ../libs/AES256GCMCore.bend as Core
import ./AES_NistKeyScheduleProof.bend as Key
import ./AES_NistBlockProof.bend as J0
import ./AES_NistBlockComposeProof.bend as J0Proof
import ./AES_NistHashBlockProof.bend as Hash
import ./AES_NistHashBlockComposeProof.bend as HashProof

Definitions

def zero source · line 9 · raw

List<&2, U32>

def auth_from_hash source · line 12 · raw

@+h:List<&2, U32> -> @+aad:List<&2, U32> -> @+bytes:List<&2, U32> -> List<&2, U32>

def tag_from_parts source · line 15 · raw

@auth:List<&2, U32> -> @mask:List<&2, U32> -> List<&2, U32>

def tag_shape source · line 18 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+bytes:List<&2, U32> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(words, nonce, aad, bytes)) == tag_from_parts(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.ghash_auth_expanded(words, aad, bytes), 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(words, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(nonce))) : List<&2, U32>}

def auth_from_checked_hash source · line 25 · raw

@+words:List<&2, U32> -> @+h:List<&2, U32> -> @+aad:List<&2, U32> -> @+bytes:List<&2, U32> -> @+auth:List<&2, U32> -> @hash_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(words, [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) == h : List<&2, U32>} -> @computed:{auth_from_hash(h, aad, bytes) == auth : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.ghash_auth_expanded(words, aad, bytes) == auth : List<&2, U32>}

def aes_block_input_matches source · line 37 · raw

@+words:List<&2, U32> -> @+input:List<&2, U32> -> @+block:List<&2, U32> -> @+result:List<&2, U32> -> @input_matches:{input == block : List<&2, U32>} -> @block_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(words, block) == result : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(words, input) == result : List<&2, U32>}

def finish_tag source · line 46 · raw

@+words:List<&2, U32> -> @+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+bytes:List<&2, U32> -> @+auth:List<&2, U32> -> @+mask:List<&2, U32> -> @+tag:List<&2, U32> -> @auth_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.ghash_auth_expanded(words, aad, bytes) == auth : List<&2, U32>} -> @mask_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.aes256_encrypt_expanded(words, 0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(nonce)) == mask : List<&2, U32>} -> @xor_matches:{tag_from_parts(auth, mask) == tag : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(words, nonce, aad, bytes)) == tag : List<&2, U32>}

def nist_tag source · line 65 · raw

@+nonce:List<&2, U32> -> @+aad:List<&2, U32> -> @+bytes:List<&2, U32> -> @+auth:List<&2, U32> -> @+tag:List<&2, U32> -> @j0_matches:{0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_j0(nonce) == 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.block : List<&2, U32>} -> @auth_matches:{auth_from_hash(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistHashBlockProof.result, aad, bytes) == auth : List<&2, U32>} -> @xor_matches:{tag_from_parts(auth, 0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistBlockProof.result) == tag : List<&2, U32>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_bytes(0xaca801afcf3e822677fd6d06895d2c71/libs/AES256GCMCore.gcm_tag_output(0xaca801afcf3e822677fd6d06895d2c71/proof/AES_NistKeyScheduleProof.words_60, nonce, aad, bytes)) == tag : List<&2, U32>}