The expected inverse group order is negligible under DDH

If a prime-order group family satisfies DDH for a setup distribution, then the expected inverse group order n ↦ ∑' d, setup n d * (F.order d)⁻¹ is negligible, with no separate lower-bound hypothesis on the group orders. The distinguisher tests whether the third challenge element is the identity: it succeeds with probability 1 / q + (q - 1) / q² on real triples and 1 / q on random ones, so the expected inverse order is at most twice its advantage.

DDH clients can use this bound without importing Naor–Reingold.

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_expected_inv_order: F.DDH setup implies that the expected inverse group order is negligible.

References

• [BS23], Attack Game 10.6 (the DDH experiment). The bound itself is original.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_expected_inv_order {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} (hDDH : F.DDH setup) : Negligible fun (n : ℕ) => (∑' (d : F.Desc), (setup n) d * (↑(F.order d))⁻¹).toNNReal

Expected inverse group order is negligible under DDH (original): if F.DDH setup holds, then n ↦ (∑' d, setup n d * (F.order d)⁻¹).toNNReal is negligible.