The Cramer–Shoup public-key encryption scheme and 1CCA security under DDH

This module completes the single-challenge adaptive chosen-ciphertext (1CCA / IND-CCA2, Definition 12.2, printed p. 468) security proof for the Multiplicative Cramer–Shoup public-key encryption scheme ($\mathcal{E}_{\mathrm{MCS}}$, Boneh and Shoup, Exercise 12.27, printed pp. 521–522, specialized to associated data $\mathcal{D} = \mathrm{Unit}$) defined in Complexity.Crypto.Computational.CramerShoup.Scheme over a PrimeOrderGroupFamily, in the standard model under:

1. the Decisional Diffie–Hellman (DDH) assumption,
2. collision resistance (CollisionResistantFor) of the $\mathbb{Z}_q$-valued hash family $H'$ (cramerShoupHashMod), and
3. a positive group-order lower bound $m(n) > 0$ with $m(n) \le q$ and negligible inverse order $1 / m(n)$,

following the Games 0–6 proof template of Boneh and Shoup, Section 12.5.3, Theorem 12.9 and Remark 12.3, printed pp. 488–493.

We first prove the concrete and asymptotic 1CCA bounds for the ideal exact-uniform PMF games (cramerShoupMsgCCA2Game, cramerShoupGroupCCA2Game, cramerShoupGroupINDCCA2, cramerShoupCCA2Game, cramerShoupINDCCA2), in which key and challenge exponents are drawn from PMF.uniformOfFintype (ZMod (F.order d)) and the 42 / 2 ^ n dyadic loss arises solely from the sampleModNat exponent draws inside the strict-PPT DDH and CRHF reductions. We then bridge these ideal games to the library's native strict-PPT PKE 1CCA notion (Encryption.cca2GameOn and Encryption.INDCCA2On in Complexity/Crypto/Computational/Encryption/CCA.lean) via advantage_cca2GameOn_cramerShoupGroupCCA2Game_le (which accounts for the additional 8 / 2 ^ n per-bit sampleModNat approximation loss of cramerShoupKeyGenProb and cramerShoupEncryptProb), yielding DDH.indcca2On_cramerShoup.

Source Statements ([BS23], Section 12.5.3 & Exercise 12.27)

Verbatim from [BS23], Section 12.5.3 (printed pp. 489–492):

Theorem 12.9. If the DDH assumption holds in $\mathbb{G}$, $\mathcal{E}_s$ is 1CCA secure, $H$ is a secure KDF, and $H'$ is collision resistant, then $\mathcal{E}_{\mathrm{CS}}$ is CCA secure.

In particular, for every 1CCA adversary $\mathcal{A}$ that attacks $\mathcal{E}_{\mathrm{CS}}$ as in Definition 12.2, and makes at most $Q_d$ decryption queries, there exist a DDH adversary $\mathcal{B}_{\mathrm{ddh}}$ for $\mathbb{G}$ as in Attack Game 10.6, a 1CCA adversary $\mathcal{B}_s$ that attacks $\mathcal{E}_s$ as in Definition 9.6, a KDF adversary $\mathcal{B}_{\mathrm{kdf}}$ that attacks $H$ as in Attack Game 11.3, and a collision-finding adversary $\mathcal{B}_{\mathrm{cr}}$ that attacks $H'$ as in Attack Game 8.1, where $\mathcal{B}_{\mathrm{ddh}}, \mathcal{B}_s, \mathcal{B}_{\mathrm{kdf}}, \mathcal{B}_{\mathrm{cr}}$ are elementary wrappers around $\mathcal{A}$, such that $$\text{1CCAadv}[\mathcal{A}, \mathcal{E}_{\mathrm{CS}}] \le 2\left(\text{DDHadv}[\mathcal{B}_{\mathrm{ddh}}, \mathbb{G}] + \text{KDFadv}[\mathcal{B}_{\mathrm{kdf}}, H] + \text{CRadv}[\mathcal{B}_{\mathrm{cr}}, H'] + \frac{Q_d + 1}{q}\right) + \text{1CCAadv}[\mathcal{B}_s, \mathcal{E}_s]. \quad (12.19)$$ … Game 1. We replace the lines marked (2) and (3) in Fig. 12.3 as follows: $$(2) \qquad z \leftarrow f(v, w)$$ $$(3) \qquad z' \leftarrow f'(v, w, \rho)$$ Here, instead of using the auxiliary information that allows us to compute $f$ on $L_u$ and $f'$ on $L_u \times \mathbb{Z}_q$, we compute them directly, using the secret key $\mathit{sk}$. This does not change the result of the computation in any way. Therefore, $$\Pr[W_1] = \Pr[W_0]. \quad (12.21)$$ … Game 2. We replace the line marked (1) in Fig. 12.3 with $$(1) \qquad \gamma \xleftarrow{R} \mathbb{Z}_q$$ … It is easy to see that $$|\Pr[W_1] - \Pr[W_2]| \le \text{DDHadv}[\mathcal{B}_{\mathrm{ddh}}, \mathbb{G}] \quad (12.22)$$ for an efficient DDH adversary $\mathcal{B}_{\mathrm{ddh}}$ …

