diff --git a/Complexity/Crypto/Computational/ElGamal/GeneralCipher.lean b/Complexity/Crypto/Computational/ElGamal/GeneralCipher.lean
index 5cc924c5d8..3421919871 100644
--- a/Complexity/Crypto/Computational/ElGamal/GeneralCipher.lean
+++ b/Complexity/Crypto/Computational/ElGamal/GeneralCipher.lean
@@ -66,8 +66,9 @@ $\mathcal{E}_s$.
   `Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherToKDFHiddenBitDistinguisher`,
   `Cslib.Crypto.PrimeOrderGroupFamily.hashedElGamalCipherToDEMAdversary`,
   `Cslib.Crypto.PrimeOrderGroupFamily.seededSetupProb`: per-bit and hidden-bit DDH and KDF
-  reductions, symmetric-cipher (`DEMOneTimeINDCPAOn`) reduction adversary, and executable seeded
-  setup sampler for Theorem 11.5 ([BonehShoup2023], Section 11.5.2, pp. 449–451).
+  reductions, symmetric-cipher (`DEMOneTimeKeyINDCPAOn` / `DEMOneTimeINDCPAOn`) reduction adversary,
+  and executable seeded setup sampler for Theorem 11.5 ([BonehShoup2023], Section 11.5.2,
+  pp. 449–451).
 
 ## Main results
 
@@ -76,18 +77,26 @@ $\mathcal{E}_s$.
   decryption correctness for general-cipher Hashed ElGamal.
 * `Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le`,
   `Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le_two_mul`,
-  `Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherUniformKeyGameOn_le_demGameOn`,
-  `Cslib.Crypto.PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le_demGameOn`:
+  `PrimeOrderGroupFamily.advantage_hashedElGamalCipherUniformKeyGameOn_le_demKeyGameOn`,
+  `PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le_demKeyGameOn`,
+  `PrimeOrderGroupFamily.advantage_hashedElGamalCipherUniformKeyGameOn_le_demGameOn`,
+  `PrimeOrderGroupFamily.advantage_hashedElGamalCipherCPAGameOn_le_demGameOn`:
   two-distinguisher and single hidden-bit distinguisher quantitative bounds for Theorem 11.5
   (matching Equation `(11.14)` of [BonehShoup2023], p. 449), together with the native
   approximate-sampling (`sampleExp`, adding `4 / 2 ^ n`) bridge to standalone
-  symmetric-cipher security (`Encryption.demGameOn`).
-* `Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCipherCPAGameOn` and its
-  `DEMOneTimeINDCPAOn` / `linearHashKDF` specializations
-  (`negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeINDCPAOn`,
-  `negligible_hashedElGamalCipherCPAGameOn_linearHashKDF`):
+  symmetric-cipher security at arbitrary (`Encryption.demKeyGameOn`) and normalized (`n`-bit,
+  `Encryption.demGameOn`) key lengths.
+* `Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCipherCPAGameOn`,
+  `PrimeOrderGroupFamily.negligible_hashedElGamalCipherUniformKeyGameOn_of_demOneTimeKeyINDCPAOn`,
+  `PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeKeyINDCPAOn`,
+  `DDH.negligible_hashedElGamalCipherCPAGameOn_linearHashKDF_of_demOneTimeKeyINDCPAOn`,
+  and their normalized `n`-bit-key specializations
+  (`PrimeOrderGroupFamily.negligible_hashedElGamalCipherUniformKeyGameOn_of_demOneTimeINDCPAOn`,
+  `PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeINDCPAOn`,
+  `PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCipherCPAGameOn_linearHashKDF`):
   Theorem 11.5 IND-CPA security in `hashedElGamalCipherCPAGameOn` from `DDH`, `SecureKDF`, and
-  `DEMOneTimeINDCPAOn`, plus unconditional KDF instantiation via `linearHashKDF`.
+  `DEMOneTimeKeyINDCPAOn` (or `DEMOneTimeINDCPAOn`), plus unconditional KDF instantiation via
+  `linearHashKDF` at arbitrary and normalized key lengths.
 
 ## References
 
@@ -1086,17 +1095,17 @@ theorem isPPT_hashedElGamalCipherToDEMAdversary {Msg : Type} {encMsg : Msg ↪ L
       ((F.isPPTOn_sampleExp hn2 hd2).bind_with
         (hchoose3.bind_with hret4.isPPTOn)))
 
