def rejects_changed_key

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

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

64def rejects_changed_key() ->
65    {AES.decrypt(zero_key(), changed_key_aad(), changed_key_envelope()) == Fail{AES.AuthenticationFailed{}} : Result<&2, &2, AES.Error, List<&2, U32>>}:
66    Obs.finish_decrypt(zero_key(), changed_key_aad(), changed_key_envelope(),
67        zero_words(), Fail{AES.AuthenticationFailed{}}, {==}, {==}, checkpoint_zero_key(), checkpoint_changed_key_rejected())