Game 3. We replace the line marked (1) in Fig. 12.3 with $$(1) \qquad \gamma \xleftarrow{R} \mathbb{Z}_q \setminus \{\alpha\beta\}$$ Since the statistical distance between the uniform distribution on all triples and the uniform distribution on all non-DH-triples is $1/q$ (see Exercise 10.7), it follows that: $$|\Pr[W_2] - \Pr[W_3]| \le \frac{1}{q}. \quad (12.23)$$

Game 4. We now play our “CR card”. Let us define $\mathit{Coll}_{u,v}(\hat{v}, \hat{w})$ to be true if $(\hat{v}, \hat{w}) \ne (v, w)$ and $H'(\hat{v}, \hat{w}) = H'(v, w)$, and to be false, otherwise. In this game, we “widen” the rejection rule at line (5), replacing it with $$(5) \qquad \text{if } \mathit{Coll}_{u,v}(\hat{u}, \hat{v}) \text{ or } z' \ne f'(\hat{v}, \hat{w}, \hat{\rho})$$ Let $Z_4$ be the event that in Game 4, some decryption query, which would not have triggered the rejection rule of Game 3, does trigger the wider rejection rule in Game 4. Clearly, Games 3 and 4 proceed identically unless event $Z_4$ occurs. By the Difference Lemma, we have $$|\Pr[W_3] - \Pr[W_4]| \le \Pr[Z_4]. \quad (12.24)$$ It should be clear that $$\Pr[Z_4] \le \text{CRadv}[\mathcal{B}_{\mathrm{cr}}, H']. \quad (12.25)$$ for an efficient collision-finding adversary $\mathcal{B}_{\mathrm{cr}}$. Indeed, adversary $\mathcal{B}_{\mathrm{cr}}$ just plays Game 4 and waits for the event $Z_4$ to happen.

Verbatim from [BS23], Exercise 12.27 (printed pp. 521–522):

… Show that $\mathcal{E}_{\mathrm{MCS}}$ is CCA secure, provided $H'$ is collision resistant and the DDH assumption holds for $\mathbb{G}$.

Scope and Quantitative Adaptation

• Associated data specialized to $\mathcal{D} = \mathrm{Unit}$ and single-challenge 1CCA (Definition 12.2).
• Adaptation of Game 4 from $\mathcal{E}_{\mathrm{CS}}$ to $\mathcal{E}_{\mathrm{MCS}}$: in Theorem 12.9 ($\mathcal{E}_{\mathrm{CS}}$), $H'$ hashes the pair $(v, w)$ and $\mathit{Coll}_{u,v}(\hat{v}, \hat{w})$ tests $(\hat{v}, \hat{w}) \ne (v, w) \land H'(\hat{v}, \hat{w}) = H'(v, w)$. In Multiplicative Cramer–Shoup $\mathcal{E}_{\mathrm{MCS}}$ (Exercise 12.27, printed pp. 521–522, with $\mathcal{D} = \mathrm{Unit}$), $H'$ hashes the triple $(v, w, e) \in \mathbb{G}^3$ (encBits3), so the Game 4 collision predicate is originally adapted to $(\hat{v}, \hat{w}, \hat{e}) \ne (v, w, e) \land H'(\hat{v}, \hat{w}, \hat{e}) = H'(v, w, e)$ (while Phase 2 decryption already rejects the full challenge ciphertext $(\hat{v}, \hat{w}, \hat{e}, \hat{z}') = (v, w, e, z')$).
• Ideal exact-uniform PMF games vs. native Encryption.INDCCA2On: cramerShoupMsgCCA2Game, cramerShoupGroupCCA2Game, cramerShoupGroupINDCCA2, cramerShoupCCA2Game, and cramerShoupINDCCA2 are ideal exact-uniform PMF 1CCA experiments and security definitions, in which the challenger samples exponents from PMF.uniformOfFintype (ZMod (F.order d)). In advantage_cramerShoupGroupCCA2Game_le (an original quantitative adaptation of (12.19) to $\mathcal{E}_{\mathrm{MCS}}$ in the uniform strict-PPT model), the two fixed-bit DDH distinguishers (cramerShoupToDDHDistinguisher) and two fixed-bit collision finders (cramerShoupToCollisionFinder) contribute 42 / 2 ^ n from their internal sampleModNat exponent draws, and (2 * Q₁ n + 2 * Q₂ n + 2) / m combines the non-DH triple exclusion (1 / m) and the adaptive Lemma 12.8 bound ((Q₁ n + Q₂ n) / m) across bit = false and bit = true. The native strict-PPT security theorem DDH.indcca2On_cramerShoup instantiates Encryption.INDCCA2On (Complexity/Crypto/Computational/Encryption/CCA.lean), bridging from cramerShoupKeyGenProb and cramerShoupEncryptProb to the ideal game via advantage_cca2GameOn_cramerShoupGroupCCA2Game_le with an additional 8 / 2 ^ n statistical loss per challenge bit (16 / 2 ^ n across both bits).
• Group-order growth premise: the asymptotic theorems (DDH.cramerShoupMsgINDCCA2, DDH.cramerShoupGroupINDCCA2, DDH.cramerShoupINDCCA2, and DDH.indcca2On_cramerShoup) assume a positive lower bound m : ℕ → ℕ on the group order F.order with Negligible (fun n => (1 / m n : ℝ≥0)) so that the information-theoretic projective-hash and non-DH-triple terms (2 * Q₁ n + 2 * Q₂ n + 2) / m n are negligible for polynomial query bounds Q₁, Q₂.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupMsgCCA2Game (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (adversary : Encryption.CCA2AdversaryOf Msg) (bit : Bool) (n : ℕ) : Game

The ideal exact-uniform PMF single-challenge 1CCA experiment for Multiplicative Cramer–Shoup parameterized by a message-to-group-word encoding encodeMsg : F.Desc × Msg → List Bool ([BS23], Section 12.1, Attack Game 12.1 and Definition 12.2, printed pp. 467–468, and Exercise 12.27, printed pp. 521–522, specialized to associated data $\mathcal{D} = \mathrm{Unit}$; Game 0 of Section 12.5.3, printed pp. 490–491). Key and challenge exponents are sampled from the exact uniform distribution PMF.uniformOfFintype (ZMod (F.order d)).

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupGroupCCA2Game (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (adversary : Encryption.WordCCA2Adversary) (bit : Bool) (n : ℕ) : Game

The ideal exact-uniform PMF single-challenge 1CCA experiment for Multiplicative Cramer–Shoup over encoded group-element messages (Msg = List Bool, encodeMsg = Prod.snd), enforcing the group-membership challenge admissibility check isElem (d, m₀) && isElem (d, m₁).

def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupGroupINDCCA2 (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) : Prop

Ideal exact-uniform PMF single-challenge 1CCA security of Multiplicative Cramer–Shoup over encoded group-element messages (WordCCA2Adversary).

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupCCA2Game (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (adversary : Encryption.CCA2Adversary) (bit : Bool) (n : ℕ) : Game

The ideal exact-uniform PMF single-challenge 1CCA experiment for Multiplicative Cramer–Shoup over single-bit messages (Msg = Bool, embedded into F.Carrier d via F.encodeBit).

def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupINDCCA2 (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) : Prop

Ideal exact-uniform PMF single-challenge 1CCA security of Multiplicative Cramer–Shoup over single-bit messages (CCA2Adversary).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupGame1 (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (adversary : Encryption.CCA2AdversaryOf Msg) (bit : Bool) (n : ℕ) : Game

Game 1 ([BS23], Section 12.5.3, printed p. 490, adapted to $\mathcal{E}_{\mathrm{MCS}}$): draw (α, β) and sk uniformly from ZMod q, and compute the challenge ciphertext from (v, w) = (β • g, (α * β) • g) using the secret key via encodeCramerShoupChallenge.

theorem Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupMsgCCA2Game_eq_game1 (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (adversary : Encryption.CCA2AdversaryOf Msg) (bit : Bool) (n : ℕ) : F.cramerShoupMsgCCA2Game encodeMsg setup H isElem adversary bit n = F.cramerShoupGame1 encodeMsg setup H isElem adversary bit n

Game 0 = Game 1 ([BS23], Section 12.5.3, equation (12.21), printed p. 490): computing the challenge ciphertext from (v, w) = (β • g, (α * β) • g) using the secret key produces the exact same distribution as public-key encryption.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.cramerShoupGame2 (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (adversary : Encryption.CCA2AdversaryOf Msg) (bit : Bool) (n : ℕ) : Game

Game 2 ([BS23], Section 12.5.3, printed p. 490, adapted to $\mathcal{E}_{\mathrm{MCS}}$): replace the Diffie–Hellman challenge pair (v, w) = (β • g, (α * β) • g) by an independent random pair (v, w) = (β • g, γ • g) with uniform γ : ZMod (F.order d).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_cramerShoupGame1_game2_le (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (adversary : Encryption.CCA2AdversaryOf Msg) (bit : Bool) (n : ℕ) : (F.cramerShoupGame1 encodeMsg setup H isElem adversary bit n).advantage (F.cramerShoupGame2 encodeMsg setup H isElem adversary bit n) ≤ (F.ddhRealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary bit) n).advantage (F.ddhIdealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary bit) n) + 12 / 2 ^ n

Game 1 $\to$ Game 2 bound ([BS23], Section 12.5.3, equation (12.22), printed p. 492): the distinguishing advantage between cramerShoupGame1 and cramerShoupGame2 is at most the DDH advantage of cramerShoupMsgToDDHDistinguisher plus 12 / 2 ^ n (six approximate sampleModNat secret-key exponent draws in ddhRealGame and six in ddhIdealGame).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_cramerShoupGame2_game3_le (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (adversary : Encryption.CCA2AdversaryOf Msg) (bit : Bool) (n : ℕ) : (F.cramerShoupGame2 encodeMsg setup H isElem adversary bit n).advantage (F.cramerShoupGame3 encodeMsg setup H isElem adversary bit n) ≤ (collisionGameFor setup (F.cramerShoupHashMod H) (fun (x : ℕ) (x_1 : F.Desc) (x_2 : List Bool) => true) (F.cramerShoupMsgToCollisionFinder encodeMsg H isElem adversary bit) n).succProbability + 9 / 2 ^ n

Game 2 $\to$ Game 3 bound ([BS23], Section 12.5.3, equations (12.24)–(12.25), printed p. 492, adapted to $\mathcal{E}_{\mathrm{MCS}}$): the distinguishing advantage between cramerShoupGame2 and cramerShoupGame3 is bounded by the collision-finding success probability of cramerShoupMsgToCollisionFinder plus 9 / 2 ^ n (from the nine approximate sampleModNat exponent draws in cramerShoupMsgToCollisionFinder).

Concrete and asymptotic 1CCA security bounds ([BS23], Theorem 12.9 & Ex. 12.27)

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_cramerShoupMsgCCA2Game_game5_le (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (adversary : Encryption.CCA2AdversaryOf Msg) (bit : Bool) (n Q₁ Q₂ m : ℕ) (hm0 : 0 < m) (hm : ∀ d ∈ (setup n).support, m ≤ F.order d) (hQ₁ : F.HonestPhase1QueryBound setup adversary n Q₁) (hQ₂ : F.HonestPhase2QueryBound setup H isElem adversary n Q₂) : (F.cramerShoupMsgCCA2Game encodeMsg setup H isElem adversary bit n).advantage (F.cramerShoupGame5 encodeMsg setup H isElem adversary bit n) ≤ (F.ddhRealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary bit) n).advantage (F.ddhIdealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary bit) n) + (collisionGameFor setup (F.cramerShoupHashMod H) (fun (x : ℕ) (x_1 : F.Desc) (x_2 : List Bool) => true) (F.cramerShoupMsgToCollisionFinder encodeMsg H isElem adversary bit) n).succProbability + ↑(Q₁ + Q₂ + 1) / ↑m + 21 / 2 ^ n

Combined Game 0 $\to$ Game 5 bound for a single challenge bit: under honest query bounds (Q₁, Q₂), the distinguishing advantage between cramerShoupMsgCCA2Game and cramerShoupGame5 is at most the DDH advantage of cramerShoupMsgToDDHDistinguisher plus the collision-finding success probability of cramerShoupMsgToCollisionFinder plus (Q₁ + Q₂ + 1) / m + 21 / 2 ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_cramerShoupMsgCCA2Game_le_of_honest_bounds (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (adversary : Encryption.CCA2AdversaryOf Msg) (n Q₁ Q₂ m : ℕ) (hm0 : 0 < m) (hm : ∀ d ∈ (setup n).support, m ≤ F.order d) (hQ₁ : F.HonestPhase1QueryBound setup adversary n Q₁) (hQ₂ : F.HonestPhase2QueryBound setup H isElem adversary n Q₂) : (F.cramerShoupMsgCCA2Game encodeMsg setup H isElem adversary false n).advantage (F.cramerShoupMsgCCA2Game encodeMsg setup H isElem adversary true n) ≤ (F.ddhRealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary false) n).advantage (F.ddhIdealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary false) n) + (F.ddhRealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary true) n).advantage (F.ddhIdealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary true) n) + (collisionGameFor setup (F.cramerShoupHashMod H) (fun (x : ℕ) (x_1 : F.Desc) (x_2 : List Bool) => true) (F.cramerShoupMsgToCollisionFinder encodeMsg H isElem adversary false) n).succProbability + (collisionGameFor setup (F.cramerShoupHashMod H) (fun (x : ℕ) (x_1 : F.Desc) (x_2 : List Bool) => true) (F.cramerShoupMsgToCollisionFinder encodeMsg H isElem adversary true) n).succProbability + ↑(2 * Q₁ + 2 * Q₂ + 2) / ↑m + 42 / 2 ^ n

Concrete ideal-game 1CCA security bound under honest query bounds: combining the Game 0 $\to$ Game 5 bounds for bit = false and bit = true via cramerShoupGame5_false_eq_true (where 42 / 2 ^ n is the reduction loss from the sampleModNat exponent draws inside the reductions).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_cramerShoupMsgCCA2Game_le (F : PrimeOrderGroupFamily) {Msg : Type} (encodeMsg : F.Desc × Msg → List Bool) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (adversary : Encryption.CCA2AdversaryOf Msg) (Q₁ Q₂ : ℕ → ℕ) (hQ : adversary.IsQueryBounded Q₁ Q₂) (n m : ℕ) (hm0 : 0 < m) (hm : ∀ d ∈ (setup n).support, m ≤ F.order d) : (F.cramerShoupMsgCCA2Game encodeMsg setup H isElem adversary false n).advantage (F.cramerShoupMsgCCA2Game encodeMsg setup H isElem adversary true n) ≤ (F.ddhRealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary false) n).advantage (F.ddhIdealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary false) n) + (F.ddhRealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary true) n).advantage (F.ddhIdealGame setup (F.cramerShoupMsgToDDHDistinguisher encodeMsg H isElem adversary true) n) + (collisionGameFor setup (F.cramerShoupHashMod H) (fun (x : ℕ) (x_1 : F.Desc) (x_2 : List Bool) => true) (F.cramerShoupMsgToCollisionFinder encodeMsg H isElem adversary false) n).succProbability + (collisionGameFor setup (F.cramerShoupHashMod H) (fun (x : ℕ) (x_1 : F.Desc) (x_2 : List Bool) => true) (F.cramerShoupMsgToCollisionFinder encodeMsg H isElem adversary true) n).succProbability + ↑(2 * Q₁ n + 2 * Q₂ n + 2) / ↑m + 42 / 2 ^ n

