proposition: Theorem GHMAC_PRF : PRF_Advantage (Rnd b) (Rnd c) GHMAC _ _ A <= RKA_Advantage _ _ _ ({ 0 , 1 }^b) ({ 0 , 1 }^c) (dual_f h) (BVxor b) (HMAC_RKA_A h iv fpad opad ipad A) + (PRF_Advantage ({ 0 , 1 }^c) ({ 0 , 1 }^c) h _ _ (PRF_h_A (h_star_pad h fpad) A) + cAU.Adv_WCR _ _ (h_star_pad h fpad) ({ 0 , 1 }^c) (au_F_A A)).
proof: Proof. eapply leRat_trans. unfold PRF_Advantage. eapply ratDistance_le_trans. eapply A_HMAC_NMAC_close. trivial. specialize (GNMAC_PRF h fpad A_wf); intuition. unfold A_NMAC. eapply H. reflexivity. Qed.
imports: FCF HMAC_spec PRF NMAC_to_HMAC hF GNMAC_PRF