proposition: Theorem GHMAC_to_HMAC : PRF_Advantage (Rnd b) (Rnd c) HMAC _ _ A == PRF_Advantage (Rnd b) (Rnd c) GHMAC _ _ A_GHMAC.
proof: Proof. unfold PRF_Advantage. eapply ratDistance_eqRat_compat. unfold PRF_G_A, HMAC, HMAC_spec.HMAC, GHMAC, NMAC_to_HMAC.GHMAC. comp_skip. unfold A_GHMAC. eapply comp_spec_eq_impl_eq. simpl. inline_first. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => True)); intuition. unfold f_oracle. unfold HMAC_2K, HMAC_spec.GHMAC. inline_first. comp_simp. inline_first. comp_simp. simpl. eapply comp_spec_ret; intuition. simpl in *. comp_simp. simpl. inline_first. comp_simp. intuition; subst. eapply comp_spec_eq_refl. unfold PRF_G_B, A_GHMAC. eapply comp_spec_eq_impl_eq. simpl. inline_first. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => forall x, arrayLookup _ (snd b) (splitAndPad x) = arrayLookup _ a x)). intuition. intuition. inline_first. unfold RndR_func, randomFunc. rewrite H. case_eq ( arrayLookup Message_EqDec x1 a ); intuition. comp_simp. inline_first. comp_simp. simpl. eapply comp_spec_ret; intuition. inline_first. comp_skip. comp_simp. inline_first. comp_simp. simpl. eapply comp_spec_ret; intuition. simpl. case_eq (eqb x a); intuition. rewrite eqb_leibniz in H5. subst. rewrite eqb_refl. trivial. case_eq (eqb (splitAndPad x) (splitAndPad a)); intuition. rewrite eqb_leibniz in H6. apply splitAndPad_1_1 in H6. subst. rewrite eqb_refl in H5. discriminate. simpl in *. intuition; subst. comp_simp. simpl. inline_first. comp_simp. eapply comp_spec_eq_refl. Qed.
imports: FCF HMAC_spec PRF NMAC_to_HMAC hF GHMAC_PRF