feat(Crypto/ElGamal): general-cipher Hashed ElGamal IND-CPA security (Theorem 11.5)

Complexity.lean

@@ -1524,6 +1524,7 @@ public import Complexity.Crypto.Computational.DiffieHellman.MultiDDH
 public import Complexity.Crypto.Computational.DiscreteLog
 public import Complexity.Crypto.Computational.DiscreteLog.SchnorrGroup
 public import Complexity.Crypto.Computational.ElGamal
+public import Complexity.Crypto.Computational.ElGamal.GeneralCipher
 public import Complexity.Crypto.Computational.ElGamal.KDF
 public import Complexity.Crypto.Computational.ElGamal.ProbComp
 public import Complexity.Crypto.Computational.Encryption.Authenticated

Complexity/Crypto/Computational/ElGamal/ProbComp.lean

@@ -124,7 +124,9 @@ fair coins via `ProbComp.sampleModNat`, within statistical distance `1 / 2 ^ n`
 noncomputable def sampleElGamalExp (n : ℕ) (d : F.Desc) : ProbComp ℕ :=
   ProbComp.sampleModNat (n + (encNat (F.order d)).length) (F.order d)
 
-private theorem isPPTOn_sampleElGamalExp {γ : Type} {encIn : γ ↪ List Bool}
+/-- `sampleElGamalExp` is uniform strict PPT whenever `n` and `d` are computable in polynomial
+time. -/
+theorem isPPTOn_sampleElGamalExp {γ : Type} {encIn : γ ↪ List Bool}
     {n : γ → ℕ} {d : γ → F.Desc}
     (hn : ComputableInPolyTime n encIn encUnary)
     (hd : ComputableInPolyTime d encIn F.encDesc) :

Complexity/Crypto/Game.lean

@@ -46,6 +46,9 @@ directly, and computational definitions over infinite sample spaces can reuse th
   `Cslib.Crypto.Game.advantage_bind_le_of_support`,
   `Cslib.Crypto.Game.advantage_bind_comm`: `ℝ≥0` mixture, pointwise error-averaging, support,
   and `PMF.bind_comm` advantage lemmas, extracted from the reviewed support in PR #1169.
+* `Cslib.Crypto.Game.succProbability_uniform_bool_xor`,
+  `Cslib.Crypto.Game.advantage_le_two_mul_uniform_bool_xor`: hidden-bit XOR mixture success
+  probability and factor-of-two game-hop bound.
 
 ## References
 
