Multiplicative Cramer–Shoup Encryption Scheme and Adaptive Projective-Hash Rejection #

This module formalizes the Multiplicative Cramer–Shoup public-key encryption scheme ($\mathcal{E}_{\mathrm{MCS}}$, Boneh and Shoup, Section 12.5.3 and Exercise 12.27, printed pp. 488–493, 521–522, specialized to associated data $\mathcal{D} = \mathrm{Unit}$) over a PrimeOrderGroupFamily, proves its algebraic and word-level decryption correctness and polynomial-time computability certificates, and establishes the adaptive Lemma 12.8 projective-hash rejection bound and Lemma 12.6 one-time group-mask challenge blindness (Games 3 $\to$ 3.5 $\to$ 4 $\to$ 5 of Theorem 12.9, printed pp. 492–493) against an adaptive CCA2AdversaryOf Msg. Groups are written additively as ZMod (F.order d)-modules (matching DiscreteLog, DiffieHellman, ElGamal, and ProjectiveHash).

Source Statements ([BS23], Sections 12.5.1–12.5.3 & Exercise 12.27) #

Verbatim from [BS23], Sections 12.5.1–12.5.2 (Lemma 12.6 in §12.5.1, printed p. 486; Lemma 12.8 in §12.5.2, printed p. 488):

Lemma 12.6. In Attack Game 12.4, $\Pr[W_0] = \Pr[W_1]$ for all adversaries $\mathcal{A}$. … Lemma 12.8. In Attack Game 12.5, for any adversary $\mathcal{A}$ that outputs at most $Q$ tuples, the probability that it wins is at most $Q/q$.

Verbatim from [BS23], Section 12.5.3 (printed pp. 488–493):

the key generation algorithm runs as follows: $$\begin{aligned} G() :=\quad & \alpha \xleftarrow{R} \mathbb{Z}_q,\; u \leftarrow g^\alpha,\; \sigma, \tau \xleftarrow{R} \mathbb{Z}_q,\; h \leftarrow g^\sigma u^\tau \\ & \sigma_1, \tau_1, \sigma_2, \tau_2 \xleftarrow{R} \mathbb{Z}_q,\; h_1 \leftarrow g^{\sigma_1} u^{\tau_1},\; h_2 \leftarrow g^{\sigma_2} u^{\tau_2} \\ & pk \leftarrow (u, h, h_1, h_2),\; sk \leftarrow (\sigma, \tau, \sigma_1, \tau_1, \sigma_2, \tau_2),\; \text{output } (pk, sk); \end{aligned}$$ … Game 5. We again widen the rejection rule at line (5), replacing it with: $$(5) \qquad \text{if } \hat{v}^\alpha \ne \hat{w} \text{ or } \mathit{Coll}_{u,v}(\hat{u}, \hat{v}) \text{ or } z' \ne f'(\hat{v}, \hat{w}, \hat{\rho})$$ So this rule will reject the ciphertext if $(\hat{v}, \hat{w}) \notin L_u$. Let $Z_5$ be the event that in Game 5, some decryption query, which would not have triggered the rejection rule of Game 4, does trigger the wider rejection rule in Game 5. Clearly, Games 4 and 5 proceed identically unless event $Z_5$ occurs. By the Difference Lemma, we have $$|\Pr[W_4] - \Pr[W_5]| \le \Pr[Z_5]. \quad (12.26)$$ We will argue that $\Pr[Z_5] \le Q_d / q$. $(12.27)$ … Game 6. Everything we did so far was leading to this point, which is the crux of the proof. We replace line (2) in Fig. 12.3 with $z \xleftarrow{R} \mathbb{G}$. We claim that $\Pr[W_6] = \Pr[W_5]$. $(12.28)$ This follows from Lemma 12.6, and the fact that in processing decryption queries in Game 5, we only need to evaluate $f(\hat{v}, \hat{w})$ at points $(\hat{v}, \hat{w}) \in L_u$. … Remark 12.3 (Group membership verification). For reasons similar to that discussed in Remark 12.1, it is essential that given a ciphertext $(v, w, z', c)$, the decryption algorithm for $\mathcal{E}_{\mathrm{CS}}$ verifies that $v$ and $w$ are in $\mathbb{G}$. It is not necessary to explicitly check that $z'$ is in $\mathbb{G}$, since the check that $v^{\sigma_1 + \rho \sigma_2} w^{\tau_1 + \rho \tau_2} = z'$ implies that $z'$ is in $\mathbb{G}$.

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

12.27 (Multiplicative Cramer-Shoup encryption). Consider the following multiplicative version of the Cramer-Shoup encryption scheme (presented in Section 12.5) that supports associated data (see Section 12.7) coming from a set $\mathcal{D}$. Let $\mathbb{G}$ be a cyclic group of prime order $q$ with generator $g \in \mathbb{G}$. Let $H' : \mathbb{G}^3 \times \mathcal{D} \to \mathbb{Z}_q$ be a hash function. The encryption scheme $\mathcal{E}_{\mathrm{MCS}} = (G, E, D)$ is defined over $(\mathbb{G}, \mathcal{D}, \mathbb{G}^4)$ as follows. Key generation is exactly as in $\mathcal{E}_{\mathrm{CS}}$. For a given public key $pk = (u, h, h_1, h_2) \in \mathbb{G}^4$ message $m \in \mathbb{G}$, and associated data $d \in \mathcal{D}$, the encryption algorithm runs as follows: $$E(pk, m, d) := \beta \xleftarrow{R} \mathbb{Z}_q,\; v \leftarrow g^\beta,\; w \leftarrow u^\beta,\; e \leftarrow h^\beta \cdot m,\; \rho \leftarrow H'(v, w, e, d),\; z' \leftarrow (h_1 h_2^\rho)^\beta,\; \text{output } (v, w, e, z').$$ For a given secret key $sk = (\sigma, \tau, \sigma_1, \tau_1, \sigma_2, \tau_2) \in \mathbb{Z}_q^6$ and a ciphertext $(v, w, e, z') \in \mathbb{G}^4$, and associated data $d \in \mathcal{D}$, the decryption algorithm runs as follows: $$D(sk, (v, w, e, z', d)) := \rho \leftarrow H'(v, w, e, d);\; \text{if } v^{\sigma_1 + \rho \sigma_2} w^{\tau_1 + \rho \tau_2} = z' \text{ then output } e / (v^\sigma w^\tau) \text{ else output reject}.$$ Show that $\mathcal{E}_{\mathrm{MCS}}$ is CCA secure, provided $H'$ is collision resistant and the DDH assumption holds for $\mathbb{G}$.