Concrete ideal-game 1CCA security bound for cramerShoupMsgCCA2Game: for any adversary with decryption-query bounds (Q₁ n, Q₂ n), the ideal 1CCA advantage at parameter n is bounded by the DDH advantages of cramerShoupMsgToDDHDistinguisher (false and true), the collision-finding success probabilities of cramerShoupMsgToCollisionFinder (false and true), plus (2 * Q₁ n + 2 * Q₂ n + 2) / m + 42 / 2 ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_cramerShoupGroupCCA2Game_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (adversary : Encryption.WordCCA2Adversary) (Q₁ Q₂ : ℕ → ℕ) (hQ : Encryption.CCA2AdversaryOf.IsQueryBounded adversary Q₁ Q₂) (n m : ℕ) (hm0 : 0 < m) (hm : ∀ d ∈ (setup n).support, m ≤ F.order d) : (F.cramerShoupGroupCCA2Game setup H isElem adversary false n).advantage (F.cramerShoupGroupCCA2Game setup H isElem adversary true n) ≤ (F.ddhRealGame setup (F.cramerShoupToDDHDistinguisher H isElem adversary false) n).advantage (F.ddhIdealGame setup (F.cramerShoupToDDHDistinguisher H isElem adversary false) n) + (F.ddhRealGame setup (F.cramerShoupToDDHDistinguisher H isElem adversary true) n).advantage (F.ddhIdealGame setup (F.cramerShoupToDDHDistinguisher H isElem adversary true) n) + (collisionGameFor setup (F.cramerShoupHashMod H) (fun (x : ℕ) (x_1 : F.Desc) (x_2 : List Bool) => true) (F.cramerShoupToCollisionFinder H isElem adversary false) n).succProbability + (collisionGameFor setup (F.cramerShoupHashMod H) (fun (x : ℕ) (x_1 : F.Desc) (x_2 : List Bool) => true) (F.cramerShoupToCollisionFinder H isElem adversary true) n).succProbability + ↑(2 * Q₁ n + 2 * Q₂ n + 2) / ↑m + 42 / 2 ^ n

