Strict-PPT ElGamal Key Generation, KEM Encapsulation, and Encryption.INDCPAOn Bridges

This module defines uniform strict-PPT (IsPPTOn) key generation, encapsulation, decapsulation, and encryption for multiplicative ElGamal and Hashed ElGamal ([BS23], Section 11.5, pp. 445–446, Remark 11.1, Section 11.5.2, Theorem 11.5, pp. 449–451, Exercise 11.5(a), p. 459, and Exercise 11.9, pp. 460–461) using ProbComp.sampleModNat, and connects the PMF-level ElGamal games in Complexity/Crypto/Computational/ElGamal.lean directly to Encryption.KEMINDCPA, Encryption.INDCPAOf, Encryption.INDCPAOn, and Encryption.INDCPA.

• Paraphrase of [BS23], Section 11.5 (p. 445) and Remark 11.1 (p. 446): key generation samples $\alpha \leftarrow \mathbb{Z}_q$ and outputs $(pk = \alpha \cdot g, sk = \alpha)$; in the $\mathcal{E}'_{\mathrm{EG}}$ variant of Remark 11.1, encapsulation/encryption samples $\beta \leftarrow \mathbb{Z}_q$, sets $v = \beta \cdot g$ and $w = \beta \cdot u$, derives the symmetric key $k = H(w)$, and encrypts $m$ under $k$; decapsulation/decryption computes $w = \alpha \cdot v$, recovers $k = H(w)$, and decrypts $c$ under $k$.
• Paraphrase of [BS23], Exercise 11.5(a) (p. 459) and Exercise 11.9 (pp. 460–461): multiplicative ElGamal encrypts a group element $m \in G$ as $(\beta \cdot g, \beta \cdot u + m)$ and is IND-CPA secure under DDH; Hashed ElGamal acts as an IND-CPA secure KEM under DDH and SecureKDF, and composing it with any one-time semantically secure DEM yields an IND-CPA secure public-key encryption scheme.

Main definitions

• Cslib.Crypto.PrimeOrderGroupFamily.elGamalKeyGenProb: uniform strict-PPT ElGamal key generation.
• Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalEncapsProb, Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecaps: uniform strict-PPT Hashed ElGamal KEM encapsulation and deterministic polynomial-time decapsulation.
• Cslib.Crypto.PrimeOrderGroupFamily.kemToDDHDistinguisher, Cslib.Crypto.PrimeOrderGroupFamily.kemToKDFDistinguisher: DDH and KDF reductions from a KEM distinguisher.
• Cslib.Crypto.PrimeOrderGroupFamily.elGamalEncryptProb, Cslib.Crypto.PrimeOrderGroupFamily.elGamalDecryptDet: uniform strict-PPT multiplicative ElGamal encryption and deterministic polynomial-time decryption.

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecaps_hashedElGamalEncapsProb, Cslib.Crypto.PrimeOrderGroupFamily.elGamalDecryptDet_elGamalEncryptProb: support-level decapsulation and decryption correctness.
• Cslib.Crypto.PrimeOrderGroupFamily.advantage_kemGame_hashedElGamalEncapsProb_le, Cslib.Crypto.PrimeOrderGroupFamily.DDH.kemINDCPA_hashedElGamalEncapsProb: quantitative KEM advantage bound and Encryption.KEMINDCPA security of Hashed ElGamal under DDH and SecureKDF.
• Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpaOf_hybrid_hashedElGamal, Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpaOn_hybrid_hashedElGamal, Cslib.Crypto.PrimeOrderGroupFamily.DDH.wordINDCPA_hybrid_hashedElGamal: Theorem 11.5 via Encryption.INDCPAOf, Encryption.INDCPAOn, and Encryption.WordINDCPA for any one-time semantically secure symmetric cipher (Encryption.DEMOneTimeINDCPAOf / Encryption.DEMOneTimeINDCPAOn / Encryption.DEMOneTimeWordINDCPA).
• Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpaOn_elGamalEncryptProb, Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpa_elGamalBitEncryptProb: multiplicative and bit ElGamal satisfy Encryption.INDCPAOn and Encryption.INDCPA under DDH.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 11.5 (pp. 445–446, Remark 11.1), Section 11.5.2 (pp. 448–451, Theorem 11.5), Exercise 11.5(a) (p. 459), and Exercise 11.9 (pp. 460–461).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.elGamalKeyGenProb (F : PrimeOrderGroupFamily) (d : ℕ → F.Desc) (n : ℕ) : ProbComp (List Bool × List Bool)

