def checkpoint_changed_key_rejected

qasim-bend-kit@0.1.0.2 · proof/AES_NistTamperVectorProof.bend:58

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as Obs

58def checkpoint_changed_key_rejected() ->
59    {Obs.decrypt_expanded(zero_words(), changed_key_aad(), changed_key_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}:
60    Obs.finish_auth(zero_words(), changed_key_aad(), changed_key_envelope(),
61        changed_key_computed_tag(), False{}, Fail{AES.AuthenticationFailed{}},
62        checkpoint_changed_key_tag(), {==}, {==})