Theorem 12.9 & Exercise 12.27 concrete ideal-game bound (group-element messages) ([BS23], Section 12.5.3, Theorem 12.9 and Remark 12.3, printed pp. 488–493, and Exercise 12.27, printed pp. 521–522): original adaptation of the concrete bound (12.19) to the ideal exact-uniform PMF 1CCA game cramerShoupGroupCCA2Game for Multiplicative Cramer–Shoup $\mathcal{E}_{\mathrm{MCS}}$ in the two-run single-bit reduction style (with 42 / 2 ^ n from the approximate sampleModNat exponent draws in the reductions).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_cramerShoupCCA2Game_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (adversary : Encryption.CCA2Adversary) (Q₁ Q₂ : ℕ → ℕ) (hQ : Encryption.CCA2AdversaryOf.IsQueryBounded adversary Q₁ Q₂) (n m : ℕ) (hm0 : 0 < m) (hm : ∀ d ∈ (setup n).support, m ≤ F.order d) : (F.cramerShoupCCA2Game setup H isElem adversary false n).advantage (F.cramerShoupCCA2Game setup H isElem adversary true n) ≤ (F.ddhRealGame setup (F.cramerShoupMsgToDDHDistinguisher (fun (p : F.Desc × Bool) => F.encodeBit p.1 p.2) H isElem adversary false) n).advantage (F.ddhIdealGame setup (F.cramerShoupMsgToDDHDistinguisher (fun (p : F.Desc × Bool) => F.encodeBit p.1 p.2) H isElem adversary false) n) + (F.ddhRealGame setup (F.cramerShoupMsgToDDHDistinguisher (fun (p : F.Desc × Bool) => F.encodeBit p.1 p.2) H isElem adversary true) n).advantage (F.ddhIdealGame setup (F.cramerShoupMsgToDDHDistinguisher (fun (p : F.Desc × Bool) => F.encodeBit p.1 p.2) H isElem adversary true) n) + (collisionGameFor setup (F.cramerShoupHashMod H) (fun (x : ℕ) (x_1 : F.Desc) (x_2 : List Bool) => true) (F.cramerShoupMsgToCollisionFinder (fun (p : F.Desc × Bool) => F.encodeBit p.1 p.2) H isElem adversary false) n).succProbability + (collisionGameFor setup (F.cramerShoupHashMod H) (fun (x : ℕ) (x_1 : F.Desc) (x_2 : List Bool) => true) (F.cramerShoupMsgToCollisionFinder (fun (p : F.Desc × Bool) => F.encodeBit p.1 p.2) H isElem adversary true) n).succProbability + ↑(2 * Q₁ n + 2 * Q₂ n + 2) / ↑m + 42 / 2 ^ n

