feat(crypto): Computational and Decisional Diffie–Hellman assumptions and ElGamal encryption (Boneh–Shoup Sections 10.4–10.6, 11.4) #873

Part of Track C (#640), Items 1 and 2.

Objective

Formalize the Computational Diffie–Hellman (CDH) and Decisional Diffie–Hellman (DDH) assumptions over PrimeOrderGroupFamily, prove the reductions DL ≤ CDH ≤ DDH and DDH random self-reducibility, and formalize ElGamal public-key encryption and its IND-CPA security reduction to DDH ([BonehShoup2023], Sections 10.4–10.6 and 11.4).

Scope & Deliverables

1. Complexity/Crypto/Computational/DiffieHellman.lean:
   • PrimeOrderGroupFamily.cdhGame and PrimeOrderGroupFamily.CDH (Attack Game 10.5).
   • Reduction DL ≤ CDH: dlToCDHAdversary, succProbability_discreteLogGame_le_cdhGame, isPPTOn_dlToCDHAdversary, and CDH.discreteLog.
   • PrimeOrderGroupFamily.ddhRealGame, PrimeOrderGroupFamily.ddhIdealGame, and PrimeOrderGroupFamily.DDH (Attack Game 10.6).
   • Reduction CDH ≤ DDH: cdhToDDHDistinguisher, ddhRealGame_cdhToDDHDistinguisher, ddhIdealGame_cdhToDDHDistinguisher_true_le, succProbability_cdhGame_le_advantage_ddh_add, isPPTOn_cdhToDDHDistinguisher, DDH.cdh, and DDH.discreteLog.
   • Random self-reducibility of DDH (ddhRerandomize, mapping any fixed real DDH tuple to the uniform real DDH distribution and any fixed non-DDH tuple to the uniform ideal DDH distribution).
2. Complexity/Crypto/Computational/ElGamal.lean:
   • Group-element ElGamal encryption/decryption (elGamalEncrypt, elGamalDecrypt, elGamalDecrypt_elGamalEncrypt), encoded decryption (decodeElGamal, decodeElGamal_encode, computableInPolyTime_decodeElGamal), and the one-time group mask lemma (map_uniform_add_smul_generator).
   • ElGamal bit encryption (bitElement, encodeBit, encodeBit_eq, elGamalCPAGame, elGamalINDCPA) reusing Cslib.Crypto.Encryption.Adversary and Adversary.IsPPT.
   • Reduction of ElGamal IND-CPA security to DDH ([BonehShoup2023], Theorem 11.1): elGamalToDDHDistinguisher, ddhRealGame_elGamalToDDHDistinguisher, ddhIdealGame_elGamalToDDHDistinguisher_false_eq_true, advantage_elGamalCPAGame_le, isPPTOn_elGamalToDDHDistinguisher, and DDH.elGamalINDCPA.
3. ComplexityTests/Crypto/DiffieHellman.lean:
   • Concrete group instance and distinguisher tests, plus #guard_msgs in #print axioms guards for all headline theorems.