proposition: Theorem A_HMAC_RKA_equiv : Pr[A_HMAC] == Pr[RKA_G0 _ (Rnd b) (dual_f h) (BVxor b) HMAC_RKA_A].
proof: Proof. unfold A_HMAC, RKA_G0, GHMAC, HMAC_RKA_A, GNMAC, HMAC_spec.GHMAC. comp_skip. simpl. repeat ( inline_first; comp_simp). comp_skip. eapply comp_spec_eq_impl_eq. eapply comp_spec_consequence. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => a = b)). trivial. intuition. unfold f_oracle. eapply comp_spec_ret; intuition. simpl. specialize (GHMAC_2K_GNMAC_equiv (Vector.append (x xor opad) (x xor ipad)) a0); intuition. rewrite splitVector_append in H1. unfold dual_f. eapply eq_trans. eapply H1. unfold GNMAC. f_equal. f_equal. f_equal. eapply BVxor_comm. f_equal. eapply BVxor_comm. intuition. destruct b2; simpl in *; subst; intuition. comp_simp. simpl. inline_first. comp_simp. intuition. Qed.
imports: FCF PRF SplitVector HMAC_spec