Concrete ideal-game 1CCA security bound for single-bit messages (cramerShoupCCA2Game).

Polynomial length bounds and asymptotic 1CCA security

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.cramerShoupMsgINDCCA2 {F : PrimeOrderGroupFamily} {Msg : Type} {encMsg : Msg ↪ List Bool} {encodeMsg : F.Desc × Msg → List Bool} (hencMsg : Turing.MultiTapeTM.ComputableInPolyTime encodeMsg (Turing.MultiTapeTM.encPair F.encDesc encMsg) Turing.MultiTapeTM.encBits) {setup : ℕ → PMF F.Desc} {H : F.Desc × List Bool → List Bool} {isElem : F.Desc × List Bool → Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hisElem : Turing.MultiTapeTM.ComputableInPolyTime isElem (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (hDDH : F.DDH setup) (hCR : CollisionResistantFor F.encDesc setup (F.cramerShoupHashMod H)) {m : ℕ → ℕ} (hm0 : ∀ (n : ℕ), 0 < m n) (hm : ∀ (n : ℕ), ∀ d ∈ (setup n).support, m n ≤ F.order d) (hinv : Negligible fun (n : ℕ) => 1 / ↑(m n)) (hdesc : ∃ (c : ℕ) (k : ℕ), ∀ (n : ℕ), ∀ d ∈ (setup n).support, (F.encDesc d).length ≤ c * (n + 1) ^ k) : Game.Indistinguishable (fun (adversary : Encryption.CCA2AdversaryOf Msg) (n : ℕ) => F.cramerShoupMsgCCA2Game encodeMsg setup H isElem adversary false n) (fun (adversary : Encryption.CCA2AdversaryOf Msg) (n : ℕ) => F.cramerShoupMsgCCA2Game encodeMsg setup H isElem adversary true n) (Encryption.CCA2AdversaryOf.IsPPT encMsg)

Asymptotic ideal-game 1CCA security of Multiplicative Cramer–Shoup for a general message encoding ([BS23], Theorem 12.9 & Exercise 12.27, printed pp. 488–493, 521–522): if DDH holds for setup, cramerShoupHashMod H is collision-resistant for setup, every supported group at parameter n has order at least m n > 0 with 1 / m n negligible, and supported group descriptions have polynomially bounded bit-length, then the ideal exact-uniform PMF game cramerShoupMsgCCA2Game is indistinguishable between bit = false and bit = true against all strict oracle PPT adversaries.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.cramerShoupGroupINDCCA2 {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} {H : F.Desc × List Bool → List Bool} {isElem : F.Desc × List Bool → Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hisElem : Turing.MultiTapeTM.ComputableInPolyTime isElem (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (hDDH : F.DDH setup) (hCR : CollisionResistantFor F.encDesc setup (F.cramerShoupHashMod H)) {m : ℕ → ℕ} (hm0 : ∀ (n : ℕ), 0 < m n) (hm : ∀ (n : ℕ), ∀ d ∈ (setup n).support, m n ≤ F.order d) (hinv : Negligible fun (n : ℕ) => 1 / ↑(m n)) (hdesc : ∃ (c : ℕ) (k : ℕ), ∀ (n : ℕ), ∀ d ∈ (setup n).support, (F.encDesc d).length ≤ c * (n + 1) ^ k) : F.cramerShoupGroupINDCCA2 setup H isElem

Theorem 12.9 & Exercise 12.27 (asymptotic ideal-game 1CCA security for group-element messages): Multiplicative Cramer–Shoup satisfies the ideal exact-uniform PMF 1CCA notion cramerShoupGroupINDCCA2 under DDH, collision resistance of cramerShoupHashMod H, a positive group-order lower bound m n > 0 with 1 / m n negligible, and polynomially bounded group description bit-length.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.cramerShoupINDCCA2 {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} {H : F.Desc × List Bool → List Bool} {isElem : F.Desc × List Bool → Bool} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hisElem : Turing.MultiTapeTM.ComputableInPolyTime isElem (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (hDDH : F.DDH setup) (hCR : CollisionResistantFor F.encDesc setup (F.cramerShoupHashMod H)) {m : ℕ → ℕ} (hm0 : ∀ (n : ℕ), 0 < m n) (hm : ∀ (n : ℕ), ∀ d ∈ (setup n).support, m n ≤ F.order d) (hinv : Negligible fun (n : ℕ) => 1 / ↑(m n)) (hdesc : ∃ (c : ℕ) (k : ℕ), ∀ (n : ℕ), ∀ d ∈ (setup n).support, (F.encDesc d).length ≤ c * (n + 1) ^ k) : F.cramerShoupINDCCA2 setup H isElem

Asymptotic ideal-game 1CCA security for single-bit messages (cramerShoupINDCCA2): Multiplicative Cramer–Shoup with bit embedding encodeBit satisfies the ideal exact-uniform PMF 1CCA notion cramerShoupINDCCA2 under DDH, collision resistance of cramerShoupHashMod H, a positive group-order lower bound m n > 0 with 1 / m n negligible, and polynomially bounded group description bit-length.

Encryption.cca2GameOn and Encryption.INDCCA2On instantiation

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_cca2GameOn_cramerShoupGroupCCA2Game_le (F : PrimeOrderGroupFamily) (H : F.Desc × List Bool → List Bool) (isElem : F.Desc × List Bool → Bool) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (d : ℕ → F.Desc) (adversary : Encryption.WordCCA2Adversary) (bit : Bool) (n : ℕ) : Game.advantage (Encryption.cca2GameOn (F.cramerShoupValid isElem d) Turing.MultiTapeTM.encBits (F.cramerShoupKeyGenProb d) (F.cramerShoupEncryptProb H d) (F.cramerShoupDecryptOpt H isElem d) adversary bit n).eval (F.cramerShoupGroupCCA2Game (fun (n : ℕ) => PMF.pure (d n)) H isElem adversary bit n) ≤ 8 / 2 ^ n

The native Encryption.cca2GameOn experiment for (cramerShoupValid, cramerShoupKeyGenProb, cramerShoupEncryptProb, cramerShoupDecryptOpt) is within statistical distance 8 / 2 ^ n of the ideal exact-uniform PMF game cramerShoupGroupCCA2Game (fun n => PMF.pure (d n)) (accounting for the eight sampleModNat exponent draws in cramerShoupKeyGenProb and cramerShoupEncryptProb).

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.indcca2On_cramerShoup {F : PrimeOrderGroupFamily} {H : F.Desc × List Bool → List Bool} {isElem : F.Desc × List Bool → Bool} {d : ℕ → F.Desc} (hH : Turing.MultiTapeTM.ComputableInPolyTime H (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hisElem : Turing.MultiTapeTM.ComputableInPolyTime isElem (Turing.MultiTapeTM.encPair F.encDesc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hd : Turing.MultiTapeTM.ComputableInPolyTime d Turing.MultiTapeTM.encUnary F.encDesc) (hmem : ∀ (d : F.Desc) (x : List Bool), isElem (d, x) = true ↔ x ∈ Set.range (F.encode d)) (hDDH : F.DDH fun (n : ℕ) => PMF.pure (d n)) (hCR : CollisionResistantFor F.encDesc (fun (n : ℕ) => PMF.pure (d n)) (F.cramerShoupHashMod H)) {m : ℕ → ℕ} (hm0 : ∀ (n : ℕ), 0 < m n) (hm : ∀ (n : ℕ), m n ≤ F.order (d n)) (hinv : Negligible fun (n : ℕ) => 1 / ↑(m n)) : Encryption.INDCCA2On (F.cramerShoupValid isElem d) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits (F.cramerShoupKeyGenProb d) (F.cramerShoupEncryptProb H d) (F.cramerShoupDecryptOpt H isElem d)

Theorem 12.9 & Exercise 12.27 via Encryption.INDCCA2On: for any polynomial-time group description family d : ℕ → F.Desc, the probabilistic polynomial-time Cramer–Shoup encryption scheme (cramerShoupKeyGenProb d, cramerShoupEncryptProb H d, cramerShoupDecryptOpt H isElem d) satisfies the native Encryption.INDCCA2On notion with respect to the group-membership admissibility predicate cramerShoupValid isElem d under DDH, collision resistance of cramerShoupHashMod H, and a positive group-order lower bound m n > 0 with 1 / m n negligible.