Probabilistic polynomial-time ElGamal key generation for a group description family d : ℕ → F.Desc ([BS23], Section 11.5, p. 445, and Exercise 11.5, p. 459): sample a ← sampleExp n (d n) and output (encPair F.encDesc encBits (d n, encode (a • g)), encNat a).

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_elGamalKeyGenProb (F : PrimeOrderGroupFamily) {d : ℕ → F.Desc} (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (F.elGamalKeyGenProb d)

elGamalKeyGenProb is uniformly strict PPT whenever d is computable in polynomial time.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalEncapsProb (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : ℕ → F.Desc) (n : ℕ) (pk : List Bool) : ProbComp (List Bool × List Bool)

Probabilistic polynomial-time Hashed ElGamal KEM encapsulation for a group description family d : ℕ → F.Desc ([BS23], Section 11.5, p. 445, Remark 11.1, p. 446, and Exercise 11.9, pp. 460–461): sample b ← sampleExp n (d n), unpack u = dropFrame pk, and output (H (d n, encode (b • u)), encode (b • g)).

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_hashedElGamalEncapsProb (F : PrimeOrderGroupFamily) {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool) => F.hashedElGamalEncapsProb H d p.1 p.2

hashedElGamalEncapsProb is uniformly strict PPT whenever H and d are computable in polynomial time.

def Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecaps (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : ℕ → F.Desc) (n : ℕ) (sk ctKem : List Bool) : List Bool

Deterministic polynomial-time Hashed ElGamal KEM decapsulation ([BS23], Section 11.5, p. 445, Remark 11.1, p. 446): given secret key sk = encNat a and KEM ciphertext ctKem = encode (b • g), recover H (d n, encode (a • v)).

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_hashedElGamalDecaps (F : PrimeOrderGroupFamily) {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => F.hashedElGamalDecaps H d p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

hashedElGamalDecaps is computable in polynomial time whenever H and d are.

theorem Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalDecaps_hashedElGamalEncapsProb (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : ℕ → F.Desc) (n : ℕ) {keys : List Bool × List Bool} (hkeys : keys ∈ (F.elGamalKeyGenProb d n).eval.support) {encapsulated : List Bool × List Bool} (hencaps : encapsulated ∈ (F.hashedElGamalEncapsProb H d n keys.1).eval.support) : F.hashedElGamalDecaps H d n keys.2 encapsulated.2 = encapsulated.1

Hashed ElGamal KEM decapsulation correctness: for any n : ℕ, any (pk, sk) in the support of elGamalKeyGenProb d n, and any (k, ctKem) in the support of hashedElGamalEncapsProb H d n pk, hashedElGamalDecaps H d n sk ctKem = k.

def Cslib.Crypto.PrimeOrderGroupFamily.kemToDDHDistinguisher (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (distinguisher : Distinguisher) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

DDH distinguisher constructed from a KEMAdversary (Distinguisher) for (elGamalKeyGenProb d, hashedElGamalEncapsProb H d).

def Cslib.Crypto.PrimeOrderGroupFamily.kemToKDFDistinguisher (F : PrimeOrderGroupFamily) (distinguisher : Distinguisher) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

KDF distinguisher constructed from a KEMAdversary (Distinguisher) for (elGamalKeyGenProb d, hashedElGamalEncapsProb H d).

theorem Cslib.Crypto.PrimeOrderGroupFamily.ddhIdealGame_kemToDDHDistinguisher_eq_kdfRealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (distinguisher : Distinguisher) (n : ℕ) : F.ddhIdealGame setup (F.kemToDDHDistinguisher H distinguisher) n = F.kdfRealGame setup H (F.kemToKDFDistinguisher distinguisher) n

ddhIdealGame for kemToDDHDistinguisher is identical to kdfRealGame for kemToKDFDistinguisher.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_kemToDDHDistinguisher (F : PrimeOrderGroupFamily) {H : F.Desc × List Bool → List Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) {distinguisher : Distinguisher} (hD : Probability.IsPPT Turing.MultiTapeTM.encBool distinguisher) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.kemToDDHDistinguisher H distinguisher input.1 input.2

kemToDDHDistinguisher is uniform strict PPT whenever H is polynomial time and distinguisher is uniform strict PPT.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_kemToKDFDistinguisher (F : PrimeOrderGroupFamily) {distinguisher : Distinguisher} (hD : Probability.IsPPT Turing.MultiTapeTM.encBool distinguisher) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.kemToKDFDistinguisher distinguisher input.1 input.2

kemToKDFDistinguisher is uniform strict PPT whenever distinguisher is.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_kemGame_hashedElGamalEncapsProb_le (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (d : ℕ → F.Desc) (distinguisher : Distinguisher) (n : ℕ) : Game.advantage (Encryption.kemRealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n).eval (Encryption.kemIdealGame (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d) distinguisher n).eval ≤ (F.ddhRealGame (fun (m : ℕ) => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n).advantage (F.ddhIdealGame (fun (m : ℕ) => PMF.pure (d m)) (F.kemToDDHDistinguisher H distinguisher) n) + (F.kdfRealGame (fun (m : ℕ) => PMF.pure (d m)) H (F.kemToKDFDistinguisher distinguisher) n).advantage (F.kdfIdealGame (fun (m : ℕ) => PMF.pure (d m)) (fun (m : ℕ) => m) (F.kemToKDFDistinguisher distinguisher) n) + 4 / 2 ^ n

Quantitative KEM IND-CPA bound for Hashed ElGamal: the KEM distinguishing advantage of distinguisher against (elGamalKeyGenProb d, hashedElGamalEncapsProb H d) is bounded by the DDH advantage of kemToDDHDistinguisher H distinguisher plus the KDF advantage of kemToKDFDistinguisher distinguisher plus 4 / 2 ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.kemINDCPA_hashedElGamalEncapsProb {F : PrimeOrderGroupFamily} {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} (hDDH : F.DDH fun (n : ℕ) => PMF.pure (d n)) (hKDF : F.SecureKDF (fun (n : ℕ) => PMF.pure (d n)) H fun (n : ℕ) => n) (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) : Encryption.KEMINDCPA (F.elGamalKeyGenProb d) (F.hashedElGamalEncapsProb H d)

Hashed ElGamal KEM is Encryption.KEMINDCPA-secure under DDH and SecureKDF ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451, and Exercise 11.9, pp. 460–461): for any group description family d : ℕ → F.Desc, if F.DDH (fun n => PMF.pure (d n)) and F.SecureKDF (fun n => PMF.pure (d n)) H (fun n => n) hold and H is computable in polynomial time, then (elGamalKeyGenProb d, hashedElGamalEncapsProb H d) satisfies Encryption.KEMINDCPA.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpaOf_hybrid_hashedElGamal {F : PrimeOrderGroupFamily} {Msg : Type} {encMsg : Msg ↪ List Bool} {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hDDH : F.DDH fun (n : ℕ) => PMF.pure (d n)) (hKDF : F.SecureKDF (fun (n : ℕ) => PMF.pure (d n)) H fun (n : ℕ) => n) (hdem : Encryption.DEMOneTimeINDCPAOf encMsg encryptSym) (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) : Encryption.INDCPAOf encMsg (F.elGamalKeyGenProb d) (Encryption.hybridEncrypt (F.hashedElGamalEncapsProb H d) encryptSym)

Theorem 11.5 via Encryption.INDCPAOf ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451): combining DDH.kemINDCPA_hashedElGamalEncapsProb with KEMINDCPA.hybrid_indcpa, Hashed ElGamal coupled with any uniform strict-PPT one-time semantically secure symmetric cipher encryptSym (DEMOneTimeINDCPAOf encMsg encryptSym) satisfies Encryption.INDCPAOf.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpaOn_hybrid_hashedElGamal {F : PrimeOrderGroupFamily} {Msg : Type} {encMsg : Msg ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)} (hDDH : F.DDH fun (n : ℕ) => PMF.pure (d n)) (hKDF : F.SecureKDF (fun (n : ℕ) => PMF.pure (d n)) H fun (n : ℕ) => n) (hdem : Encryption.DEMOneTimeINDCPAOn valid encMsg encryptSym) (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × Msg × Msg) => valid p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair encMsg encMsg))) Turing.MultiTapeTM.encBool) (hpk : ∀ (n : ℕ) (pk : List Bool) (m₀ m₁ : Msg), valid n pk m₀ m₁ = valid n [] m₀ m₁) (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => encryptSym p.1 p.2.1 p.2.2) : Encryption.INDCPAOn valid encMsg (F.elGamalKeyGenProb d) (Encryption.hybridEncrypt (F.hashedElGamalEncapsProb H d) encryptSym)

