def nist_tag

qasim-bend-kit@0.1.0.2 · proof/AES_NistTagProof.bend:65

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
import qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend as Key
import qasim-bend-kit@0.1.0.2/proof/AES_NistBlockProof.bend as J0
import qasim-bend-kit@0.1.0.2/proof/AES_NistBlockComposeProof.bend as J0Proof
import qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend as Hash
import qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockComposeProof.bend as HashProof

65def nist_tag(+nonce: List<&2, U32>, +aad: List<&2, U32>, +bytes: List<&2, U32>,
66    +auth: List<&2, U32>, +tag: List<&2, U32>,
67    j0_matches: {Core.gcm_j0(nonce) == J0.block() : List<&2, U32>},
68    auth_matches: {auth_from_hash(Hash.result(), aad, bytes) == auth : List<&2, U32>},
69    xor_matches: {tag_from_parts(auth, J0.result()) == tag : List<&2, U32>}) ->
70    {Core.gcm_tag_bytes(Core.gcm_tag_output(Key.words_60(), nonce, aad, bytes)) == tag : List<&2, U32>}:
71    finish_tag(Key.words_60(), nonce, aad, bytes, auth, J0.result(), tag,
72        auth_from_checked_hash(Key.words_60(), Hash.result(), aad, bytes, auth,
73            aes_block_input_matches(Key.words_60(), [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], Hash.block(), Hash.result(),
74                {==}, HashProof.expanded_block_matches()), auth_matches),
75        aes_block_input_matches(Key.words_60(), Core.gcm_j0(nonce), J0.block(), J0.result(),
76            j0_matches, J0Proof.expanded_block_matches()), xor_matches)