@@ -404,5 +407,61 @@ theorem advantage_bind_comm {α β : Type*} (p : PMF α) (q : PMF β) (f g : α
       (q.bind fun b => p.bind fun a => g a b) := by
   rw [PMF.bind_comm p q f, PMF.bind_comm p q g]
 
+open Probability in
+/-- For any Boolean-indexed family of games `g : Bool → Game`, sampling a uniform hidden bit
+`bit ← PMF.uniformOfFintype Bool` and outputting `guess ^^ bit` for `guess ← g bit` succeeds with
+probability `(1 + succProbability (g false) - succProbability (g true)) / 2`. -/
+theorem succProbability_uniform_bool_xor (g : Bool → Game) :
+    (succProbability
+      ((PMF.uniformOfFintype Bool).bind fun bit => (g bit).map (fun guess => guess ^^ bit)) : ℝ) =
+      (1 + (succProbability (g false) : ℝ) - succProbability (g true)) / 2 := by
+  have h1 :
+      ((PMF.uniformOfFintype Bool).bind fun bit =>
+        (g bit).map (fun guess => guess ^^ bit)) true =
+      2⁻¹ * g false true + 2⁻¹ * g true false := by
+    rw [PMF.bind_apply, tsum_bool]
+    simp [PMF.uniformOfFintype_apply, PMF.map_apply]
+  have hfalse : (g true false).toReal = 1 - (g true true).toReal := by
+    have hsum := succProbability_add_failProbability (g true)
+    have hsumR := congrArg (fun x : ℝ≥0 => (x : ℝ)) hsum
+    simp only [NNReal.coe_add, NNReal.coe_one, succProbability, failProbability,
+      ENNReal.coe_toNNReal_eq_toReal] at hsumR
+    linarith
+  rw [coe_succProbability, h1, ENNReal.toReal_add
+    (ENNReal.mul_ne_top (by simp) (PMF.apply_ne_top _ _))
+    (ENNReal.mul_ne_top (by simp) (PMF.apply_ne_top _ _)),
+    ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_inv, ENNReal.toReal_ofNat,
+    hfalse, coe_succProbability, coe_succProbability]
+  ring
+
+open Probability in
+/-- For any two Boolean-indexed game families `g₀, g₁ : Bool → Game`, the advantage
+`advantage (g₀ false) (g₀ true)` is bounded by twice the distinguishing advantage between their
+uniform hidden-bit XOR mixtures plus `advantage (g₁ false) (g₁ true)`. -/
+theorem advantage_le_two_mul_uniform_bool_xor (g₀ g₁ : Bool → Game) :
+    advantage (g₀ false) (g₀ true) ≤
+      2 * advantage
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₀ bit).map (fun guess => guess ^^ bit))
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₁ bit).map (fun guess => guess ^^ bit)) +
+      advantage (g₁ false) (g₁ true) := by
+  rw [← NNReal.coe_le_coe]
+  simp only [NNReal.coe_add, NNReal.coe_mul, NNReal.coe_ofNat, coe_advantage,
+    succProbability_uniform_bool_xor]
+  have hle :
+      |((succProbability (g₀ false) : ℝ) - succProbability (g₀ true)) -
+        ((succProbability (g₁ false) : ℝ) - succProbability (g₁ true))| =
+      2 * |(1 + (succProbability (g₀ false) : ℝ) - succProbability (g₀ true)) / 2 -
+        (1 + (succProbability (g₁ false) : ℝ) - succProbability (g₁ true)) / 2| := by
+    rw [show (1 + (succProbability (g₀ false) : ℝ) - succProbability (g₀ true)) / 2 -
+        (1 + (succProbability (g₁ false) : ℝ) - succProbability (g₁ true)) / 2 =
+      (((succProbability (g₀ false) : ℝ) - succProbability (g₀ true)) -
+        ((succProbability (g₁ false) : ℝ) - succProbability (g₁ true))) / 2 by ring,
+      abs_div, Nat.abs_ofNat]
+    ring
+  have htri := abs_sub_abs_le_abs_sub
+    ((succProbability (g₀ false) : ℝ) - succProbability (g₀ true))
+    ((succProbability (g₁ false) : ℝ) - succProbability (g₁ true))
+  linarith
+
 end Game
 end Cslib.Crypto

ComplexityTests/Crypto/DiffieHellman.lean

@@ -8,6 +8,7 @@ import Complexity.Crypto.Computational.DiscreteLog.SchnorrGroup
 import Complexity.Crypto.Computational.DiffieHellman
 import Complexity.Crypto.Computational.DiffieHellman.EncodingBounds
 import Complexity.Crypto.Computational.ElGamal
+import Complexity.Crypto.Computational.ElGamal.GeneralCipher
 import Complexity.Crypto.Computational.ElGamal.KDF
 import Complexity.Crypto.Computational.ElGamal.ProbComp
 import Complexity.Crypto.Negligible.Basic
@@ -631,4 +632,152 @@ example (d : ℕ → schnorrGroups.Desc)
       admitsGroupElements_twoElements (by fun_prop),
     hDDH.indcpa_elGamalBitEncryptProb⟩
 