Theorem 11.5 via Encryption.INDCPAOn ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451): combining DDH.kemINDCPA_hashedElGamalEncapsProb with KEMINDCPA.hybrid_indcpaOn, for any polynomial-time admissibility predicate valid that ignores the public key (such as the equal-length predicate fun _ _ m₀ m₁ => m₀.length == m₁.length), Hashed ElGamal coupled with any one-time semantically secure symmetric cipher encryptSym (DEMOneTimeINDCPAOn valid encMsg encryptSym) satisfies Encryption.INDCPAOn.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.wordINDCPA_hybrid_hashedElGamal {F : PrimeOrderGroupFamily} {H : F.Desc × List Bool → List Bool} {d : ℕ → F.Desc} {encryptSym : ℕ → List Bool → List Bool → ProbComp (List Bool)} (hDDH : F.DDH fun (n : ℕ) => PMF.pure (d n)) (hKDF : F.SecureKDF (fun (n : ℕ) => PMF.pure (d n)) H fun (n : ℕ) => n) (hdem : Encryption.DEMOneTimeWordINDCPA encryptSym) (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) (hencryptSym : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × List Bool) => encryptSym p.1 p.2.1 p.2.2) : Encryption.WordINDCPA (F.elGamalKeyGenProb d) (Encryption.hybridEncrypt (F.hashedElGamalEncapsProb H d) encryptSym)

