Universal and $\text{universal}_2$ projective hash functions over prime-order groups #

This module formalizes the universal and $\text{universal}_2$ projective hash families over a PrimeOrderGroupFamily from Boneh and Shoup, Sections 12.5.1–12.5.2, printed pp. 484–488, which form the algebraic core of the Cramer–Shoup public-key encryption scheme (Section 12.5.3 and Exercise 12.27).

Groups are written additively as ZMod (F.order d)-modules (matching DiscreteLog, DiffieHellman, and ElGamal), so the book's $v^\sigma w^\tau$ is $\sigma \bullet v + \tau \bullet w$.

Source Statements ([BS23], Sections 12.5.1–12.5.2, printed pp. 485–488) #

Verbatim from [BS23], Section 12.5.1 (printed p. 485):

The function $f := f_{\sigma, \tau}$ is indexed by randomly chosen $\sigma, \tau \in \mathbb{Z}_q$, and is defined as follows: $$f_{\sigma, \tau} : \mathbb{G}^2 \to \mathbb{G}, \quad (v, w) \mapsto v^\sigma w^\tau. \quad (12.13)$$ The auxiliary information $h$ that defines $f$ on $L_u$ is $$h := f(g, u) = g^\sigma u^\tau. \quad (12.14)$$ … Lemma 12.5. Suppose $\sigma$ and $\tau$ are uniformly and independently distributed over $\mathbb{Z}_q$. Then for all $u, v, w, h, z \in \mathbb{G}$, if $(u, v, w)$ is not a DH-triple, then $$\Pr[g^\sigma u^\tau = h \land v^\sigma w^\tau = z] = \frac{1}{q^2}.$$

Verbatim from [BS23], Section 12.5.2 (printed pp. 487–488):

We define a new function $f' := f'_{\sigma_1, \tau_1, \sigma_2, \tau_2}$, indexed by randomly chosen $\sigma_1, \tau_1, \sigma_2, \tau_2 \in \mathbb{Z}_q$, as follows $$f'_{\sigma_1, \tau_1, \sigma_2, \tau_2} : \mathbb{G}^2 \times \mathbb{Z}_q \to \mathbb{G}, \quad (v, w, \rho) \mapsto f_{\sigma_1, \tau_1}(v, w) \cdot f_{\sigma_2, \tau_2}(v, w)^\rho = v^{\sigma_1 + \rho \sigma_2} w^{\tau_1 + \rho \tau_2}. \quad (12.16)$$ The auxiliary information that defines $f'$ on $L_u \times \mathbb{Z}_q$ is $h' := (h_1, h_2)$, where $h_i$ is the auxiliary information that defines $f_{\sigma_i, \tau_i}$ on $L_u$; that is $$h_i := f_{\sigma_i, \tau_i}(g, u) = g^{\sigma_i} u^{\tau_i} \quad \text{for } i = 1, 2. \quad (12.17)$$ … Lemma 12.7. Suppose $\sigma_1, \tau_1, \sigma_2, \tau_2$ are uniformly and independently distributed over $\mathbb{Z}_q$. Then for all $u, v, w, \hat{v}, \hat{w}, h_1, h_2, z, \hat{z} \in \mathbb{G}$ and all $\rho, \hat{\rho} \in \mathbb{Z}_q$, if $(u, v, w)$ and $(u, \hat{v}, \hat{w})$ are not DH-triples, and $\rho \ne \hat{\rho}$, then $$\Pr[g^{\sigma_1} u^{\tau_1} = h_1 \land g^{\sigma_2} u^{\tau_2} = h_2 \land v^{\sigma_1 + \rho_1 \sigma_2} w^{\tau_1 + \rho_1 \tau_2} = z \land \hat{v}^{\sigma_1 + \rho_2 \sigma_2} \hat{w}^{\tau_1 + \rho_2 \tau_2} = \hat{z}] = \frac{1}{q^4}.$$ … 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$.