+/-! ### Theorem 11.5: General-cipher Hashed ElGamal tests -/
+
+/-- Equal-length challenge-pair admissibility predicate on bit words (`Attack Game 11.1`,
+[BonehShoup2023], p. 436). -/
+def equalLengthWords (_ : ℕ) (_ : List Bool) (m₀ m₁ : List Bool) : Bool :=
+  m₀.length == m₁.length
+
+/-- `equalLengthWords` is computable in polynomial time. -/
+theorem computableInPolyTime_equalLengthWords :
+    ComputableInPolyTime
+      (fun p : ℕ × List Bool × List Bool × List Bool =>
+        equalLengthWords p.1 p.2.1 p.2.2.1 p.2.2.2)
+      (encPair encUnary (encPair encBits (encPair encBits encBits))) encBool := by
+  unfold equalLengthWords
+  have h1 : ComputableInPolyTime
+      (fun p : ℕ × List Bool × List Bool × List Bool => (p.2.2.1).length)
+      (encPair encUnary (encPair encBits (encPair encBits encBits))) encUnary :=
+    (ComputableInPolyTime.encoding_length encBits).comp (by fun_prop)
+  have h2 : ComputableInPolyTime
+      (fun p : ℕ × List Bool × List Bool × List Bool => (p.2.2.2).length)
+      (encPair encUnary (encPair encBits (encPair encBits encBits))) encUnary :=
+    (ComputableInPolyTime.encoding_length encBits).comp (by fun_prop)
+  have hbeq : ComputableInPolyTime (fun q : ℕ × ℕ => q.1 == q.2)
+      (encPair encUnary encUnary) encBool := by fun_prop
+  exact hbeq.comp (h1.prod h2)
+
+/-- Every encoded element of `schnorrGroups.Carrier d` has bit-length bounded by the description
+length `(schnorrGroups.encDesc d).length`. -/
+theorem schnorrGroups_encode_length_le (d : schnorrGroups.Desc) (x : schnorrGroups.Carrier d) :
+    (schnorrGroups.encode d x).length ≤ (schnorrGroups.encDesc d).length := by
+  have hbits (a b : ℕ) (h : a ≤ b) : a.bits.length ≤ b.bits.length := by
+    rw [Nat.size_eq_bits_len, Nat.size_eq_bits_len]
+    exact Nat.size_le_size h
+  have : NeZero d.1.1 := ⟨d.2.prime_modulus.ne_zero⟩
+  have hsize : (schnorrGroups.encode d x).length ≤ (encNat d.1.1).length :=
+    hbits _ _ (le_of_lt (ZMod.val_lt _))
+  have hdesc : (encNat d.1.1).length ≤ (schnorrGroups.encDesc d).length := by
+    change (encNat d.1.1).length ≤ (encPair encNat (encPair encNat encNat) d.1).length
+    simp only [encPair_apply, List.length_append, length_frame]
+    omega
+  exact hsize.trans hdesc
+
+/-- Concrete word-level round-trip check for `encodeHashedElGamalCipherEncrypt` and
+`decodeHashedElGamalCipher` on `d23` with `(a = 3, b = 5)` using `linearHashKDF (fun _ => 4)
+(fun _ => 6)` and a 4-bit bitwise-XOR cipher. -/
+example :
+    let dSeed : schnorrGroups.withSeed.Desc := (d23, List.replicate 52 true)
+    let H := schnorrGroups.linearHashKDF (fun _ => 4) (fun _ => 6)
+    let xorCipher (p : List Bool × List Bool) : List Bool := List.zipWith bne p.1 p.2
+    let pk := schnorrGroups.withSeed.encodeElGamalPublicKey (dSeed, 3)
+    let m := [true, false, true, false]
+    let ct := schnorrGroups.withSeed.encodeHashedElGamalCipherEncrypt H xorCipher (dSeed, pk, m, 5)
+    schnorrGroups.withSeed.decodeHashedElGamalCipher H xorCipher (dSeed, 3, ct.1, ct.2) = m := by
+  decide
+
+/-- Positive-side instantiation of `DDH.negligible_hashedElGamalCipherCPAGameOn_linearHashKDF`
+with a consistent polynomial description-dependent encoding bound
+`bound d := (schnorrGroups.encDesc d).length`, super-polynomial group order `2 ^ (2 * n) ≤ order d`,
+and the one-time pad symmetric word cipher `Encryption.otpWordEncrypt`
+(`Encryption.demOneTimeWordINDCPA_otpWordEncrypt`): IND-CPA security holds under `schnorrGroups.DDH`
+alone with no separate KDF or Game 2 assumption. -/
+example (setupProb : ℕ → ProbComp schnorrGroups.Desc)
+    (hsetup : IsPPTOn encUnary schnorrGroups.encDesc setupProb)
+    (hDDH : schnorrGroups.DDH (fun n => ProbComp.eval (setupProb n)))
+    (keyLen : schnorrGroups.Desc → ℕ)
+    (hkey_poly : ComputableInPolyTime keyLen schnorrGroups.encDesc encUnary)
+    (hkey : ∀ n, ∀ d ∈ (ProbComp.eval (setupProb n)).support, keyLen d = n)
+    (hsize : ∀ n, ∀ d ∈ (ProbComp.eval (setupProb n)).support,
+      2 ^ (2 * n) ≤ schnorrGroups.order d) :
+    Negligible fun n =>
+      Game.advantage
+        (schnorrGroups.withSeed.hashedElGamalCipherCPAGameOn equalLengthWords
+          (schnorrGroups.seededSetup (fun m => ProbComp.eval (setupProb m))
+            (schnorrGroups.linearHashSeedLen (fun n => n)
+              (fun d => (schnorrGroups.encDesc d).length)))
+          (schnorrGroups.linearHashKDF keyLen (fun d => (schnorrGroups.encDesc d).length))
+          Encryption.otpWordEncrypt hashedWordAdversary false n)
+        (schnorrGroups.withSeed.hashedElGamalCipherCPAGameOn equalLengthWords
+          (schnorrGroups.seededSetup (fun m => ProbComp.eval (setupProb m))
+            (schnorrGroups.linearHashSeedLen (fun n => n)
+              (fun d => (schnorrGroups.encDesc d).length)))
+          (schnorrGroups.linearHashKDF keyLen (fun d => (schnorrGroups.encDesc d).length))
+          Encryption.otpWordEncrypt hashedWordAdversary true n) := by
+  refine hDDH.negligible_hashedElGamalCipherCPAGameOn_linearHashKDF
+    Encryption.demOneTimeWordINDCPA_otpWordEncrypt hsetup hkey_poly
+    (ComputableInPolyTime.encoding_length schnorrGroups.encDesc)
+    (fun _ => Nat.two_pow_pos _) hkey (fun _ d _ x => schnorrGroups_encode_length_le d x)
+    hsize ?_ computableInPolyTime_equalLengthWords (fun _ _ _ _ _ h => h)
+    Encryption.isPPTOn_otpWordEncrypt hashedWordAdversary_isPPT
+  have h : (fun n => (2 : ℝ≥0) ^ n / ((2 ^ (2 * n) : ℕ) : ℝ≥0)) =
+      fun n => (1 / (2 ^ n : ℕ) : ℝ≥0) := by
+    funext n
+    push_cast
+    rw [two_mul, pow_add, div_mul_eq_div_div, div_self (by positivity)]
+  rw [h]
+  exact negligible_inv_two_pow
+
+/-- Negative-side symmetric cipher for Theorem 11.5: `identitySym` ignores the derived symmetric
+key `k` and outputs the message `m` in the clear. -/
+noncomputable def identitySym (_ : ℕ) (_ m : List Bool) : ProbComp (List Bool) :=
+  pure m
+
+/-- A uniform strict-PPT IND-CPA adversary that submits `([false], [true])` (equal length `1`) and
+returns the first bit of the symmetric ciphertext `dropFrame ct`. -/
+noncomputable def firstBitCipherAdversary : Encryption.WordAdversary where
+  choose _ _ := pure (([false], [true]), [])
+  guess _ _ ct := pure ((dropFrame ct).headD false)
+
+/-- `firstBitCipherAdversary` is uniform strict PPT. -/
+theorem firstBitCipherAdversary_isPPT : firstBitCipherAdversary.IsPPT where
+  choose := (ComputableInPolyTime.const _).isPPTOn
+  guess := by
+    have hdrop : ComputableInPolyTime dropFrame encBits encBits :=
+      ComputableInPolyTime.dropFrame
+    have hhead : ComputableInPolyTime (fun s : List Bool => s.headD false) encBits encBool :=
+      by fun_prop
+    have hct : ComputableInPolyTime
+        (fun p : ℕ × List Bool × List Bool => (dropFrame p.2.2).headD false)
+        (encPair encUnary (encPair encBits encBits)) encBool :=
+      hhead.comp (hdrop.comp (by fun_prop))
+    exact hct.isPPTOn
+
+/-- Negative-side test for Theorem 11.5: when the symmetric cipher `identitySym` is not
+semantically secure, `firstBitCipherAdversary` wins `hashedElGamalCipherCPAGameOn
+equalLengthWords` with advantage `1` at every security parameter `n` regardless of the KDF `H`. -/
+theorem advantage_hashedElGamalCipherCPAGameOn_identitySym
+    (H : schnorrGroups.Desc × List Bool → List Bool) (n : ℕ) :
+    Game.advantage
+      (schnorrGroups.hashedElGamalCipherCPAGameOn equalLengthWords
+        (fun _ => PMF.pure d23) H identitySym firstBitCipherAdversary false n)
+      (schnorrGroups.hashedElGamalCipherCPAGameOn equalLengthWords
+        (fun _ => PMF.pure d23) H identitySym firstBitCipherAdversary true n) = 1 := by
+  have hval : ∀ pk, equalLengthWords n pk [false] [true] = true := fun _ => rfl
+  have h0 :
+      schnorrGroups.hashedElGamalCipherCPAGameOn equalLengthWords
+        (fun _ => PMF.pure d23) H identitySym firstBitCipherAdversary false n =
+        PMF.pure false := by
+    simp [PrimeOrderGroupFamily.hashedElGamalCipherCPAGameOn, identitySym,
+      firstBitCipherAdversary, hval]
+  have h1 :
+      schnorrGroups.hashedElGamalCipherCPAGameOn equalLengthWords
+        (fun _ => PMF.pure d23) H identitySym firstBitCipherAdversary true n =
+        PMF.pure true := by
+    simp [PrimeOrderGroupFamily.hashedElGamalCipherCPAGameOn, identitySym,
+      firstBitCipherAdversary, hval]
+  rw [h0, h1, Game.advantage, Game.succProbability, Game.succProbability]
+  simp
+
 end ComplexityTests.Crypto.DiffieHellman