Theorem 11.5 via Encryption.WordINDCPA ([BS23], Section 11.5.2, Theorem 11.5, pp. 449–451): combining DDH.indcpaOn_hybrid_hashedElGamal with Attack Game 11.1's equal-length rule (fun _ _ m₀ m₁ => m₀.length == m₁.length), Hashed ElGamal coupled with any equal-length one-time semantically secure word cipher encryptSym (DEMOneTimeWordINDCPA encryptSym) satisfies Encryption.WordINDCPA.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.elGamalEncryptProb (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc → Msg → List Bool) (d : ℕ → F.Desc) (n : ℕ) (pk : List Bool) (m : Msg) : ProbComp (List Bool)

Probabilistic polynomial-time multiplicative ElGamal encryption for a group description family d : ℕ → F.Desc and message encoder encodeMsg : F.Desc → Msg → List Bool ([BS23], Exercise 11.5, p. 459): sample b ← sampleExp n (d n), unpack u = dropFrame pk, and output encPair encBits encBits (encodeElGamalEncrypt (d n, u, encodeMsg (d n) m, b)).

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_elGamalEncryptProb (F : PrimeOrderGroupFamily) {Msg : Type} {encMsg : Msg ↪ List Bool} {encodeMsg : F.Desc → Msg → List Bool} {d : ℕ → F.Desc} (hencMsg : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : F.Desc × Msg) => encodeMsg p.1 p.2) (Turing.MultiTapeTM.encPair F.encDesc encMsg) Turing.MultiTapeTM.encBits) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits encMsg)) Turing.MultiTapeTM.encBits fun (p : ℕ × List Bool × Msg) => F.elGamalEncryptProb encodeMsg d p.1 p.2.1 p.2.2

elGamalEncryptProb is uniformly strict PPT whenever encodeMsg and d are computable in polynomial time.

def Cslib.Crypto.PrimeOrderGroupFamily.elGamalDecryptDet (F : PrimeOrderGroupFamily) (d : ℕ → F.Desc) (n : ℕ) (sk ct : List Bool) : List Bool