Existing Notions Considered #

Cslib.Crypto.PrimeOrderGroupFamily (DiffieHellman.lean) and ElGamal (ElGamal.lean): reused for group descriptions, carriers, generators, encodings, and word-level group operations.
Cslib.Crypto.ProjectiveHash (Complexity/Crypto/Computational/CramerShoup/ProjectiveHash.lean): reused for projHash, projHashAux, projHash2, projHash2Aux, fiber identities, projHashFiberEquiv, projHash2QueryFiberEquiv, and uniform_projHash_fiber_add.
Cslib.Crypto.Encryption.CCA2AdversaryOf (Complexity/Crypto/Computational/Encryption/CCA.lean) and Cslib.Crypto.isCollisionFor (CollisionResistant.lean): reused for adaptive 1CCA adversaries and Phase 2 hash collisions in ZMod (F.order d).
Cslib.Crypto.Game (Game.lean, Complexity/Crypto/Game/UntilBad.lean): reused for runStatelessOracle, advantage_runStatelessOracle_bind_le, bind_runStatelessOracle_comm, advantage_runStatelessOracle_le_of_support, advantage_bind_le_nnreal, advantage_bind_le_of_support, advantage_bind_comm, and advantage_uniform_bind_of_eq_of_ne.

Main definitions and results #

cramerShoupHashMod, cramerShoupPublicKey, cramerShoupEncrypt, cramerShoupDecrypt, encodeCramerShoupPublicKey, encodeCramerShoupEncrypt, encodeCramerShoupChallenge, decodeCramerShoup: algebraic and word-level Multiplicative Cramer–Shoup operations.
cramerShoupDecrypt_cramerShoupEncrypt, decodeCramerShoup_encode, decodeCramerShoup_cramerShoupEncrypt, computableInPolyTime_encodeCramerShoupPublicKey, computableInPolyTime_encodeCramerShoupEncrypt, computableInPolyTime_encodeCramerShoupChallenge, computableInPolyTime_decodeCramerShoup: decryption correctness and polynomial-time computability certificates.
cramerShoupGame3, cramerShoupGame3Half, cramerShoupGame4, cramerShoupGame5, advantage_cramerShoupGame3_game3Half_le, advantage_cramerShoupGame3Half_game4_le, advantage_cramerShoupGame3_game4_le, cramerShoupGame5_false_eq_true, advantage_cramerShoupGame4_game5_le: the adaptive Lemma 12.8 projective-hash rejection bounds (Q₁ / m, Q₂ / m, (Q₁ + Q₂) / m) and Lemma 12.6 one-time group-mask bound (1 / m).

Multiplicative Cramer–Shoup Encryption Scheme and Adaptive Projective-Hash Rejection #

Source Statements ([BS23], Sections 12.5.1–12.5.3 & Exercise 12.27) #

Existing Notions Considered #

Main definitions and results #

Framing for 3-tuples and 4-tuples of bit strings #

Algebraic Multiplicative Cramer–Shoup ([BS23], Section 12.5.3 & Exercise 12.27) #

Word-level polynomial-time Cramer–Shoup operations #

Polynomial-time certificates for word-level operations #

Collision detection and decryption oracle replies #

Canonical secret-key conversion and hybrid Games 3–5 #

Projective-hash rejection (Games 3.5, 4, and 5) and concrete 1CCA bound #