ComplexityTests/Crypto/GameBounds.lean

@@ -59,4 +59,46 @@ example {α β : Type*} (p : PMF α) (q : PMF β) (f g : α → β → Game) :
       (q.bind fun b => p.bind fun a => g a b) :=
   Game.advantage_bind_comm p q f g
 
+open Cslib.Probability in
+-- Concrete check of `succProbability_uniform_bool_xor`: when `g false = PMF.pure true` and
+-- `g true = PMF.pure false`, `guess ^^ bit` is always `true`, so the success probability is `1`.
+example :
+    (Game.succProbability
+      ((PMF.uniformOfFintype Bool).bind fun bit =>
+        ((if bit then PMF.pure false else PMF.pure true : Game)).map
+          (fun guess => guess ^^ bit)) : ℝ) = 1 := by
+  rw [Game.succProbability_uniform_bool_xor]
+  simp [Game.succProbability]
+
+open Cslib.Probability in
+-- Concrete application of `advantage_le_two_mul_uniform_bool_xor` on `g₀ bit = PMF.pure (!bit)` and
+-- `g₁ _ = PMF.pure false` (where the inequality holds with equality `1 ≤ 2 * (1 / 2) + 0`).
+example :
+    let g₀ : Bool → Game := fun bit => PMF.pure (!bit)
+    let g₁ : Bool → Game := fun _ => PMF.pure false
+    Game.advantage (g₀ false) (g₀ true) ≤
+      2 * Game.advantage
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₀ bit).map (fun guess => guess ^^ bit))
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₁ bit).map (fun guess => guess ^^ bit)) +
+      Game.advantage (g₁ false) (g₁ true) :=
+  Game.advantage_le_two_mul_uniform_bool_xor (fun bit => PMF.pure (!bit)) (fun _ => PMF.pure false)
+
+open Cslib.Probability in
+-- Tightness / refutation test: the factor `2` in `advantage_le_two_mul_uniform_bool_xor` cannot be
+-- replaced by `1`. For `g₀ bit = PMF.pure (!bit)` and `g₁ _ = PMF.pure false`, the game gap of `g₀`
+-- is `1`, the game gap of `g₁` is `0`, and the hidden-bit XOR mixture advantage is `1 / 2`.
+example :
+    let g₀ : Bool → Game := fun bit => PMF.pure (!bit)
+    let g₁ : Bool → Game := fun _ => PMF.pure false
+    ¬ (Game.advantage (g₀ false) (g₀ true) ≤
+      1 * Game.advantage
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₀ bit).map (fun guess => guess ^^ bit))
+        ((PMF.uniformOfFintype Bool).bind fun bit => (g₁ bit).map (fun guess => guess ^^ bit)) +
+      Game.advantage (g₁ false) (g₁ true)) := by
+  dsimp only
+  rw [← NNReal.coe_le_coe]
+  simp only [NNReal.coe_add, NNReal.coe_mul, NNReal.coe_one, Game.coe_advantage,
+    Game.succProbability_uniform_bool_xor, Game.succProbability]
+  norm_num
+
 end ComplexityTests.GameBounds

ROADMAP.md

@@ -120,8 +120,10 @@ families and full-input native runtime.
 - **Sigma protocols and Fiat–Shamir** ([#581]): computational Schnorr signatures under discrete
   log against strict PPT forgers; eavesdropping security in the strict-PPT model, with the
   statistical-distance term from sampling `ZMod q`.
-- **Diffie–Hellman and ElGamal:** Hashed ElGamal with a general semantically secure symmetric
-  cipher `E_s` (Boneh–Shoup Theorem 11.5) ([#1047]).
+- **Diffie–Hellman and ElGamal:** arbitrary-key-length standalone symmetric-cipher bridge for
+  general-cipher Hashed ElGamal (Boneh–Shoup Theorem 11.5; the general-cipher construction,
+  Game 0/1/2 hybrids, Equation `(11.14)` reductions, and normalized `n`-bit-key `DEMOneTimeINDCPAOn`
+  / `linearHashKDF` endpoints have landed) ([#1047]).
 - **Chosen-ciphertext security** ([#1000]): authenticated encryption by encrypt-then-MAC and
   Cramer–Shoup from DDH, with KEM–DEM hybrid encryption ([#881]) as the chosen-plaintext
   starting point (Boneh–Shoup Exercise 11.9).