Deterministic polynomial-time multiplicative ElGamal decryption on words: given secret key sk = encNat a and ciphertext ct = encPair encBits encBits (v, e), compute decodeElGamal (d n, ofBits sk, unframe ct, dropFrame ct).

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_elGamalDecryptDet (F : PrimeOrderGroupFamily) {d : ℕ → F.Desc} (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => F.elGamalDecryptDet d p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

elGamalDecryptDet is computable in polynomial time whenever d is.

theorem Cslib.Crypto.PrimeOrderGroupFamily.elGamalDecryptDet_elGamalEncryptProb (F : PrimeOrderGroupFamily) (d : ℕ → F.Desc) (n : ℕ) {keys : List Bool × List Bool} (hkeys : keys ∈ (F.elGamalKeyGenProb d n).eval.support) (m : F.Carrier (d n)) {ct : List Bool} (hct : ct ∈ (F.elGamalEncryptProb (fun (x : F.Desc) (x_1 : List Bool) => x_1) d n keys.1 (F.encode (d n) m)).eval.support) : F.elGamalDecryptDet d n keys.2 ct = F.encode (d n) m

Multiplicative ElGamal decryption correctness on ProbComp outputs: for any (pk, sk) in the support of elGamalKeyGenProb d n, any m : F.Carrier (d n), and any ct in the support of elGamalEncryptProb (fun d x => x) d n pk (F.encode (d n) m), elGamalDecryptDet d n sk ct = F.encode (d n) m.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_gameOn_elGamalMsgCPAGameOn_le (F : PrimeOrderGroupFamily) {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool) (encodeMsg : F.Desc → Msg → List Bool) (d : ℕ → F.Desc) (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ) : Game.advantage (Encryption.gameOn valid (F.elGamalKeyGenProb d) (F.elGamalEncryptProb encodeMsg d) adversary bit n).eval (F.elGamalMsgCPAGameOn valid encodeMsg (fun (m : ℕ) => PMF.pure (d m)) adversary bit n) ≤ 2 / 2 ^ n

The native Encryption.gameOn experiment for (elGamalKeyGenProb d, elGamalEncryptProb encodeMsg d) is within statistical distance 2 / 2 ^ n of the ideal exact-uniform PMF game elGamalMsgCPAGameOn valid encodeMsg (fun n => PMF.pure (d n)).

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpaOn_elGamalEncryptProb {F : PrimeOrderGroupFamily} {Msg : Type} {encMsg : Msg ↪ List Bool} {valid : ℕ → List Bool → Msg → Msg → Bool} {encodeMsg : F.Desc → Msg → List Bool} {d : ℕ → F.Desc} (hDDH : F.DDH fun (n : ℕ) => PMF.pure (d n)) (hvalid : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × Msg × Msg) => valid p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair encMsg encMsg))) Turing.MultiTapeTM.encBool) (hsound : F.AdmitsGroupElements encodeMsg valid) (hencMsg : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : F.Desc × Msg) => encodeMsg p.1 p.2) (Turing.MultiTapeTM.encPair F.encDesc encMsg) Turing.MultiTapeTM.encBits) : Encryption.INDCPAOn valid encMsg (F.elGamalKeyGenProb d) (F.elGamalEncryptProb encodeMsg d)

Multiplicative ElGamal satisfies Encryption.INDCPAOn under DDH ([BS23], Exercise 11.5(a), p. 459): for any polynomial-time group description family d : ℕ → F.Desc, polynomial-time message encoder encodeMsg, and polynomial-time admissibility predicate valid admitting only group elements (AdmitsGroupElements encodeMsg valid), (elGamalKeyGenProb d, elGamalEncryptProb encodeMsg d) satisfies Encryption.INDCPAOn valid encMsg whenever F.DDH (fun n => PMF.pure (d n)) holds.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcpa_elGamalBitEncryptProb {F : PrimeOrderGroupFamily} {d : ℕ → F.Desc} (hDDH : F.DDH fun (n : ℕ) => PMF.pure (d n)) : Encryption.INDCPA (F.elGamalKeyGenProb d) (F.elGamalEncryptProb F.encodeBit d)

Bit ElGamal satisfies Encryption.INDCPA under DDH ([BS23], Exercise 11.5(a), p. 459): specialization of DDH.indcpaOn_elGamalEncryptProb to encodeBit.