def tag_parameters

qasim-bend-kit@0.1.0.2 · proof/AES_NistObservationProof.bend:180

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

180def tag_parameters(+words: List<&2, U32>, +aad: List<&2, U32>, +envelope: AES.Envelope,
181    +nonce: List<&2, U32>, +bytes: List<&2, U32>, +tag: List<&2, U32>,
182    nonce_matches: {AES.raw_nonce_bytes(AES.envelope_nonce(envelope)) == nonce : List<&2, U32>},
183    ciphertext_matches: {AES.ciphertext(envelope) == bytes : List<&2, U32>},
184    computed: {Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, bytes)) == tag : List<&2, U32>}) ->
185    {envelope_tag_computed(words, aad, envelope) == tag : List<&2, U32>}:
186    Equal.trans(List<&2, U32>, envelope_tag_computed(words, aad, envelope),
187        Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, AES.ciphertext(envelope))), tag,
188        Equal.cong(List<&2, U32>, List<&2, U32>, value =>
189            Core.gcm_tag_bytes(Core.gcm_tag_output(words, value, aad, AES.ciphertext(envelope))),
190            AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), nonce, nonce_matches),
191        Equal.trans(List<&2, U32>, Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, AES.ciphertext(envelope))),
192            Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, bytes)), tag,
193            Equal.cong(List<&2, U32>, List<&2, U32>, value =>
194                Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, value)),
195                AES.ciphertext(envelope), bytes, ciphertext_matches), computed))