proposition: Theorem A_HMAC_NMAC_close : | Pr[A_HMAC] - Pr[A_NMAC] | <= RKA_Advantage _ _ _ (Rnd b) (Rnd c) (dual_f h) (BVxor b) HMAC_RKA_A.
proof: Proof. rewrite A_HMAC_RKA_equiv. rewrite A_NMAC_RKA_equiv. reflexivity. Qed.
imports: FCF PRF SplitVector HMAC_spec