proposition: Theorem GNMAC_PRF : PRF_Advantage (Rnd (c + c)) (Rnd c) GNMAC _ _ A <= PRF_Advantage ({ 0 , 1 }^c) ({ 0 , 1 }^c) h (Bvector_EqDec b) _ (PRF_h_A (h_star_pad) A) + cAU.Adv_WCR _ _ (h_star_pad) ({ 0 , 1 }^c) (au_F_A A).
proof: Proof. specialize (hF_PRF h h_star_pad A_wf); intuition. Qed.
imports: FCF HMAC_spec PRF hF