-/-- For each bit `bit : Bool`, the Game 2 distribution `hashedElGamalCipherUniformKeyGameOn` over
-`fun m => ProbComp.eval (setupProb m)` with `keyLen n = n` is within `2 / 2 ^ n` in
-`Game.advantage` of the standalone one-time symmetric experiment `Encryption.demGameOn` on
-`hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)` (two approximate exponent
-draws via `sampleExp`, each within `1 / 2 ^ n` of uniform). -/
-theorem advantage_hashedElGamalCipherUniformKeyGameOn_demGameOn_le {Msg : Type}
+/-- For each bit `bit : Bool` and any key-length function `keyLen : ℕ → ℕ`, the Game 2 distribution
+`hashedElGamalCipherUniformKeyGameOn` over `fun m => ProbComp.eval (setupProb m)` is within
+`2 / 2 ^ n` in `Game.advantage` of the standalone one-time symmetric experiment
+`Encryption.demKeyGameOn` on the wrapper adversary
+`hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)`
+(two approximate exponent draws via `sampleExp`, each within `1 / 2 ^ n` of uniform). -/
+theorem advantage_hashedElGamalCipherUniformKeyGameOn_demKeyGameOn_le {Msg : Type}
     (valid validSym : ℕ → List Bool → Msg → Msg → Bool)
     (setupProb : ℕ → ProbComp F.Desc) (keyLen : ℕ → ℕ)
     (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
     (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ)
-    (hkeyLen : keyLen n = n)
     (hvalid_imp : ∀ d u m₀ m₁,
       valid n (encPair F.encDesc encBits (d, u)) m₀ m₁ = true →
         validSym n [] m₀ m₁ = true) :
@@ -1104,14 +1113,14 @@ theorem advantage_hashedElGamalCipherUniformKeyGameOn_demGameOn_le {Msg : Type}
       (F.hashedElGamalCipherUniformKeyGameOn valid (fun m => ProbComp.eval (setupProb m))
         keyLen encryptSym adversary bit n)
       (ProbComp.eval
-        (Encryption.demGameOn validSym encryptSym
+        (Encryption.demKeyGameOn validSym keyLen encryptSym
           (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) bit n)) ≤
       2 / 2 ^ n := by
   let k (d : F.Desc) (α β : ZMod (F.order d)) : Game :=
     let pk := encPair F.encDesc encBits (d, F.encode d (α • F.generator d))
     (ProbComp.eval (adversary.choose n pk)).bind fun choice =>
       if valid n pk choice.1.1 choice.1.2 then
-        (Cslib.BitString.uniformList n).bind fun key =>
+        (Cslib.BitString.uniformList (keyLen n)).bind fun key =>
           (ProbComp.eval (encryptSym n key (if bit then choice.1.2 else choice.1.1))).bind fun c =>
             ProbComp.eval (adversary.guess n choice.2
               (encPair encBits encBits (F.encode d (β • F.generator d), c)))
@@ -1123,7 +1132,7 @@ theorem advantage_hashedElGamalCipherUniformKeyGameOn_demGameOn_le {Msg : Type}
       (ProbComp.eval (setupProb n)).bind fun d =>
         (PMF.uniformOfFintype (ZMod (F.order d))).bind fun α =>
           (PMF.uniformOfFintype (ZMod (F.order d))).bind fun β => k d α β := by
-    simp only [hashedElGamalCipherUniformKeyGameOn, hkeyLen, PMF.monad_bind_eq_bind,
+    simp only [hashedElGamalCipherUniformKeyGameOn, PMF.monad_bind_eq_bind,
       PMF.monad_pure_eq_pure, k]
     congr 1; funext d
     congr 1; funext α
@@ -1132,13 +1141,13 @@ theorem advantage_hashedElGamalCipherUniformKeyGameOn_demGameOn_le {Msg : Type}
     split_ifs <;> simp [PMF.bind_const]
   have hdem :
       ProbComp.eval
-        (Encryption.demGameOn validSym encryptSym
+        (Encryption.demKeyGameOn validSym keyLen encryptSym
           (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) bit n) =
       (ProbComp.eval (setupProb n)).bind fun d =>
         (ProbComp.eval (F.sampleExp n d)).bind fun a =>
           (ProbComp.eval (F.sampleExp n d)).bind fun b =>
             k d (a : ZMod (F.order d)) (b : ZMod (F.order d)) := by
-    simp only [Encryption.demGameOn, hashedElGamalCipherToDEMAdversary,
+    simp only [Encryption.demKeyGameOn, hashedElGamalCipherToDEMAdversary,
       Encryption.AdversaryOf.restrict, ProbComp.eval_bind, ProbComp.eval_pure,
       Cslib.BitString.eval_sampleList, apply_ite ProbComp.eval,
       PMF.bind_bind, PMF.pure_bind, encPair_apply, encBits_apply,
@@ -1176,16 +1185,40 @@ theorem advantage_hashedElGamalCipherUniformKeyGameOn_demGameOn_le {Msg : Type}
   calc _ ≤ (1 : ℝ≥0) / 2 ^ n + 1 / 2 ^ n := add_le_add h1 h2
     _ = 2 / 2 ^ n := by ring
 
+/-- For each bit `bit : Bool`, the Game 2 distribution `hashedElGamalCipherUniformKeyGameOn` over
+`fun m => ProbComp.eval (setupProb m)` with `keyLen n = n` is within `2 / 2 ^ n` in
+`Game.advantage` of the standalone one-time symmetric experiment `Encryption.demGameOn` on
+`hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)` (two approximate exponent
+draws via `sampleExp`, each within `1 / 2 ^ n` of uniform). -/
+theorem advantage_hashedElGamalCipherUniformKeyGameOn_demGameOn_le {Msg : Type}
+    (valid validSym : ℕ → List Bool → Msg → Msg → Bool)
+    (setupProb : ℕ → ProbComp F.Desc) (keyLen : ℕ → ℕ)
+    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
+    (adversary : Encryption.AdversaryOf Msg) (bit : Bool) (n : ℕ)
+    (hkeyLen : keyLen n = n)
+    (hvalid_imp : ∀ d u m₀ m₁,
+      valid n (encPair F.encDesc encBits (d, u)) m₀ m₁ = true →
+        validSym n [] m₀ m₁ = true) :
+    Game.advantage
+      (F.hashedElGamalCipherUniformKeyGameOn valid (fun m => ProbComp.eval (setupProb m))
+        keyLen encryptSym adversary bit n)
+      (ProbComp.eval
+        (Encryption.demGameOn validSym encryptSym
+          (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) bit n)) ≤
+      2 / 2 ^ n := by
+  rw [← Encryption.demKeyGameOn_eq_demGameOn_of_eq validSym keyLen encryptSym _ bit hkeyLen]
+  exact F.advantage_hashedElGamalCipherUniformKeyGameOn_demKeyGameOn_le
+    valid validSym setupProb keyLen encryptSym adversary bit n hvalid_imp
+
 /-- **Quantitative bridge from Game 2 (`hashedElGamalCipherUniformKeyGameOn`) to standalone
-symmetric-cipher security (`Encryption.demGameOn`)**: the Game 2 advantage is bounded by the
-`Encryption.demGameOn` advantage of
+symmetric-cipher security at arbitrary key length (`Encryption.demKeyGameOn`)**: for any
+`keyLen : ℕ → ℕ`, the Game 2 advantage is bounded by the `Encryption.demKeyGameOn` advantage of
 `hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)` plus `4 / 2 ^ n`. -/
-theorem advantage_hashedElGamalCipherUniformKeyGameOn_le_demGameOn {Msg : Type}
+theorem advantage_hashedElGamalCipherUniformKeyGameOn_le_demKeyGameOn {Msg : Type}
     (valid validSym : ℕ → List Bool → Msg → Msg → Bool)
     (setupProb : ℕ → ProbComp F.Desc) (keyLen : ℕ → ℕ)
     (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
     (adversary : Encryption.AdversaryOf Msg) (n : ℕ)
-    (hkeyLen : keyLen n = n)
     (hvalid_imp : ∀ d u m₀ m₁,
       valid n (encPair F.encDesc encBits (d, u)) m₀ m₁ = true →
         validSym n [] m₀ m₁ = true) :
@@ -1196,50 +1229,133 @@ theorem advantage_hashedElGamalCipherUniformKeyGameOn_le_demGameOn {Msg : Type}
         keyLen encryptSym adversary true n) ≤
       Game.advantage
         (ProbComp.eval
-          (Encryption.demGameOn validSym encryptSym
+          (Encryption.demKeyGameOn validSym keyLen encryptSym
             (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) false n))
         (ProbComp.eval
-          (Encryption.demGameOn validSym encryptSym
+          (Encryption.demKeyGameOn validSym keyLen encryptSym
             (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) true n)) +
       4 / 2 ^ n := by
-  have hf := F.advantage_hashedElGamalCipherUniformKeyGameOn_demGameOn_le
-    valid validSym setupProb keyLen encryptSym adversary false n hkeyLen hvalid_imp
-  have ht := F.advantage_hashedElGamalCipherUniformKeyGameOn_demGameOn_le
-    valid validSym setupProb keyLen encryptSym adversary true n hkeyLen hvalid_imp
+  have hf := F.advantage_hashedElGamalCipherUniformKeyGameOn_demKeyGameOn_le
+    valid validSym setupProb keyLen encryptSym adversary false n hvalid_imp
+  have ht := F.advantage_hashedElGamalCipherUniformKeyGameOn_demKeyGameOn_le
+    valid validSym setupProb keyLen encryptSym adversary true n hvalid_imp
   have htri1 := Game.advantage_triangle
     (F.hashedElGamalCipherUniformKeyGameOn valid (fun m => ProbComp.eval (setupProb m))
       keyLen encryptSym adversary false n)
     (ProbComp.eval
-      (Encryption.demGameOn validSym encryptSym
+      (Encryption.demKeyGameOn validSym keyLen encryptSym
         (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) false n))
     (F.hashedElGamalCipherUniformKeyGameOn valid (fun m => ProbComp.eval (setupProb m))
       keyLen encryptSym adversary true n)
   have htri2 := Game.advantage_triangle
     (ProbComp.eval
-      (Encryption.demGameOn validSym encryptSym
+      (Encryption.demKeyGameOn validSym keyLen encryptSym
         (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) false n))
     (ProbComp.eval
-      (Encryption.demGameOn validSym encryptSym
+      (Encryption.demKeyGameOn validSym keyLen encryptSym
         (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) true n))
     (F.hashedElGamalCipherUniformKeyGameOn valid (fun m => ProbComp.eval (setupProb m))
       keyLen encryptSym adversary true n)
   rw [Game.advantage_comm
     (ProbComp.eval
-      (Encryption.demGameOn validSym encryptSym
+      (Encryption.demKeyGameOn validSym keyLen encryptSym
         (F.hashedElGamalCipherToDEMAdversary setupProb
           (adversary.restrict valid)) true n))] at htri2
   have hcomb := htri1.trans (add_le_add hf (htri2.trans (add_le_add le_rfl ht)))
   calc _ ≤ (2 : ℝ≥0) / 2 ^ n +
         (Game.advantage
           (ProbComp.eval
-            (Encryption.demGameOn validSym encryptSym
+            (Encryption.demKeyGameOn validSym keyLen encryptSym
               (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) false n))
           (ProbComp.eval
-            (Encryption.demGameOn validSym encryptSym
+            (Encryption.demKeyGameOn validSym keyLen encryptSym
               (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) true n)) +
         2 / 2 ^ n) := hcomb
     _ = _ := by ring
 
+/-- **Quantitative bridge from Game 2 (`hashedElGamalCipherUniformKeyGameOn`) to standalone
+symmetric-cipher security (`Encryption.demGameOn`)**: the Game 2 advantage is bounded by the
+`Encryption.demGameOn` advantage of
+`hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)` plus `4 / 2 ^ n`. -/
+theorem advantage_hashedElGamalCipherUniformKeyGameOn_le_demGameOn {Msg : Type}
+    (valid validSym : ℕ → List Bool → Msg → Msg → Bool)
+    (setupProb : ℕ → ProbComp F.Desc) (keyLen : ℕ → ℕ)
+    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
+    (adversary : Encryption.AdversaryOf Msg) (n : ℕ)
+    (hkeyLen : keyLen n = n)
+    (hvalid_imp : ∀ d u m₀ m₁,
+      valid n (encPair F.encDesc encBits (d, u)) m₀ m₁ = true →
+        validSym n [] m₀ m₁ = true) :
+    Game.advantage
+      (F.hashedElGamalCipherUniformKeyGameOn valid (fun m => ProbComp.eval (setupProb m))
+        keyLen encryptSym adversary false n)
+      (F.hashedElGamalCipherUniformKeyGameOn valid (fun m => ProbComp.eval (setupProb m))
+        keyLen encryptSym adversary true n) ≤
+      Game.advantage
+        (ProbComp.eval
+          (Encryption.demGameOn validSym encryptSym
+            (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) false n))
+        (ProbComp.eval
+          (Encryption.demGameOn validSym encryptSym
+            (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) true n)) +
+      4 / 2 ^ n := by
+  rw [← Encryption.demKeyGameOn_eq_demGameOn_of_eq validSym keyLen encryptSym _ false hkeyLen,
+    ← Encryption.demKeyGameOn_eq_demGameOn_of_eq validSym keyLen encryptSym _ true hkeyLen]
+  exact F.advantage_hashedElGamalCipherUniformKeyGameOn_le_demKeyGameOn
+    valid validSym setupProb keyLen encryptSym adversary n hvalid_imp
+
+/-- **Native approximate-sampling version of Equation `(11.14)` for Theorem 11.5 via DDH,
+`SecureKDF`, and standalone symmetric-cipher security at arbitrary key length
+(`Encryption.demKeyGameOn`)** ([BonehShoup2023], Section 11.5.2, Theorem 11.5, Equation `(11.14)`,
+p. 449): combining the exact PMF-level Equation `(11.14)` bound
+`advantage_hashedElGamalCipherCPAGameOn_le_two_mul` with the `sampleExp` Game 2 bridge
+`advantage_hashedElGamalCipherUniformKeyGameOn_le_demKeyGameOn` adds `4 / 2 ^ n` for the two
+approximate exponent draws per branch:
+$$\mathsf{SSadv}[\mathcal{A}, \mathcal{E}_{\mathrm{EG}}] \le
+  2 \cdot \mathsf{DDHadv}[\mathcal{B}_{\mathrm{ddh}}, \mathbb{G}] +
+  2 \cdot \mathsf{KDFadv}[\mathcal{B}_{\mathrm{kdf}}, H] +
+  \mathsf{SSadv}[\mathcal{B}_s, \mathcal{E}_s] + \frac{4}{2^n}.$$ -/
+theorem advantage_hashedElGamalCipherCPAGameOn_le_demKeyGameOn {Msg : Type}
+    (valid validSym : ℕ → List Bool → Msg → Msg → Bool)
+    (setupProb : ℕ → ProbComp F.Desc) (H : F.Desc × List Bool → List Bool) (keyLen : ℕ → ℕ)
+    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
+    (adversary : Encryption.AdversaryOf Msg) (n : ℕ)
+    (hvalid_imp : ∀ d u m₀ m₁,
+      valid n (encPair F.encDesc encBits (d, u)) m₀ m₁ = true →
+        validSym n [] m₀ m₁ = true) :
+    Game.advantage
+      (F.hashedElGamalCipherCPAGameOn valid (fun m => ProbComp.eval (setupProb m))
+        H encryptSym adversary false n)
+      (F.hashedElGamalCipherCPAGameOn valid (fun m => ProbComp.eval (setupProb m))
+        H encryptSym adversary true n) ≤
+      2 * Game.advantage
+        (F.ddhRealGame (fun m => ProbComp.eval (setupProb m))
+          (F.hashedElGamalCipherToDDHHiddenBitDistinguisher H encryptSym
+            (adversary.restrict valid)) n)
+        (F.ddhIdealGame (fun m => ProbComp.eval (setupProb m))
+          (F.hashedElGamalCipherToDDHHiddenBitDistinguisher H encryptSym
+            (adversary.restrict valid)) n) +
+      2 * Game.advantage
+        (F.kdfRealGame (fun m => ProbComp.eval (setupProb m)) H
+          (F.hashedElGamalCipherToKDFHiddenBitDistinguisher encryptSym
+            (adversary.restrict valid)) n)
+        (F.kdfIdealGame (fun m => ProbComp.eval (setupProb m)) keyLen
+          (F.hashedElGamalCipherToKDFHiddenBitDistinguisher encryptSym
+            (adversary.restrict valid)) n) +
+      Game.advantage
+        (ProbComp.eval
+          (Encryption.demKeyGameOn validSym keyLen encryptSym
+            (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) false n))
+        (ProbComp.eval
+          (Encryption.demKeyGameOn validSym keyLen encryptSym
+            (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) true n)) +
+      4 / 2 ^ n := by
+  have h1 := F.advantage_hashedElGamalCipherCPAGameOn_le_two_mul
+    valid (fun m => ProbComp.eval (setupProb m)) H keyLen encryptSym adversary n
+  have h2 := F.advantage_hashedElGamalCipherUniformKeyGameOn_le_demKeyGameOn
+    valid validSym setupProb keyLen encryptSym adversary n hvalid_imp
+  exact (h1.trans (add_le_add le_rfl h2)).trans_eq (by ring)
+
 /-- **Native approximate-sampling version of Equation `(11.14)` for Theorem 11.5 via DDH,
 `SecureKDF`, and standalone symmetric-cipher security (`Encryption.demGameOn`)** ([BonehShoup2023],
 Section 11.5.2, Theorem 11.5, Equation `(11.14)`, p. 449): combining the exact PMF-level Equation
@@ -1286,23 +1402,22 @@ theorem advantage_hashedElGamalCipherCPAGameOn_le_demGameOn {Msg : Type}
           (Encryption.demGameOn validSym encryptSym
             (F.hashedElGamalCipherToDEMAdversary setupProb (adversary.restrict valid)) true n)) +
       4 / 2 ^ n := by
-  have h1 := F.advantage_hashedElGamalCipherCPAGameOn_le_two_mul
-    valid (fun m => ProbComp.eval (setupProb m)) H keyLen encryptSym adversary n
-  have h2 := F.advantage_hashedElGamalCipherUniformKeyGameOn_le_demGameOn
-    valid validSym setupProb keyLen encryptSym adversary n hkeyLen hvalid_imp
-  exact (h1.trans (add_le_add le_rfl h2)).trans_eq (by ring)
-
-/-- One-time symmetric IND-CPA security (`Encryption.DEMOneTimeINDCPAOn`) implies negligibility of
-the Game 2 advantage (`hashedElGamalCipherUniformKeyGameOn`) whenever the setup law is efficiently
-samplable (`setupProb : ℕ → ProbComp F.Desc`), `keyLen n = n`, and `valid` implies `validSym`. -/
-theorem negligible_hashedElGamalCipherUniformKeyGameOn_of_demOneTimeINDCPAOn {Msg : Type}
+  rw [← Encryption.demKeyGameOn_eq_demGameOn_of_eq validSym keyLen encryptSym _ false hkeyLen,
+    ← Encryption.demKeyGameOn_eq_demGameOn_of_eq validSym keyLen encryptSym _ true hkeyLen]
+  exact F.advantage_hashedElGamalCipherCPAGameOn_le_demKeyGameOn
+    valid validSym setupProb H keyLen encryptSym adversary n hvalid_imp
+
+/-- One-time symmetric IND-CPA security at arbitrary key length (`Encryption.DEMOneTimeKeyINDCPAOn`)
+implies negligibility of the Game 2 advantage (`hashedElGamalCipherUniformKeyGameOn`) whenever the
+setup law is efficiently samplable (`setupProb : ℕ → ProbComp F.Desc`) and `valid` implies
+`validSym`. -/
+theorem negligible_hashedElGamalCipherUniformKeyGameOn_of_demOneTimeKeyINDCPAOn {Msg : Type}
     {encMsg : Msg ↪ List Bool}
     {valid validSym : ℕ → List Bool → Msg → Msg → Bool}
     {setupProb : ℕ → ProbComp F.Desc} {keyLen : ℕ → ℕ}
     {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
-    (hDEM : Encryption.DEMOneTimeINDCPAOn validSym encMsg encryptSym)
+    (hDEM : Encryption.DEMOneTimeKeyINDCPAOn validSym encMsg keyLen encryptSym)
     (hsetup : IsPPTOn encUnary F.encDesc setupProb)
-    (hkeyLen : ∀ n, keyLen n = n)
     (hvalid : ComputableInPolyTime
       (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2)
       (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool)
@@ -1325,8 +1440,73 @@ theorem negligible_hashedElGamalCipherUniformKeyGameOn_of_demOneTimeINDCPAOn {Ms
       (negligible_geometric (ratio := 2⁻¹) (by norm_num)).polynomiallyBounded_mul
         (p := fun _ => 4) (by fun_prop)
   exact negligible_of_le (hdem.add herr) fun n =>
-    F.advantage_hashedElGamalCipherUniformKeyGameOn_le_demGameOn
-      valid validSym setupProb keyLen encryptSym adversary n (hkeyLen n) (hvalid_imp n)
+    F.advantage_hashedElGamalCipherUniformKeyGameOn_le_demKeyGameOn
+      valid validSym setupProb keyLen encryptSym adversary n (hvalid_imp n)
+
+/-- One-time symmetric IND-CPA security (`Encryption.DEMOneTimeINDCPAOn`) implies negligibility of
+the Game 2 advantage (`hashedElGamalCipherUniformKeyGameOn`) whenever the setup law is efficiently
+samplable (`setupProb : ℕ → ProbComp F.Desc`), `keyLen n = n`, and `valid` implies `validSym`. -/
+theorem negligible_hashedElGamalCipherUniformKeyGameOn_of_demOneTimeINDCPAOn {Msg : Type}
+    {encMsg : Msg ↪ List Bool}
+    {valid validSym : ℕ → List Bool → Msg → Msg → Bool}
+    {setupProb : ℕ → ProbComp F.Desc} {keyLen : ℕ → ℕ}
+    {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
+    (hDEM : Encryption.DEMOneTimeINDCPAOn validSym encMsg encryptSym)
+    (hsetup : IsPPTOn encUnary F.encDesc setupProb)
+    (hkeyLen : ∀ n, keyLen n = n)
+    (hvalid : ComputableInPolyTime
+      (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2)
+      (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool)
+    (hvalid_imp : ∀ n d u m₀ m₁,
+      valid n (encPair F.encDesc encBits (d, u)) m₀ m₁ = true →
+        validSym n [] m₀ m₁ = true)
+    {adversary : Encryption.AdversaryOf Msg}
+    (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) :
+    Negligible fun n =>
+      Game.advantage
+        (F.hashedElGamalCipherUniformKeyGameOn valid (fun m => ProbComp.eval (setupProb m))
+          keyLen encryptSym adversary false n)
+        (F.hashedElGamalCipherUniformKeyGameOn valid (fun m => ProbComp.eval (setupProb m))
+          keyLen encryptSym adversary true n) :=
+  F.negligible_hashedElGamalCipherUniformKeyGameOn_of_demOneTimeKeyINDCPAOn
+    (hDEM.demOneTimeKeyINDCPAOn hkeyLen) hsetup hvalid hvalid_imp hA
+
+/-- **Boneh–Shoup Theorem 11.5 from DDH, `SecureKDF`, and `Encryption.DEMOneTimeKeyINDCPAOn` at
+arbitrary key length** ([BonehShoup2023], Section 11.5.2, Theorem 11.5, pp. 449–451): for any
+efficiently samplable setup `setupProb : ℕ → ProbComp F.Desc`
+(`setup n = ProbComp.eval (setupProb n)`), key-length function `keyLen : ℕ → ℕ`, and admissibility
+predicate `valid` implying `validSym`, if `F.DDH`, `F.SecureKDF`, and
+`Encryption.DEMOneTimeKeyINDCPAOn validSym encMsg keyLen encryptSym` hold, then every uniform strict
+PPT adversary has negligible advantage in `hashedElGamalCipherCPAGameOn valid`. -/
+theorem DDH.negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeKeyINDCPAOn
+    {F : PrimeOrderGroupFamily} {Msg : Type} {encMsg : Msg ↪ List Bool}
+    {valid validSym : ℕ → List Bool → Msg → Msg → Bool}
+    {setupProb : ℕ → ProbComp F.Desc} {H : F.Desc × List Bool → List Bool} {keyLen : ℕ → ℕ}
+    {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
+    (hDDH : F.DDH (fun n => ProbComp.eval (setupProb n)))
+    (hKDF : F.SecureKDF (fun n => ProbComp.eval (setupProb n)) H keyLen)
+    (hDEM : Encryption.DEMOneTimeKeyINDCPAOn validSym encMsg keyLen encryptSym)
+    (hsetup : IsPPTOn encUnary F.encDesc setupProb)
+    (hvalid : ComputableInPolyTime
+      (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2)
+      (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool)
+    (hvalid_imp : ∀ n d u m₀ m₁,
+      valid n (encPair F.encDesc encBits (d, u)) m₀ m₁ = true →
+        validSym n [] m₀ m₁ = true)
+    (hH : ComputableInPolyTime H (encPair F.encDesc encBits) encBits)
+    (hencryptSym : IsPPTOn (encPair encUnary (encPair encBits encMsg)) encBits
+      (fun p => encryptSym p.1 p.2.1 p.2.2))
+    {adversary : Encryption.AdversaryOf Msg}
+    (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) :
+    Negligible fun n =>
+      Game.advantage
+        (F.hashedElGamalCipherCPAGameOn valid (fun n => ProbComp.eval (setupProb n))
+          H encryptSym adversary false n)
+        (F.hashedElGamalCipherCPAGameOn valid (fun n => ProbComp.eval (setupProb n))
+          H encryptSym adversary true n) :=
+  hDDH.negligible_hashedElGamalCipherCPAGameOn hKDF hvalid hH hencryptSym hA
+    (F.negligible_hashedElGamalCipherUniformKeyGameOn_of_demOneTimeKeyINDCPAOn
+      hDEM hsetup hvalid hvalid_imp hA)
 
 /-- **Boneh–Shoup Theorem 11.5 from DDH, `SecureKDF`, and `Encryption.DEMOneTimeINDCPAOn`**
 ([BonehShoup2023], Section 11.5.2, Theorem 11.5, pp. 449–451): for any efficiently samplable setup
@@ -1361,9 +1541,8 @@ theorem DDH.negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeINDCPAOn
           H encryptSym adversary false n)
         (F.hashedElGamalCipherCPAGameOn valid (fun n => ProbComp.eval (setupProb n))
           H encryptSym adversary true n) :=
-  hDDH.negligible_hashedElGamalCipherCPAGameOn hKDF hvalid hH hencryptSym hA
-    (F.negligible_hashedElGamalCipherUniformKeyGameOn_of_demOneTimeINDCPAOn
-      hDEM hsetup hkeyLen hvalid hvalid_imp hA)
+  hDDH.negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeKeyINDCPAOn
+    hKDF (hDEM.demOneTimeKeyINDCPAOn hkeyLen) hsetup hvalid hvalid_imp hH hencryptSym hA
 
 /-- Executable `ProbComp` sampler for `F.seededSetup`: sample `d ← setupProb n`, then conditional on
 `d`, sample a uniform seed `s ← Cslib.BitString.sampleList (seedLen n d)` and output `(d, s)`. -/
@@ -1403,6 +1582,70 @@ theorem isPPTOn_seededSetupProb {setupProb : ℕ → ProbComp F.Desc}
   unfold seededSetupProb
   exact hsetup.bind_with (hsample.bind_with hret.isPPTOn)
 
+/-- **General-cipher Hashed ElGamal IND-CPA security with `linearHashKDF` at arbitrary key length
+`outLen : ℕ → ℕ` from `DDH` and `Encryption.DEMOneTimeKeyINDCPAOn` alone** ([BonehShoup2023],
+Section 8.10.4, Theorem 8.11, p. 334, and Section 11.5.2, Theorem 11.5, pp. 449–451): combining
+`DDH.withSeed`, `secureKDF_linearHashKDF`, `isPPTOn_seededSetupProb`, and
+`DDH.negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeKeyINDCPAOn` yields IND-CPA security of
+general-cipher Hashed ElGamal instantiated with `linearHashKDF` at any polynomial-time key length
+`outLen` under `F.DDH` and `Encryption.DEMOneTimeKeyINDCPAOn` alone, with no separate KDF
+assumption. -/
+theorem DDH.negligible_hashedElGamalCipherCPAGameOn_linearHashKDF_of_demOneTimeKeyINDCPAOn
+    {F : PrimeOrderGroupFamily} {Msg : Type} {encMsg : Msg ↪ List Bool}
+    {valid validSym : ℕ → List Bool → Msg → Msg → Bool}
+    {setupProb : ℕ → ProbComp F.Desc} {keyLen bound : F.Desc → ℕ} {outLen qMin : ℕ → ℕ}
+    {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
+    (hDDH : F.DDH (fun n => ProbComp.eval (setupProb n)))
+    (hDEM : Encryption.DEMOneTimeKeyINDCPAOn validSym encMsg outLen encryptSym)
+    (hsetup : IsPPTOn encUnary F.encDesc setupProb)
+    (hout_poly : ComputableInPolyTime outLen encUnary encUnary)
+    (hkey_poly : ComputableInPolyTime keyLen F.encDesc encUnary)
+    (hbound_poly : ComputableInPolyTime bound F.encDesc encUnary)
+    (hq0 : ∀ n, 0 < qMin n)
+    (hkey : ∀ n, ∀ d ∈ (ProbComp.eval (setupProb n)).support, keyLen d = outLen n)
+    (hbound : ∀ n, ∀ d ∈ (ProbComp.eval (setupProb n)).support,
+      ∀ x : F.Carrier d, (F.encode d x).length ≤ bound d)
+    (hq : ∀ n, ∀ d ∈ (ProbComp.eval (setupProb n)).support, qMin n ≤ F.order d)
+    (hneg : Negligible fun n => (2 : ℝ≥0) ^ (outLen n) / (qMin n : ℝ≥0))
+    (hvalid : ComputableInPolyTime
+      (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2)
+      (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool)
+    (hvalid_imp : ∀ n d u m₀ m₁,
+      valid n (encPair F.withSeed.encDesc encBits (d, u)) m₀ m₁ = true →
+        validSym n [] m₀ m₁ = true)
+    (hencryptSym : IsPPTOn (encPair encUnary (encPair encBits encMsg)) encBits
+      (fun p => encryptSym p.1 p.2.1 p.2.2))
+    {adversary : Encryption.AdversaryOf Msg}
+    (hA : Encryption.AdversaryOf.IsPPT encMsg adversary) :
+    Negligible fun n =>
+      Game.advantage
+        (F.withSeed.hashedElGamalCipherCPAGameOn valid
+          (F.seededSetup (fun m => ProbComp.eval (setupProb m))
+            (F.linearHashSeedLen outLen bound))
+          (F.linearHashKDF keyLen bound) encryptSym adversary false n)
+        (F.withSeed.hashedElGamalCipherCPAGameOn valid
+          (F.seededSetup (fun m => ProbComp.eval (setupProb m))
+            (F.linearHashSeedLen outLen bound))
+          (F.linearHashKDF keyLen bound) encryptSym adversary true n) := by
+  have hseed_poly := F.computableInPolyTime_linearHashSeedLen hout_poly hbound_poly
+  have hsetup_seeded := F.isPPTOn_seededSetupProb hsetup hseed_poly
+  have hDDH_seeded :
+      F.withSeed.DDH (fun n => ProbComp.eval (F.seededSetupProb setupProb
+        (F.linearHashSeedLen outLen bound) n)) := by
+    simp only [F.eval_seededSetupProb]
+    exact hDDH.withSeed hseed_poly
+  have hKDF_seeded :
+      F.withSeed.SecureKDF (fun n => ProbComp.eval (F.seededSetupProb setupProb
+        (F.linearHashSeedLen outLen bound) n))
+        (F.linearHashKDF keyLen bound) outLen := by
+    simp only [F.eval_seededSetupProb]
+    exact F.secureKDF_linearHashKDF (fun m => ProbComp.eval (setupProb m))
+      keyLen bound outLen hq0 hkey hbound hq hneg
+  simpa only [F.eval_seededSetupProb] using
+    hDDH_seeded.negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeKeyINDCPAOn
+      hKDF_seeded hDEM hsetup_seeded hvalid hvalid_imp
+      (F.computableInPolyTime_linearHashKDF hkey_poly hbound_poly) hencryptSym hA
+
 /-- **General-cipher Hashed ElGamal IND-CPA security with `linearHashKDF` from `DDH` and
 `Encryption.DEMOneTimeINDCPAOn` alone** ([BonehShoup2023], Section 8.10.4, Theorem 8.11, p. 334, and
 Section 11.5.2, Theorem 11.5, pp. 449–451): combining `DDH.withSeed`, `secureKDF_linearHashKDF`,
@@ -1444,24 +1687,9 @@ theorem DDH.negligible_hashedElGamalCipherCPAGameOn_linearHashKDF {F : PrimeOrde
         (F.withSeed.hashedElGamalCipherCPAGameOn valid
           (F.seededSetup (fun m => ProbComp.eval (setupProb m))
             (F.linearHashSeedLen (fun n => n) bound))
-          (F.linearHashKDF keyLen bound) encryptSym adversary true n) := by
-  have hseed_poly := F.computableInPolyTime_linearHashSeedLen ComputableInPolyTime.id' hbound_poly
-  have hsetup_seeded := F.isPPTOn_seededSetupProb hsetup hseed_poly
-  have hDDH_seeded :
-      F.withSeed.DDH (fun n => ProbComp.eval (F.seededSetupProb setupProb
-        (F.linearHashSeedLen (fun n => n) bound) n)) := by
-    simp only [F.eval_seededSetupProb]
-    exact hDDH.withSeed hseed_poly
-  have hKDF_seeded :
-      F.withSeed.SecureKDF (fun n => ProbComp.eval (F.seededSetupProb setupProb
-        (F.linearHashSeedLen (fun n => n) bound) n))
-        (F.linearHashKDF keyLen bound) (fun n => n) := by
-    simp only [F.eval_seededSetupProb]
-    exact F.secureKDF_linearHashKDF (fun m => ProbComp.eval (setupProb m))
-      keyLen bound (fun n => n) hq0 hkey hbound hq hneg
-  simpa only [F.eval_seededSetupProb] using
-    hDDH_seeded.negligible_hashedElGamalCipherCPAGameOn_of_demOneTimeINDCPAOn
-      hKDF_seeded hDEM hsetup_seeded (fun _ => rfl) hvalid hvalid_imp
-      (F.computableInPolyTime_linearHashKDF hkey_poly hbound_poly) hencryptSym hA
+          (F.linearHashKDF keyLen bound) encryptSym adversary true n) :=
+  hDDH.negligible_hashedElGamalCipherCPAGameOn_linearHashKDF_of_demOneTimeKeyINDCPAOn
+    hDEM hsetup ComputableInPolyTime.id' hkey_poly hbound_poly hq0 hkey hbound hq hneg
+    hvalid hvalid_imp hencryptSym hA
 
 end Cslib.Crypto.PrimeOrderGroupFamily
diff --git a/Complexity/Crypto/Computational/Encryption/Hybrid.lean b/Complexity/Crypto/Computational/Encryption/Hybrid.lean
index 9824865fcd..d464655788 100644
--- a/Complexity/Crypto/Computational/Encryption/Hybrid.lean
+++ b/Complexity/Crypto/Computational/Encryption/Hybrid.lean
@@ -75,10 +75,15 @@ representation conventions:
 * `Cslib.Crypto.Encryption.kemRealGame`, `Cslib.Crypto.Encryption.kemIdealGame`,
   `Cslib.Crypto.Encryption.KEMINDCPA`: real and ideal KEM IND-CPA experiments and security.
 * `Cslib.Crypto.Encryption.demGameOn`, `Cslib.Crypto.Encryption.demGame`,
+  `Cslib.Crypto.Encryption.demKeyGameOn`, `Cslib.Crypto.Encryption.demKeyGame`,
   `Cslib.Crypto.Encryption.DEMOneTimeINDCPAOn`, `Cslib.Crypto.Encryption.DEMOneTimeINDCPAOf`,
   `Cslib.Crypto.Encryption.DEMOneTimeINDCPA`,
-  `Cslib.Crypto.Encryption.DEMOneTimeWordINDCPA`: one-time symmetric encryption experiments and
-  security, with and without an admissibility predicate.
+  `Cslib.Crypto.Encryption.DEMOneTimeWordINDCPA`,
+  `Cslib.Crypto.Encryption.DEMOneTimeKeyINDCPAOn`, `Cslib.Crypto.Encryption.DEMOneTimeKeyINDCPAOf`,
+  `Cslib.Crypto.Encryption.DEMOneTimeKeyINDCPA`,
+  `Cslib.Crypto.Encryption.DEMOneTimeKeyWordINDCPA`: one-time symmetric encryption experiments and
+  security at normalized (`n`-bit) and arbitrary (`keyLen n`-bit) key lengths, with and without an
+  admissibility predicate.
 * `Cslib.Crypto.Encryption.hybridEncrypt`, `Cslib.Crypto.Encryption.hybridDecrypt`: KEM–DEM
   hybrid encryption and deterministic decryption.
 * `Cslib.Crypto.Encryption.hybridIdealGame`: intermediate game replacing the encapsulated key
@@ -87,8 +92,9 @@ representation conventions:
   `Cslib.Crypto.Encryption.hybridToKEMHiddenBitDistinguisher`,
   `Cslib.Crypto.Encryption.hybridToDEMAdversary`: the certified uniform reductions.
 * `Cslib.Crypto.Encryption.otpEncrypt`, `Cslib.Crypto.Encryption.otpDecrypt`,
-  `Cslib.Crypto.Encryption.otpWordEncrypt`, `Cslib.Crypto.Encryption.otpWordDecrypt`: one-time pad
-  single-bit and `n`-bit word DEMs.
+  `Cslib.Crypto.Encryption.otpWordEncrypt`, `Cslib.Crypto.Encryption.otpWordDecrypt`,
+  `Cslib.Crypto.Encryption.otpKeyWordEncrypt`, `Cslib.Crypto.Encryption.otpKeyWordDecrypt`:
+  one-time pad single-bit, `n`-bit word, and `keyLen n`-bit word DEMs.
 
 ## Main results
 
@@ -96,6 +102,8 @@ representation conventions:
   `Cslib.Crypto.Encryption.isPPTOn_kemIdealGame`,
   `Cslib.Crypto.Encryption.isPPTOn_demGameOn`,
   `Cslib.Crypto.Encryption.isPPTOn_demGame`,
+  `Cslib.Crypto.Encryption.isPPTOn_demKeyGameOn`,
+  `Cslib.Crypto.Encryption.isPPTOn_demKeyGame`,
   `Cslib.Crypto.Encryption.isPPTOn_hybridEncrypt`,
   `Cslib.Crypto.Encryption.computableInPolyTime_hybridDecrypt`: polynomial-time certificates.
 * `Cslib.Crypto.Encryption.hybridDecrypt_encPair`,
@@ -105,8 +113,10 @@ representation conventions:
   `Cslib.Crypto.Encryption.advantage_hybridGame_le`: quantitative Boneh–Shoup Exercise 11.9(b)
   reduction and its two-distinguisher variant.
 * `Cslib.Crypto.Encryption.eval_demGame_restrict`,
-  `Cslib.Crypto.Encryption.DEMOneTimeINDCPAOf.demOneTimeINDCPAOn`: unrestricted one-time security
-  implies one-time security under every polynomial-time admissibility predicate.
+  `Cslib.Crypto.Encryption.eval_demKeyGame_restrict`,
+  `Cslib.Crypto.Encryption.DEMOneTimeINDCPAOf.demOneTimeINDCPAOn`,
+  `Cslib.Crypto.Encryption.DEMOneTimeKeyINDCPAOf.demOneTimeKeyINDCPAOn`: unrestricted one-time
+  security implies one-time security under every polynomial-time admissibility predicate.
 * `Cslib.Crypto.Encryption.KEMINDCPA.hybrid_indcpa`,
   `Cslib.Crypto.Encryption.KEMINDCPA.hybrid_indcpaOn`: asymptotic Boneh–Shoup Exercise 11.9(b),
   without and with an admissibility predicate.
@@ -114,6 +124,8 @@ representation conventions:
   `Cslib.Crypto.Encryption.KEMINDCPA.hybrid_otpEncrypt_indcpa`,
   `Cslib.Crypto.Encryption.demOneTimeINDCPA_otpWordEncrypt`,
   `Cslib.Crypto.Encryption.demOneTimeWordINDCPA_otpWordEncrypt`,
+  `Cslib.Crypto.Encryption.demOneTimeKeyINDCPA_otpKeyWordEncrypt`,
+  `Cslib.Crypto.Encryption.demOneTimeKeyWordINDCPA_otpKeyWordEncrypt`,
   `Cslib.Crypto.Encryption.KEMINDCPA.hybrid_otpWordEncrypt_indcpa`: unconditional one-time pad DEM
   security and the KEM-to-PKE corollaries.
 
@@ -244,15 +256,16 @@ def KEMINDCPA (keyGen : ℕ → ProbComp (List Bool × List Bool))
 /-! ### One-Time Symmetric Encryption (DEM) -/
 
 /-- The one-time symmetric chosen-plaintext experiment over message space `Msg` with challenge-pair
-admissibility predicate `valid` ([BonehShoup2023], Section 2.2, Attack Game 2.1, p. 16): sample a
-uniform `n`-bit key `k ← BitString.sampleList n` and invoke `adversary.choose n []`; the adversary
-receives the empty public key `[]`, and `valid` is evaluated at it. If the chosen pair is valid,
-encrypt the selected message under `encryptSym n k` and pass the saved state and challenge
-ciphertext to `adversary.guess n`; otherwise return `false`, in both experiments. -/
-noncomputable def demGameOn {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool)
-    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
+admissibility predicate `valid` and key-length function `keyLen : ℕ → ℕ` ([BonehShoup2023],
+Section 2.2, Attack Game 2.1, p. 16): sample a uniform `keyLen n`-bit key
+`k ← BitString.sampleList (keyLen n)` and invoke `adversary.choose n []`; the adversary receives
+the empty public key `[]`, and `valid` is evaluated at it. If the chosen pair is valid, encrypt the
+selected message under `encryptSym n k` and pass the saved state and challenge ciphertext to
+`adversary.guess n`; otherwise return `false`, in both experiments. -/
+noncomputable def demKeyGameOn {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool)
+    (keyLen : ℕ → ℕ) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
     (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool := do
-  let k ← BitString.sampleList n
+  let k ← BitString.sampleList (keyLen n)
   let choice ← adversary.choose n []
   if valid n [] choice.1.1 choice.1.2 then
     let ciphertext ← encryptSym n k (if bit then choice.1.2 else choice.1.1)
@@ -260,36 +273,78 @@ noncomputable def demGameOn {Msg : Type} (valid : ℕ → List Bool → Msg →
   else
     return false
 
-/-- The unrestricted one-time symmetric experiment: `demGameOn` with every challenge pair
-admissible. -/
+/-- The unrestricted one-time symmetric experiment at key-length function `keyLen`: `demKeyGameOn`
+with every challenge pair admissible. -/
+noncomputable abbrev demKeyGame {Msg : Type} (keyLen : ℕ → ℕ)
+    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
+    (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool :=
+  demKeyGameOn (fun _ _ _ _ => true) keyLen encryptSym adversary bit n
+
+/-- The normalized (`n`-bit key) one-time symmetric chosen-plaintext experiment over message space
+`Msg` with challenge-pair admissibility predicate `valid` ([BonehShoup2023], Section 2.2, Attack
+Game 2.1, p. 16): `demKeyGameOn` specialized to `keyLen n = n`. -/
+noncomputable abbrev demGameOn {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool)
+    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
+    (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool :=
+  demKeyGameOn valid (fun m => m) encryptSym adversary bit n
+
+/-- The unrestricted `n`-bit key one-time symmetric experiment: `demGameOn` with every challenge
+pair admissible. -/
 noncomputable abbrev demGame {Msg : Type}
     (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
     (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) : ProbComp Bool :=
   demGameOn (fun _ _ _ _ => true) encryptSym adversary bit n
 
-/-- Running the unrestricted `demGame` on `adversary.restrict valid` has the same output
-distribution as running `demGameOn valid` on `adversary`. -/
-theorem eval_demGame_restrict {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool)
+/-- At the normalized key length `keyLen n = n`, `demKeyGameOn` is definitionally `demGameOn`. -/
+theorem demKeyGameOn_id {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool)
     (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
     (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) :
-    ProbComp.eval (demGame encryptSym (adversary.restrict valid) bit n) =
-      ProbComp.eval (demGameOn valid encryptSym adversary bit n) := by
-  simp only [demGame, demGameOn, AdversaryOf.restrict, ↓reduceIte, ProbComp.eval_bind,
+    demKeyGameOn valid (fun m => m) encryptSym adversary bit n =
+      demGameOn valid encryptSym adversary bit n :=
+  rfl
+
+/-- Whenever `keyLen n = n`, `demKeyGameOn` at security parameter `n` coincides with `demGameOn`. -/
+theorem demKeyGameOn_eq_demGameOn_of_eq {Msg : Type}
+    (valid : ℕ → List Bool → Msg → Msg → Bool) (keyLen : ℕ → ℕ)
+    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
+    (adversary : AdversaryOf Msg) (bit : Bool) {n : ℕ} (h : keyLen n = n) :
+    demKeyGameOn valid keyLen encryptSym adversary bit n =
+      demGameOn valid encryptSym adversary bit n := by
+  simp only [demKeyGameOn, demGameOn, h]
+
+/-- Running the unrestricted `demKeyGame` on `adversary.restrict valid` has the same output
+distribution as running `demKeyGameOn valid` on `adversary`. -/
+theorem eval_demKeyGame_restrict {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool)
+    (keyLen : ℕ → ℕ) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
+    (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) :
+    ProbComp.eval (demKeyGame keyLen encryptSym (adversary.restrict valid) bit n) =
+      ProbComp.eval (demKeyGameOn valid keyLen encryptSym adversary bit n) := by
+  simp only [demKeyGame, demKeyGameOn, AdversaryOf.restrict, ↓reduceIte, ProbComp.eval_bind,
     ProbComp.eval_pure, PMF.bind_bind, PMF.pure_bind, apply_ite ProbComp.eval]
   congr 1; funext k
   congr 1; funext choice
   cases valid n [] choice.1.1 choice.1.2 <;>
     simp [PMF.bind_const]
 
-/-- The one-time symmetric experiment `demGameOn valid` has a strict polynomial clock when `valid`
-is computable in polynomial time and symmetric encryption and both adversary stages have native
-certificates. -/
+/-- Running the unrestricted `demGame` on `adversary.restrict valid` has the same output
+distribution as running `demGameOn valid` on `adversary`. -/
+theorem eval_demGame_restrict {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool)
+    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool))
+    (adversary : AdversaryOf Msg) (bit : Bool) (n : ℕ) :
+    ProbComp.eval (demGame encryptSym (adversary.restrict valid) bit n) =
+      ProbComp.eval (demGameOn valid encryptSym adversary bit n) :=
+  eval_demKeyGame_restrict valid (fun m => m) encryptSym adversary bit n
+
+/-- The one-time symmetric experiment `demKeyGameOn valid keyLen` has a strict polynomial clock
+when `valid` and `keyLen` are computable in polynomial time and symmetric encryption and both
+adversary stages have native certificates. -/
 @[fun_prop]
-theorem isPPTOn_demGameOn {Msg : Type} {encMsg : Msg ↪ List Bool}
-    {valid : ℕ → List Bool → Msg → Msg → Bool}
+theorem isPPTOn_demKeyGameOn {Msg : Type} {encMsg : Msg ↪ List Bool}
+    {valid : ℕ → List Bool → Msg → Msg → Bool} {keyLen : ℕ → ℕ}
     (hvalid : ComputableInPolyTime
       (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2)
       (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool)
+    (hkeyLen : ComputableInPolyTime keyLen encUnary encUnary)
     {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
     (hencrypt : IsPPTOn (encPair encUnary (encPair encBits encMsg)) encBits
       (fun p => encryptSym p.1 p.2.1 p.2.2))
@@ -297,16 +352,52 @@ theorem isPPTOn_demGameOn {Msg : Type} {encMsg : Msg ↪ List Bool}
     {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {bit : α → Bool}
     (hn : ComputableInPolyTime n input encUnary)
     (hbit : ComputableInPolyTime bit input encBool) :
-    IsPPTOn input encBool (fun a => demGameOn valid encryptSym adversary (bit a) (n a)) := by
+    IsPPTOn input encBool
+      (fun a => demKeyGameOn valid keyLen encryptSym adversary (bit a) (n a)) := by
   have hchoose := hadversary.choose
   have hguess := hadversary.guess
-  have hsample : IsPPTOn input encBits (fun a => BitString.sampleList (n a)) :=
-    ComputableInPolyTime.sampleList hn
-  unfold demGameOn
+  have hsample : IsPPTOn input encBits (fun a => BitString.sampleList (keyLen (n a))) :=
+    ComputableInPolyTime.sampleList (hkeyLen.comp hn)
+  unfold demKeyGameOn
   ppt
 
-/-- The unrestricted one-time symmetric experiment has a strict polynomial clock when symmetric
-encryption and both adversary stages have native certificates. -/
+/-- The unrestricted one-time symmetric experiment `demKeyGame keyLen` has a strict polynomial
+clock when `keyLen` is computable in polynomial time and symmetric encryption and both adversary
+stages have native certificates. -/
+@[fun_prop]
+theorem isPPTOn_demKeyGame {Msg : Type} {encMsg : Msg ↪ List Bool}
+    {keyLen : ℕ → ℕ} (hkeyLen : ComputableInPolyTime keyLen encUnary encUnary)
+    {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
+    (hencrypt : IsPPTOn (encPair encUnary (encPair encBits encMsg)) encBits
+      (fun p => encryptSym p.1 p.2.1 p.2.2))
+    {adversary : AdversaryOf Msg} (hadversary : AdversaryOf.IsPPT encMsg adversary)
+    {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {bit : α → Bool}
+    (hn : ComputableInPolyTime n input encUnary)
+    (hbit : ComputableInPolyTime bit input encBool) :
+    IsPPTOn input encBool (fun a => demKeyGame keyLen encryptSym adversary (bit a) (n a)) :=
+  isPPTOn_demKeyGameOn (ComputableInPolyTime.const true) hkeyLen hencrypt hadversary hn hbit
+
+/-- The normalized (`n`-bit key) one-time symmetric experiment `demGameOn valid` has a strict
+polynomial clock when `valid` is computable in polynomial time and symmetric encryption and both
+adversary stages have native certificates. -/
+@[fun_prop]
+theorem isPPTOn_demGameOn {Msg : Type} {encMsg : Msg ↪ List Bool}
+    {valid : ℕ → List Bool → Msg → Msg → Bool}
+    (hvalid : ComputableInPolyTime
+      (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2)
+      (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool)
+    {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
+    (hencrypt : IsPPTOn (encPair encUnary (encPair encBits encMsg)) encBits
+      (fun p => encryptSym p.1 p.2.1 p.2.2))
+    {adversary : AdversaryOf Msg} (hadversary : AdversaryOf.IsPPT encMsg adversary)
+    {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {bit : α → Bool}
+    (hn : ComputableInPolyTime n input encUnary)
+    (hbit : ComputableInPolyTime bit input encBool) :
+    IsPPTOn input encBool (fun a => demGameOn valid encryptSym adversary (bit a) (n a)) :=
+  isPPTOn_demKeyGameOn hvalid ComputableInPolyTime.id' hencrypt hadversary hn hbit
+
+/-- The unrestricted `n`-bit key one-time symmetric experiment has a strict polynomial clock when
+symmetric encryption and both adversary stages have native certificates. -/
 @[fun_prop]
 theorem isPPTOn_demGame {Msg : Type} {encMsg : Msg ↪ List Bool}
     {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
@@ -317,29 +408,70 @@ theorem isPPTOn_demGame {Msg : Type} {encMsg : Msg ↪ List Bool}
     (hn : ComputableInPolyTime n input encUnary)
     (hbit : ComputableInPolyTime bit input encBool) :
     IsPPTOn input encBool (fun a => demGame encryptSym adversary (bit a) (n a)) :=
-  isPPTOn_demGameOn (ComputableTidilyInPolyTime.const true).computableInPolyTime hencrypt
-    hadversary hn hbit
+  isPPTOn_demKeyGame ComputableInPolyTime.id' hencrypt hadversary hn hbit
 
 /-- One-time symmetric IND-CPA / semantic security over message encoding `encMsg` with
-challenge-pair admissibility predicate `valid` ([BonehShoup2023], Section 2.2, Attack Game 2.1,
-p. 16, and Definition 2.2): every uniform strict PPT `Encryption.AdversaryOf Msg` has negligible
-distinguishing advantage between `demGameOn valid encryptSym adversary false` and
-`demGameOn valid encryptSym adversary true`. -/
-def DEMOneTimeINDCPAOn {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool)
-    (encMsg : Msg ↪ List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) : Prop :=
+challenge-pair admissibility predicate `valid` and key-length function `keyLen : ℕ → ℕ`
+([BonehShoup2023], Section 2.2, Attack Game 2.1, p. 16, and Definition 2.2): every uniform strict
+PPT `Encryption.AdversaryOf Msg` has negligible distinguishing advantage between
+`demKeyGameOn valid keyLen encryptSym adversary false` and
+`demKeyGameOn valid keyLen encryptSym adversary true`. -/
+def DEMOneTimeKeyINDCPAOn {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool)
+    (encMsg : Msg ↪ List Bool) (keyLen : ℕ → ℕ)
+    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) : Prop :=
   Game.Indistinguishable
-    (fun adversary n => ProbComp.eval (demGameOn valid encryptSym adversary false n))
-    (fun adversary n => ProbComp.eval (demGameOn valid encryptSym adversary true n))
+    (fun adversary n => ProbComp.eval (demKeyGameOn valid keyLen encryptSym adversary false n))
+    (fun adversary n => ProbComp.eval (demKeyGameOn valid keyLen encryptSym adversary true n))
     (AdversaryOf.IsPPT encMsg)
 
-/-- One-time symmetric IND-CPA with every challenge pair admissible. For `List Bool` messages this
-is stronger than the textbook notion, which `DEMOneTimeWordINDCPA` states. -/
+/-- One-time symmetric IND-CPA at key-length function `keyLen` with every challenge pair
+admissible. -/
+abbrev DEMOneTimeKeyINDCPAOf {Msg : Type} (encMsg : Msg ↪ List Bool) (keyLen : ℕ → ℕ)
+    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) : Prop :=
+  DEMOneTimeKeyINDCPAOn (fun _ _ _ _ => true) encMsg keyLen encryptSym
+
+/-- Unrestricted one-time symmetric IND-CPA at key length `keyLen` implies one-time symmetric
+IND-CPA under every polynomial-time admissibility predicate. -/
+theorem DEMOneTimeKeyINDCPAOf.demOneTimeKeyINDCPAOn {Msg : Type} {encMsg : Msg ↪ List Bool}
+    {valid : ℕ → List Bool → Msg → Msg → Bool} {keyLen : ℕ → ℕ}
+    {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
+    (h : DEMOneTimeKeyINDCPAOf encMsg keyLen encryptSym)
+    (hvalid : ComputableInPolyTime
+      (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2)
+      (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool) :
+    DEMOneTimeKeyINDCPAOn valid encMsg keyLen encryptSym := by
+  intro adversary hadversary
+  simpa only [eval_demKeyGame_restrict] using
+    h (adversary.restrict valid) (hadversary.restrict hvalid)
+
+/-- One-time symmetric IND-CPA / semantic security for single-bit encryption at key length
+`keyLen`. -/
+abbrev DEMOneTimeKeyINDCPA (keyLen : ℕ → ℕ)
+    (encryptSym : ℕ → List Bool → Bool → ProbComp (List Bool)) : Prop :=
+  DEMOneTimeKeyINDCPAOf encBool keyLen encryptSym
+
+/-- One-time symmetric IND-CPA / semantic security for bit-word encryption at key length `keyLen`
+under Attack Game 2.1's equal-length rule ([BonehShoup2023], Section 2.2, p. 16). -/
+abbrev DEMOneTimeKeyWordINDCPA (keyLen : ℕ → ℕ)
+    (encryptSym : ℕ → List Bool → List Bool → ProbComp (List Bool)) : Prop :=
+  DEMOneTimeKeyINDCPAOn (fun _ _ m₀ m₁ => m₀.length == m₁.length) encBits keyLen encryptSym
+
+/-- Normalized (`n`-bit key) one-time symmetric IND-CPA / semantic security over message encoding
+`encMsg` with challenge-pair admissibility predicate `valid` ([BonehShoup2023], Section 2.2, Attack
+Game 2.1, p. 16, and Definition 2.2): `DEMOneTimeKeyINDCPAOn` specialized to `keyLen n = n`. -/
+abbrev DEMOneTimeINDCPAOn {Msg : Type} (valid : ℕ → List Bool → Msg → Msg → Bool)
+    (encMsg : Msg ↪ List Bool) (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) : Prop :=
+  DEMOneTimeKeyINDCPAOn valid encMsg (fun n => n) encryptSym
+
+/-- Normalized (`n`-bit key) one-time symmetric IND-CPA with every challenge pair admissible. For
+`List Bool` messages this is stronger than the textbook notion, which `DEMOneTimeWordINDCPA`
+states. -/
 abbrev DEMOneTimeINDCPAOf {Msg : Type} (encMsg : Msg ↪ List Bool)
     (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) : Prop :=
   DEMOneTimeINDCPAOn (fun _ _ _ _ => true) encMsg encryptSym
 
-/-- Unrestricted one-time symmetric IND-CPA implies one-time symmetric IND-CPA under every
-polynomial-time admissibility predicate. -/
+/-- Unrestricted `n`-bit key one-time symmetric IND-CPA implies one-time symmetric IND-CPA under
+every polynomial-time admissibility predicate. -/
 theorem DEMOneTimeINDCPAOf.demOneTimeINDCPAOn {Msg : Type} {encMsg : Msg ↪ List Bool}
     {valid : ℕ → List Bool → Msg → Msg → Bool}
     {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
@@ -347,22 +479,42 @@ theorem DEMOneTimeINDCPAOf.demOneTimeINDCPAOn {Msg : Type} {encMsg : Msg ↪ Lis
     (hvalid : ComputableInPolyTime
       (fun p : ℕ × List Bool × Msg × Msg => valid p.1 p.2.1 p.2.2.1 p.2.2.2)
       (encPair encUnary (encPair encBits (encPair encMsg encMsg))) encBool) :
-    DEMOneTimeINDCPAOn valid encMsg encryptSym := by
-  intro adversary hadversary
-  simpa only [eval_demGame_restrict] using
-    h (adversary.restrict valid) (hadversary.restrict hvalid)
+    DEMOneTimeINDCPAOn valid encMsg encryptSym :=
+  DEMOneTimeKeyINDCPAOf.demOneTimeKeyINDCPAOn h hvalid
 
-/-- One-time symmetric IND-CPA / semantic security for single-bit encryption. -/
+/-- Normalized (`n`-bit key) one-time symmetric IND-CPA / semantic security for single-bit
+encryption. -/
 abbrev DEMOneTimeINDCPA (encryptSym : ℕ → List Bool → Bool → ProbComp (List Bool)) : Prop :=
   DEMOneTimeINDCPAOf encBool encryptSym
 
-/-- One-time symmetric IND-CPA / semantic security for bit-word encryption under Attack Game 2.1's
-equal-length rule ([BonehShoup2023], Section 2.2, p. 16): challenge pairs with
-`m₀.length ≠ m₁.length` are inadmissible. -/
+/-- Normalized (`n`-bit key) one-time symmetric IND-CPA / semantic security for bit-word encryption
+under Attack Game 2.1's equal-length rule ([BonehShoup2023], Section 2.2, p. 16): challenge pairs
+with `m₀.length ≠ m₁.length` are inadmissible. -/
 abbrev DEMOneTimeWordINDCPA
     (encryptSym : ℕ → List Bool → List Bool → ProbComp (List Bool)) : Prop :=
   DEMOneTimeINDCPAOn (fun _ _ m₀ m₁ => m₀.length == m₁.length) encBits encryptSym
 
+/-- At the normalized key length `keyLen n = n`, `DEMOneTimeKeyINDCPAOn` is definitionally
+`DEMOneTimeINDCPAOn`. -/
+theorem demOneTimeKeyINDCPAOn_id {Msg : Type}
+    (valid : ℕ → List Bool → Msg → Msg → Bool) (encMsg : Msg ↪ List Bool)
+    (encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)) :
+    DEMOneTimeKeyINDCPAOn valid encMsg (fun n => n) encryptSym ↔
+      DEMOneTimeINDCPAOn valid encMsg encryptSym :=
+  Iff.rfl
+
+/-- Whenever `keyLen n = n` for all `n`, `DEMOneTimeINDCPAOn` implies `DEMOneTimeKeyINDCPAOn`. -/
+theorem DEMOneTimeINDCPAOn.demOneTimeKeyINDCPAOn {Msg : Type} {encMsg : Msg ↪ List Bool}
+    {valid : ℕ → List Bool → Msg → Msg → Bool} {keyLen : ℕ → ℕ}
+    {encryptSym : ℕ → List Bool → Msg → ProbComp (List Bool)}
+    (h : DEMOneTimeINDCPAOn valid encMsg encryptSym) (hkeyLen : ∀ n, keyLen n = n) :
+    DEMOneTimeKeyINDCPAOn valid encMsg keyLen encryptSym := by
+  intro adversary hadversary
+  simpa only [fun n => demKeyGameOn_eq_demGameOn_of_eq valid keyLen encryptSym adversary false
+    (hkeyLen n),
+    fun n => demKeyGameOn_eq_demGameOn_of_eq valid keyLen encryptSym adversary true
+    (hkeyLen n)] using h adversary hadversary
+
 /-! ### Hybrid Encryption Construction and Correctness -/
 
 /-- KEM–DEM hybrid encryption ([BonehShoup2023], Exercise 11.9): encapsulate a symmetric key
@@ -758,9 +910,9 @@ game `hybridIdealGame`. -/
     ProbComp.eval
       (demGame encryptSym (hybridToDEMAdversary keyGen encaps adversary) bit n) =
       ProbComp.eval (hybridIdealGame keyGen encaps encryptSym adversary bit n) := by
-  simp only [demGame, demGameOn, ↓reduceIte, hybridToDEMAdversary, hybridIdealGame, encPair_apply,
-    encBits_apply, ProbComp.eval_bind, ProbComp.eval_pure, PMF.bind_bind, PMF.pure_bind,
-    unframe_frame_append, dropFrame_frame_append]
+  simp only [demGame, demGameOn, demKeyGameOn, ↓reduceIte, hybridToDEMAdversary, hybridIdealGame,
+    encPair_apply, encBits_apply, ProbComp.eval_bind, ProbComp.eval_pure, PMF.bind_bind,
+    PMF.pure_bind, unframe_frame_append, dropFrame_frame_append]
   rw [PMF.bind_comm]
   congr 1; funext keys
   rw [PMF.bind_comm]
@@ -985,8 +1137,8 @@ theorem eval_demGame_hybridToDEMAdversary_restrict {Msg : Type}
       (demGame encryptSym (hybridToDEMAdversary keyGen encaps (adversary.restrict valid)) bit n) =
       ProbComp.eval (demGameOn valid encryptSym
         (hybridToDEMAdversary keyGen encaps (adversary.restrict valid)) bit n) := by
-  simp only [demGame, demGameOn, hybridToDEMAdversary, AdversaryOf.restrict, ↓reduceIte,
-    ProbComp.eval_bind, ProbComp.eval_pure, PMF.bind_bind, PMF.pure_bind,
+  simp only [demGame, demGameOn, demKeyGameOn, hybridToDEMAdversary, AdversaryOf.restrict,
+    ↓reduceIte, ProbComp.eval_bind, ProbComp.eval_pure, PMF.bind_bind, PMF.pure_bind,
     apply_ite ProbComp.eval, encPair_apply, encBits_apply, unframe_frame_append,
     dropFrame_frame_append]
   congr 1; funext k
@@ -1073,7 +1225,7 @@ theorem eval_demGame_otpEncrypt_false_eq_true {n : ℕ} (hn : 1 ≤ n) (adversar
     ProbComp.eval (demGame otpEncrypt adversary false n) =
       ProbComp.eval (demGame otpEncrypt adversary true n) := by
   obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le' hn
-  simp only [demGame, demGameOn, otpEncrypt, ProbComp.eval_bind, ProbComp.eval_pure,
+  simp only [demGame, demGameOn, demKeyGameOn, otpEncrypt, ProbComp.eval_bind, ProbComp.eval_pure,
     BitString.eval_sampleList, BitString.uniformList_succ, PMF.bind_bind, PMF.bind_map,
     Function.comp_def, PMF.pure_bind, List.headD_cons, Bool.false_eq_true, ↓reduceIte]
   rw [PMF.bind_comm]
@@ -1112,81 +1264,159 @@ theorem KEMINDCPA.hybrid_otpEncrypt_indcpa
     INDCPA keyGen (hybridEncrypt encaps otpEncrypt) :=
   hkem.hybrid_indcpa demOneTimeINDCPA_otpEncrypt hkeyGen hencaps isPPTOn_otpEncrypt
 
-/-- One-time pad `n`-bit word symmetric encryption: XOR the `n`-bit key `k` with the plaintext
-word `m` at width `n` using `BitString.listXor n [k, m]`. -/
-def otpWordEncrypt (n : ℕ) (k m : List Bool) : ProbComp (List Bool) :=
-  pure (BitString.listXor n [k, m])
+/-- One-time pad `keyLen n`-bit word symmetric encryption: XOR the `keyLen n`-bit key `k` with the
+plaintext word `m` at width `keyLen n` using `BitString.listXor (keyLen n) [k, m]`. -/
+def otpKeyWordEncrypt (keyLen : ℕ → ℕ) (n : ℕ) (k m : List Bool) : ProbComp (List Bool) :=
+  pure (BitString.listXor (keyLen n) [k, m])
+
+/-- One-time pad `keyLen n`-bit word symmetric decryption: XOR the `keyLen n`-bit key `k` with the
+ciphertext word `ct` at width `keyLen n` using `BitString.listXor (keyLen n) [k, ct]`. -/
+def otpKeyWordDecrypt (keyLen : ℕ → ℕ) (n : ℕ) (k ct : List Bool) : List Bool :=
+  BitString.listXor (keyLen n) [k, ct]
+
+/-- One-time pad word decryption at key length `keyLen` inverts encryption on every
+`keyLen n`-bit plaintext word `m`. -/
+theorem otpKeyWordDecrypt_otpKeyWordEncrypt (keyLen : ℕ → ℕ) (n : ℕ) (k : List Bool)
+    {m : List Bool} (hm : m.length = keyLen n) :
+    otpKeyWordDecrypt keyLen n k (BitString.listXor (keyLen n) [k, m]) = m :=
+  BitString.listXor_pair_self_left_of_length k hm
+
+/-- `otpKeyWordEncrypt keyLen` is uniform strict PPT whenever `keyLen` is computable in polynomial
+time in unary. -/
+@[fun_prop]
+theorem isPPTOn_otpKeyWordEncrypt {keyLen : ℕ → ℕ}
+    (hkeyLen : ComputableInPolyTime keyLen encUnary encUnary) :
+    IsPPTOn (encPair encUnary (encPair encBits encBits)) encBits
+      (fun p => otpKeyWordEncrypt keyLen p.1 p.2.1 p.2.2) := by
+  have hk : ComputableInPolyTime
+      (fun p : ℕ × List Bool × List Bool => keyLen p.1)
+      (encPair encUnary (encPair encBits encBits)) encUnary :=
+    hkeyLen.comp (ComputableInPolyTime.fst _ _)
+  unfold otpKeyWordEncrypt
+  ppt
+
+/-- `otpKeyWordDecrypt keyLen` is computable in polynomial time whenever `keyLen` is computable in
+polynomial time in unary. -/
+@[fun_prop]
+theorem computableInPolyTime_otpKeyWordDecrypt {keyLen : ℕ → ℕ}
+    (hkeyLen : ComputableInPolyTime keyLen encUnary encUnary) :
+    ComputableInPolyTime
+      (fun p : ℕ × List Bool × List Bool =>
+        otpKeyWordDecrypt keyLen p.1 p.2.1 p.2.2)
+      (encPair encUnary (encPair encBits encBits)) encBits := by
+  have hk : ComputableInPolyTime
+      (fun p : ℕ × List Bool × List Bool => keyLen p.1)
+      (encPair encUnary (encPair encBits encBits)) encUnary :=
+    hkeyLen.comp (ComputableInPolyTime.fst _ _)
+  have hkt := hk.tidy
+  unfold otpKeyWordDecrypt
+  exact ComputableInPolyTime.of_tidy (by polytime)
+
+/-- A uniform `keyLen n`-bit key masks any challenge word perfectly in
+`demKeyGame keyLen (otpKeyWordEncrypt keyLen)`, so the `false` and `true` experiment distributions
+are identical for every `keyLen` and `n`. -/
+theorem eval_demKeyGame_otpKeyWordEncrypt_false_eq_true (keyLen : ℕ → ℕ) (n : ℕ)
+    (adversary : WordAdversary) :
+    ProbComp.eval (demKeyGame keyLen (otpKeyWordEncrypt keyLen) adversary false n) =
+      ProbComp.eval (demKeyGame keyLen (otpKeyWordEncrypt keyLen) adversary true n) := by
+  have hpad (msg state : List Bool) :
+      (do
+        let k ← BitString.uniformList (keyLen n)
+        ProbComp.eval
+          (adversary.guess n state (BitString.listXor (keyLen n) [k, msg]))) =
+      (do
+        let ct ← BitString.uniformList (keyLen n)
+        ProbComp.eval (adversary.guess n state ct)) := by
+    have h := congrArg
+      (fun law : PMF (List Bool) => law.bind (ProbComp.eval ∘ adversary.guess n state))
+      (BitString.uniformList_map_listXor (keyLen n) msg)
+    simpa only [PMF.bind_map, Function.comp_def, PMF.monad_bind_eq_bind] using h
+  simp only [demKeyGame, demKeyGameOn, ↓reduceIte, otpKeyWordEncrypt, ProbComp.eval_bind,
+    ProbComp.eval_pure, BitString.eval_sampleList, PMF.pure_bind, Bool.false_eq_true]
+  rw [PMF.bind_comm]
+  conv_rhs => rw [PMF.bind_comm]
+  congr 1; funext choice
+  exact (hpad choice.1.1 choice.2).trans (hpad choice.1.2 choice.2).symm
+
+/-- Every word adversary has exact advantage `0` in
+`demKeyGame keyLen (otpKeyWordEncrypt keyLen)`. -/
+theorem advantage_demKeyGame_otpKeyWordEncrypt_eq_zero (keyLen : ℕ → ℕ) (n : ℕ)
+    (adversary : WordAdversary) :
+    Game.advantage
+      (ProbComp.eval (demKeyGame keyLen (otpKeyWordEncrypt keyLen) adversary false n))
+      (ProbComp.eval (demKeyGame keyLen (otpKeyWordEncrypt keyLen) adversary true n)) = 0 := by
+  rw [eval_demKeyGame_otpKeyWordEncrypt_false_eq_true keyLen n adversary, Game.advantage_self]
+
+/-- **The `keyLen n`-bit word one-time pad is unconditionally one-time IND-CPA secure**
+(`DEMOneTimeKeyINDCPAOf encBits keyLen (otpKeyWordEncrypt keyLen)`). -/
+theorem demOneTimeKeyINDCPA_otpKeyWordEncrypt (keyLen : ℕ → ℕ) :
+    DEMOneTimeKeyINDCPAOf encBits keyLen (otpKeyWordEncrypt keyLen) := by
+  intro adversary _ c
+  refine tendsto_const_nhds.congr' ?_
+  filter_upwards with n
+  simp [advantage_demKeyGame_otpKeyWordEncrypt_eq_zero keyLen n adversary]
+
+/-- **The `keyLen n`-bit word one-time pad satisfies equal-length word DEM security**
+(`DEMOneTimeKeyWordINDCPA keyLen (otpKeyWordEncrypt keyLen)`). -/
+theorem demOneTimeKeyWordINDCPA_otpKeyWordEncrypt (keyLen : ℕ → ℕ) :
+    DEMOneTimeKeyWordINDCPA keyLen (otpKeyWordEncrypt keyLen) :=
+  (demOneTimeKeyINDCPA_otpKeyWordEncrypt keyLen).demOneTimeKeyINDCPAOn
+    (ComputableInPolyTime.of_tidy (by polytime))
 
-/-- One-time pad `n`-bit word symmetric decryption: XOR the `n`-bit key `k` with the ciphertext
-word `ct` at width `n` using `BitString.listXor n [k, ct]`. -/
-def otpWordDecrypt (n : ℕ) (k ct : List Bool) : List Bool :=
-  BitString.listXor n [k, ct]
+/-- One-time pad `n`-bit word symmetric encryption: `otpKeyWordEncrypt` specialized to
+`keyLen n = n`. -/
+abbrev otpWordEncrypt (n : ℕ) (k m : List Bool) : ProbComp (List Bool) :=
+  otpKeyWordEncrypt (fun m => m) n k m
+
+/-- One-time pad `n`-bit word symmetric decryption: `otpKeyWordDecrypt` specialized to
+`keyLen n = n`. -/
+abbrev otpWordDecrypt (n : ℕ) (k ct : List Bool) : List Bool :=
+  otpKeyWordDecrypt (fun m => m) n k ct
 
 /-- One-time pad word decryption inverts one-time pad word encryption on every `n`-bit plaintext
 word `m`. -/
 theorem otpWordDecrypt_otpWordEncrypt {n : ℕ} (k : List Bool) {m : List Bool}
     (hm : m.length = n) :
     otpWordDecrypt n k (BitString.listXor n [k, m]) = m :=
-  BitString.listXor_pair_self_left_of_length k hm
+  otpKeyWordDecrypt_otpKeyWordEncrypt (fun m => m) n k hm
 
 /-- One-time pad word encryption is uniform strict PPT. -/
 @[fun_prop]
 theorem isPPTOn_otpWordEncrypt :
     IsPPTOn (encPair encUnary (encPair encBits encBits)) encBits
-      (fun p => otpWordEncrypt p.1 p.2.1 p.2.2) := by
-  unfold otpWordEncrypt
-  ppt
+      (fun p => otpWordEncrypt p.1 p.2.1 p.2.2) :=
+  isPPTOn_otpKeyWordEncrypt ComputableInPolyTime.id'
 
 /-- One-time pad word decryption is computable in polynomial time. -/
 @[fun_prop]
 theorem computableInPolyTime_otpWordDecrypt :
     ComputableInPolyTime
       (fun p : ℕ × List Bool × List Bool => otpWordDecrypt p.1 p.2.1 p.2.2)
-      (encPair encUnary (encPair encBits encBits)) encBits := by
-  unfold otpWordDecrypt
-  exact ComputableInPolyTime.of_tidy (by fun_prop)
+      (encPair encUnary (encPair encBits encBits)) encBits :=
+  computableInPolyTime_otpKeyWordDecrypt ComputableInPolyTime.id'
 
 /-- A uniform `n`-bit key masks any challenge word perfectly in `demGame otpWordEncrypt`, so the
 `false` and `true` experiment distributions are identical for every `n`. -/
 theorem eval_demGame_otpWordEncrypt_false_eq_true (n : ℕ) (adversary : WordAdversary) :
     ProbComp.eval (demGame otpWordEncrypt adversary false n) =
-      ProbComp.eval (demGame otpWordEncrypt adversary true n) := by
-  have hpad (msg state : List Bool) :
-      (do
-        let k ← BitString.uniformList n
-        ProbComp.eval (adversary.guess n state (BitString.listXor n [k, msg]))) =
-      (do
-        let ct ← BitString.uniformList n
-        ProbComp.eval (adversary.guess n state ct)) := by
-    have h := congrArg
-      (fun law : PMF (List Bool) => law.bind (ProbComp.eval ∘ adversary.guess n state))
-      (BitString.uniformList_map_listXor n msg)
-    simpa only [PMF.bind_map, Function.comp_def, PMF.monad_bind_eq_bind] using h
-  simp only [demGame, demGameOn, ↓reduceIte, otpWordEncrypt, ProbComp.eval_bind, ProbComp.eval_pure,
-    BitString.eval_sampleList, PMF.pure_bind, Bool.false_eq_true, ↓reduceIte]
-  rw [PMF.bind_comm]
-  conv_rhs => rw [PMF.bind_comm]
-  congr 1; funext choice
-  exact (hpad choice.1.1 choice.2).trans (hpad choice.1.2 choice.2).symm
+      ProbComp.eval (demGame otpWordEncrypt adversary true n) :=
+  eval_demKeyGame_otpKeyWordEncrypt_false_eq_true (fun m => m) n adversary
 
 /-- Every word adversary has exact advantage `0` in `demGame otpWordEncrypt`. -/
 theorem advantage_demGame_otpWordEncrypt_eq_zero (n : ℕ) (adversary : WordAdversary) :
     Game.advantage (ProbComp.eval (demGame otpWordEncrypt adversary false n))
-      (ProbComp.eval (demGame otpWordEncrypt adversary true n)) = 0 := by
-  rw [eval_demGame_otpWordEncrypt_false_eq_true n adversary, Game.advantage_self]
+      (ProbComp.eval (demGame otpWordEncrypt adversary true n)) = 0 :=
+  advantage_demKeyGame_otpKeyWordEncrypt_eq_zero (fun m => m) n adversary
 
 /-- **The `n`-bit word one-time pad is unconditionally one-time IND-CPA secure**
 (`DEMOneTimeINDCPAOf encBits otpWordEncrypt`). -/
-theorem demOneTimeINDCPA_otpWordEncrypt : DEMOneTimeINDCPAOf encBits otpWordEncrypt := by
-  intro adversary _ c
-  refine tendsto_const_nhds.congr' ?_
-  filter_upwards with n
-  simp [advantage_demGame_otpWordEncrypt_eq_zero n adversary]
+theorem demOneTimeINDCPA_otpWordEncrypt : DEMOneTimeINDCPAOf encBits otpWordEncrypt :=
+  demOneTimeKeyINDCPA_otpKeyWordEncrypt (fun m => m)
 
 /-- **The `n`-bit word one-time pad satisfies equal-length word DEM security**
 (`DEMOneTimeWordINDCPA otpWordEncrypt`). -/
 theorem demOneTimeWordINDCPA_otpWordEncrypt : DEMOneTimeWordINDCPA otpWordEncrypt :=
-  demOneTimeINDCPA_otpWordEncrypt.demOneTimeINDCPAOn (ComputableInPolyTime.of_tidy (by polytime))
+  demOneTimeKeyWordINDCPA_otpKeyWordEncrypt (fun m => m)
 
 /-- **KEM-to-word-PKE corollary**: combining any IND-CPA secure KEM with the `n`-bit word one-time
 pad DEM yields a public-key word-encryption scheme satisfying `WordINDCPA`, through the
diff --git a/ComplexityTests/Crypto/DiffieHellman.lean b/ComplexityTests/Crypto/DiffieHellman.lean
index 328635dae4..1036bf8db4 100644
--- a/ComplexityTests/Crypto/DiffieHellman.lean
+++ b/ComplexityTests/Crypto/DiffieHellman.lean
@@ -785,4 +785,97 @@ theorem advantage_hashedElGamalCipherCPAGameOn_identitySym
   rw [h0, h1, Game.advantage, Game.succProbability, Game.succProbability]
   simp
 
+/-- Positive-side non-`n` key-length instantiation (`outLen := fun _ => 4`) of
+`DDH.negligible_hashedElGamalCipherCPAGameOn_linearHashKDF_of_demOneTimeKeyINDCPAOn` with a
+4-bit one-time pad symmetric cipher `Encryption.otpKeyWordEncrypt (fun _ => 4)`
+(`Encryption.demOneTimeKeyWordINDCPA_otpKeyWordEncrypt (fun _ => 4)`): IND-CPA security holds
+under `schnorrGroups.DDH` and `2 ^ n ≤ schnorrGroups.order d` at constant 4-bit symmetric key
+length. -/
+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 = 4)
+    (hsize : ∀ n, ∀ d ∈ (ProbComp.eval (setupProb n)).support,
+      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 _ => 4)
+              (fun d => (schnorrGroups.encDesc d).length)))
+          (schnorrGroups.linearHashKDF keyLen (fun d => (schnorrGroups.encDesc d).length))
+          (Encryption.otpKeyWordEncrypt (fun _ => 4)) hashedWordAdversary false n)
+        (schnorrGroups.withSeed.hashedElGamalCipherCPAGameOn equalLengthWords
+          (schnorrGroups.seededSetup (fun m => ProbComp.eval (setupProb m))
+            (schnorrGroups.linearHashSeedLen (fun _ => 4)
+              (fun d => (schnorrGroups.encDesc d).length)))
+          (schnorrGroups.linearHashKDF keyLen (fun d => (schnorrGroups.encDesc d).length))
+          (Encryption.otpKeyWordEncrypt (fun _ => 4)) hashedWordAdversary true n) := by
+  have hout_poly : ComputableInPolyTime (fun _ : ℕ => 4) encUnary encUnary :=
+    ComputableInPolyTime.const 4
+  refine hDDH.negligible_hashedElGamalCipherCPAGameOn_linearHashKDF_of_demOneTimeKeyINDCPAOn
+    (Encryption.demOneTimeKeyWordINDCPA_otpKeyWordEncrypt (fun _ => 4)) hsetup hout_poly 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_otpKeyWordEncrypt hout_poly) hashedWordAdversary_isPPT
+  have h : (fun n => (2 : ℝ≥0) ^ 4 / ((2 ^ n : ℕ) : ℝ≥0)) =
+      fun n => (16 : ℝ≥0) * (1 / (2 ^ n : ℕ) : ℝ≥0) := by
+    funext n
+    push_cast
+    ring
+  rw [h]
+  exact negligible_inv_two_pow.const_mul 16
+
+/-- A uniform strict-PPT standalone symmetric word adversary that submits `([false], [true])` and
+returns the first bit of the symmetric ciphertext `ct`. -/
+noncomputable def firstBitSymAdversary : Encryption.WordAdversary where
+  choose _ _ := pure (([false], [true]), [])
+  guess _ _ ct := pure (ct.headD false)
+
+/-- `firstBitSymAdversary` is uniform strict PPT. -/
+theorem firstBitSymAdversary_isPPT : firstBitSymAdversary.IsPPT where
+  choose := (ComputableInPolyTime.const _).isPPTOn
+  guess := by
+    have hhead : ComputableInPolyTime (fun s : List Bool => s.headD false) encBits encBool :=
+      by fun_prop
+    have hct : ComputableInPolyTime
+        (fun p : ℕ × List Bool × List Bool => p.2.2.headD false)
+        (encPair encUnary (encPair encBits encBits)) encBool :=
+      hhead.comp (by fun_prop)
+    exact hct.isPPTOn
+
+/-- Refutation test for `DEMOneTimeKeyWordINDCPA` at non-`n` key length (`keyLen = fun _ => 4`):
+`identitySym` is not one-time semantically secure at 4-bit key length. -/
+theorem not_demOneTimeKeyWordINDCPA_identitySym :
+    ¬ Encryption.DEMOneTimeKeyWordINDCPA (fun _ => 4) identitySym := by
+  intro hsec
+  have hneg := hsec firstBitSymAdversary firstBitSymAdversary_isPPT
+  have hadv (n : ℕ) :
+      Game.advantage
+        (ProbComp.eval
+          (Encryption.demKeyGameOn (fun _ _ m₀ m₁ => m₀.length == m₁.length) (fun _ => 4)
+            identitySym firstBitSymAdversary false n))
+        (ProbComp.eval
+          (Encryption.demKeyGameOn (fun _ _ m₀ m₁ => m₀.length == m₁.length) (fun _ => 4)
+            identitySym firstBitSymAdversary true n)) = 1 := by
+    have h0 :
+        ProbComp.eval
+          (Encryption.demKeyGameOn (fun _ _ m₀ m₁ => m₀.length == m₁.length) (fun _ => 4)
+            identitySym firstBitSymAdversary false n) = PMF.pure false := by
+      simp [Encryption.demKeyGameOn, identitySym, firstBitSymAdversary, PMF.map,
+        Function.comp_def, PMF.bind_const]
+    have h1 :
+        ProbComp.eval
+          (Encryption.demKeyGameOn (fun _ _ m₀ m₁ => m₀.length == m₁.length) (fun _ => 4)
+            identitySym firstBitSymAdversary true n) = PMF.pure true := by
+      simp [Encryption.demKeyGameOn, identitySym, firstBitSymAdversary, PMF.map,
+        Function.comp_def, PMF.bind_const]
+    rw [h0, h1, Game.advantage, Game.succProbability, Game.succProbability]
+    simp
+  simp only [hadv] at hneg
+  exact not_negligible_const one_ne_zero hneg
+
 end ComplexityTests.Crypto.DiffieHellman
diff --git a/ComplexityTests/Crypto/HybridEncryption.lean b/ComplexityTests/Crypto/HybridEncryption.lean
index abf6cab961..083009af6d 100644
--- a/ComplexityTests/Crypto/HybridEncryption.lean
+++ b/ComplexityTests/Crypto/HybridEncryption.lean
@@ -372,7 +372,7 @@ example :
       1 := by
   have h : [false, true, true] =
       BitString.listXor 3 [[true, false, true], [true, true, false]] := by decide
-  rw [otpWordEncrypt, ProbComp.eval_pure, h, PMF.pure_apply_self]
+  rw [otpWordEncrypt, otpKeyWordEncrypt, ProbComp.eval_pure, h, PMF.pure_apply_self]
 
 /-- Instantiation of the word-message security reduction `KEMINDCPA.hybrid_otpWordEncrypt_indcpa`
 on `idealEncaps` and `otpWordEncrypt`. -/
diff --git a/ROADMAP.md b/ROADMAP.md
index 966929f763..67ab723dfe 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -119,10 +119,6 @@ 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:** 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** ([#1885]): multi-challenge CCA from the single-challenge
   Cramer–Shoup theorem.
 - **Lattices**: Fiat–Shamir with aborts and signatures from SIS (Lyubashevsky 2009,
@@ -724,7 +720,6 @@ not planned, not as proved.
 [#999]: https://github.com/cslib-community/complexitylib/issues/999
 [#1001]: https://github.com/cslib-community/complexitylib/issues/1001
 [#1002]: https://github.com/cslib-community/complexitylib/issues/1002
-[#1047]: https://github.com/cslib-community/complexitylib/issues/1047
 [#1104]: https://github.com/cslib-community/complexitylib/issues/1104
 [#1124]: https://github.com/cslib-community/complexitylib/issues/1124
 [#1155]: https://github.com/cslib-community/complexitylib/issues/1155