proposition: Theorem DRBG_P_DH : | Pr[DRBG_P G2] - Pr[DRBG_P DRBG_GB] | == @DDH_Advantage _ groupOp ident inverse _ g order A.
proof: Proof. unfold DDH_Advantage. unfold DRBG_P, DRBG_GB, G2, DDH0, DDH1. unfold P. eapply ratDistance_eqRat_compat. comp_skip. comp_skip. rewrite groupExp_mult. reflexivity. reflexivity. Qed.
imports: FCF DiffieHellman RndNat