proposition: Theorem A_NMAC_RKA_equiv : Pr[A_NMAC] == Pr[RKA_G1 _ _ _ (Rnd b) (Rnd c) (BVxor b) HMAC_RKA_A].
proof: Proof. rewrite A_NMAC_G1_equiv . unfold A_NMAC_G1, RKA_G1, HMAC_RKA_A. comp_irr_r. wftac. simpl. inline_first. comp_skip. comp_simp. inline_first. unfold RKA_randomFunc, randomFunc. simpl. case_eq ( @eqbPair (Bvector b) (Bvector c) (Bvector_EqDec b) (Bvector_EqDec c) (@pair (Bvector b) (Bvector c) (BVxor b ipad x) iv) (@pair (Bvector b) (Bvector c) (BVxor b opad x) iv) ); intuition. unfold eqbPair in *. simpl in *. apply andb_true_iff in H1. intuition. apply eqbBvector_sound in H2. exfalso. eapply opad_ne_ipad. eapply xor_1_1. eauto. inline_first. comp_skip. comp_simp. inline_first. comp_skip. comp_simp. simpl. inline_first. comp_simp. intuition. Qed.
imports: FCF PRF SplitVector HMAC_spec