Attack Game 12.5 itself is not formalized as a standalone game here; instead, this module proves the explicit change-of-variables equivalences (projHashFiberChangeEquiv, projHash2FiberChangeEquiv), the single-tuple 1 / q hit law (uniform_projHash2_fiber_apply), and the finite-list Q / q union bound (uniform_projHash2_fiber_any_le) on the τ₂-fiber given δ₁ = σ₁ + α * τ₁, δ₂ = σ₂ + α * τ₂, and ξ = τ₁ + ρ * τ₂ (where (h₁, h₂, z) and all DH queries depend only on (δ₁, δ₂, ξ)). The adaptive decryption-oracle reduction for Cramer–Shoup using these ingredients is carried by Complexity/Crypto/Computational/CramerShoup.lean (PR 2).

Main definitions #

Cslib.Crypto.ProjectiveHash.projHash, Cslib.Crypto.ProjectiveHash.projHashAux: universal projective hash evaluation (12.13) and public projection (12.14).
Cslib.Crypto.ProjectiveHash.projHashFiberChangeEquiv, Cslib.Crypto.ProjectiveHash.projHashEquiv: fiber change-of-variables (δ, τ) ↦ (δ - α * τ, τ) and 2×2 linear equivalence on ZMod q × ZMod q underlying Lemma 12.5 when γ ≠ α * β.
Cslib.Crypto.ProjectiveHash.projHash2, Cslib.Crypto.ProjectiveHash.projHash2Aux: $\text{universal}_2$ projective hash evaluation (12.16) and public projection pair (12.17).
Cslib.Crypto.ProjectiveHash.projHash2FiberChangeEquiv, Cslib.Crypto.ProjectiveHash.projHash2Equiv: 4-tuple fiber change-of-variables ((δ₁, δ₂), (ξ, τ₂)) ↦ ((δ₁ - α * (ξ - ρ * τ₂), ξ - ρ * τ₂), (δ₂ - α * τ₂, τ₂)) and 4×4 linear equivalence on (ZMod q × ZMod q) × (ZMod q × ZMod q) underlying Lemma 12.7 when γ ≠ α * β, γ' ≠ α * β', and ρ' ≠ ρ.

Main results #

Cslib.Crypto.ProjectiveHash.projHash_smul_generator, Cslib.Crypto.ProjectiveHash.projHash2_smul_generator: projective evaluation on Diffie–Hellman triples (β • g, β • u) ∈ L_u via the public projections h and (h₁, h₂).
Cslib.Crypto.ProjectiveHash.projHash_bijective_of_ne, Cslib.Crypto.ProjectiveHash.uniform_projHash_apply_of_ne, Cslib.Crypto.ProjectiveHash.uniform_projHash_fiber, Cslib.Crypto.ProjectiveHash.uniform_projHash_fiber_add: Lemma 12.5 bijection and 1 / q ^ 2 joint point mass, together with conditional uniform masking on non-DH triples as a consequence of Lemma 12.5 under projHashFiberChangeEquiv.
Cslib.Crypto.ProjectiveHash.projHash2_fiber_eq, Cslib.Crypto.ProjectiveHash.projHash2_bijective_of_ne, Cslib.Crypto.ProjectiveHash.uniform_projHash2_apply_of_ne, Cslib.Crypto.ProjectiveHash.projHash2_fiber_bijective_of_ne, Cslib.Crypto.ProjectiveHash.uniform_projHash2_fiber_apply, Cslib.Crypto.ProjectiveHash.uniform_projHash2_fiber_any_le: Lemma 12.7 4-tuple bijection and 1 / q ^ 4 joint point mass, and the single-tuple 1 / q and Q-tuple Q / q union-bound ingredients of Lemma 12.8 (via Lemma 12.7) on the τ₂-fiber of projHash2FiberChangeEquiv for non-DH triples with ρ' ≠ ρ.

References #

D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Sections 12.5.1–12.5.2 (printed pp. 484–488).

Universal and $\text{universal}_2$ projective hash functions over prime-order groups #

Source Statements ([BS23], Sections 12.5.1–12.5.2, printed pp. 485–488) #

Main definitions #

Main results #

References #

Universal projective hash functions ([BS23], Section 12.5.1, printed p. 485) #

$\text{Universal}_2$ projective hash functions ([BS23], Section 12.5.2) #