Unconditionally Secure Key Derivation for Hashed ElGamal via the Leftover Hash Lemma #
In [BS23], Section 8.10.4 (Theorem 8.11, p. 334) and Section 11.5.2 (p. 449), a universal
hash function whose key is placed in the public system parameter yields an unconditionally secure
key derivation function (SecureKDF, Attack Game 11.3, pp. 448–449, and Definition 11.5, p. 449)
via the Leftover Hash Lemma, without any computational assumptions on the hash family.
- Paraphrase of [BS23], Section 8.10.4, Theorem 8.11 (p. 334, Leftover Hash Lemma): for a $(1 + \alpha)/N$-universal keyed hash function $H$ over $(\mathcal{K}, \mathcal{S}, \mathcal{T})$ with $N = |\mathcal{T}|$, if $k$ is uniform on $\mathcal{K}$ and $s_1, \dots, s_m$ are independent of $k$ and of each other with guessing/collision probability at most $\gamma$, the statistical distance $\delta$ between $(k, H(k, s_1), \dots, H(k, s_m))$ and the uniform distribution on $\mathcal{K} \times \mathcal{T}^m$ satisfies $\delta \le \frac{1}{2} m \sqrt{N \gamma + \alpha}$.
- Paraphrase of [BS23], Section 11.5.2, Attack Game 11.3 and Definition 11.5
(pp. 448–449): for $F : \mathcal{X} \times \mathcal{Y} \to \mathcal{Z}$, Experiment $b$ samples
$x \leftarrow \mathcal{X}$, $y \leftarrow \mathcal{Y}$, sets $z_0 = F(x, y)$, samples uniform
$z_1 \leftarrow \mathcal{Z}$, and passes $(x, z_b)$ to $\mathcal{A}$; $F$ is a secure KDF if
$|\Pr[W_0] - \Pr[W_1]|$ is negligible for every efficient adversary $\mathcal{A}$. As noted on
p. 449:
One may even build a secure KDF without making any assumptions at all: the construction in Section 8.10.4 based on a universal hash function and the leftover hash lemma yields an unconditionally secure KDF.
To formalize this over an arbitrary PrimeOrderGroupFamily:
PrimeOrderGroupFamily.withSeedaugments the public group descriptiond : F.Descwith a public bit-string seeds : List Bool, givingF.withSeed.Desc = F.Desc × List Bool. UnderPrimeOrderGroupFamily.seededSetup, given the sampled group descriptiond ← setup n,sis sampled uniformly from{0, 1}^{seedLen n d}conditional ond(and independently of the group exponents). WhenseedLenis polynomial-time computable in unary,DDH.withSeedtransfers theDDHassumption from(F, setup)to(F.withSeed, F.seededSetup setup seedLen).PrimeOrderGroupFamily.linearHashKDFpads the encoded group elementw : List Boolto the fixed self-delimiting width2 * bound d + 1viaCslib.BitString.padWord (bound d) wand hashes it with the public Boolean matrix seedsviaCslib.BitString.LinearHash.wordHash (keyLen d) s. BecausepadWordis injective on words of length at mostbound d(Cslib.BitString.word_eq_of_paddedBits_eq) andF.encode dis injective onF.Carrier d, a uniform group elementγ • gmaps injectively intoBitString (2 * bound d + 1)with collision probability(F.order d)⁻¹.- Applying the Leftover Hash Lemma for two-universal binary matrix hashing
(
Cslib.BitString.LinearHash.isTwoUniversal_flatandIsTwoUniversal.leftover_hash),advantage_kdfGame_linearHashKDF_lebounds the distinguishing advantage betweenkdfRealGameandkdfIdealGamefor every (even computationally unbounded) distinguisher byNNReal.sqrt ((2 : ℝ≥0) ^ (msgLen n) / (qMin : ℝ≥0)) / 2. Consequently,secureKDF_linearHashKDF,secureKDF_linearHashKDF_const,exists_secureKDF_withSeed, andDDH.negligible_hashedElGamalCPAGame_linearHashKDFyield non-degenerateSecureKDFand Hashed ElGamal instantiations for arbitrary positive key lengthsmsgLen n > 0whenever2 ^ (msgLen n) / qis negligible.
Main definitions #
Cslib.Crypto.PrimeOrderGroupFamily.withSeed: prime-order group family with a public hash seed in the description.Cslib.Crypto.PrimeOrderGroupFamily.seededSetup: setup distribution augmentingsetup nwith a bit-string seed sampled uniformly conditional on the sampled group description.Cslib.Crypto.PrimeOrderGroupFamily.seededDDHDistinguisher: DDH reduction that samples the public seed internally.Cslib.Crypto.PrimeOrderGroupFamily.linearHashKDF: polynomial-time key-derivation function built fromCslib.BitString.padWordandCslib.BitString.LinearHash.wordHash.Cslib.Crypto.PrimeOrderGroupFamily.linearHashSeedLen: seed lengthmsgLen n * (2 * bound d + 1)forlinearHashKDF.
Main results #
Cslib.Crypto.PrimeOrderGroupFamily.DDH.withSeed:DDHis preserved underseededSetupwhenseedLenis polynomial-time computable in unary.Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_linearHashKDF:linearHashKDFis computable in polynomial time whenkeyLenandboundare polynomial-time computable in unary.Cslib.Crypto.PrimeOrderGroupFamily.advantage_kdfGame_linearHashKDF_le: unconditional Leftover Hash Lemma bound onGame.advantagebetweenkdfRealGameandkdfIdealGame([BS23], Section 8.10.4, Theorem 8.11, p. 334, and Section 11.5.2, p. 449).Cslib.Crypto.PrimeOrderGroupFamily.secureKDF_linearHashKDF,Cslib.Crypto.PrimeOrderGroupFamily.secureKDF_linearHashKDF_const,Cslib.Crypto.PrimeOrderGroupFamily.exists_secureKDF_withSeed,Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_hashedElGamalCPAGame_linearHashKDF: non-degenerateSecureKDFand Hashed ElGamal IND-CPA instantiations vialinearHashKDF.
References #
- D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 8.10.4 (Theorem 8.11, p. 334) and Section 11.5.2 (Attack Game 11.3, Definition 11.5, and Theorem 11.5, pp. 448–451).
Prime-order group family with a public seed in the description #
Augment a PrimeOrderGroupFamily with a public bit-string seed in the group description
(Desc := F.Desc × List Bool), as in [BS23], Section 8.10.4 (p. 334), where the
universal-hash key is part of the public system parameter. All group operations act on the
underlying group description d.1 : F.Desc.
Instances For
Setup distribution for F.withSeed: draw d ← setup n, then sample a uniform seed
s ← Cslib.BitString.uniformList (seedLen n d) conditional on d, and return (d, s).
Instances For
Given a DDH distinguisher for F.withSeed, construct a DDH distinguisher for F by sampling
a fresh uniform seed s ← Cslib.BitString.sampleList (seedLen n d) and passing
((d, s), u, v, w) to distinguisher.
Instances For
In ddhRealGame, seededDDHDistinguisher simulates F.withSeed.ddhRealGame under
seededSetup.
In ddhIdealGame, seededDDHDistinguisher simulates F.withSeed.ddhIdealGame under
seededSetup.
seededDDHDistinguisher is uniform strict PPT whenever seedLen is polynomial-time computable
in unary and distinguisher is uniform strict PPT.
Preservation of DDH under public-seed augmentation: if F.DDH setup holds and
seedLen is polynomial-time computable in unary, then F.withSeed.DDH (F.seededSetup setup seedLen) holds.
Binary Linear-Hash Key Derivation and Leftover Hash Lemma #
Binary linear-hash key derivation function ([BS23], Section 8.10.4, Theorem 8.11,
p. 334, and Section 11.5.2, p. 449): given a seeded group description (d, s) : F.withSeed.Desc
and an encoded group element w : List Bool, pad w to the self-delimiting width
2 * bound d + 1 via Cslib.BitString.padWord (bound d) w and hash with the public seed s
via Cslib.BitString.LinearHash.wordHash (keyLen d) s.
Instances For
linearHashKDF always outputs a word of length keyLen input.1.1.
linearHashKDF is computable in polynomial time whenever keyLen and bound are computable
in polynomial time in unary from the group description d : F.Desc.
The matrix seed length required by linearHashKDF for output length msgLen n and encoding
length bound bound d: msgLen n * (2 * bound d + 1) bits.
Instances For
linearHashSeedLen is computable in polynomial time in unary whenever msgLen and bound
are computable in polynomial time in unary.
When every encoded group element in F.Carrier d has bit-length at most bound d,
List.ofFn (F.paddedGeneratorMultiple bound d γ) recovers the padded word
Cslib.BitString.padWord (bound d) (F.encode d (γ • F.generator d)).
When every encoded group element in F.Carrier d has bit-length at most bound d,
paddedGeneratorMultiple bound d is injective on ZMod (F.order d).
Unconditional Leftover Hash Lemma bound for linearHashKDF ([BS23],
Section 8.10.4, Theorem 8.11, p. 334, and Section 11.5.2, p. 449): for every (even computationally
unbounded) distinguisher, when every d ∈ (setup n).support satisfies keyLen d = msgLen n,
∀ x, (F.encode d x).length ≤ bound d, and qMin ≤ F.order d with 0 < qMin, the distinguishing
advantage between kdfRealGame and kdfIdealGame under F.seededSetup and F.linearHashKDF is at
most NNReal.sqrt ((2 : ℝ≥0) ^ (msgLen n) / (qMin : ℝ≥0)) / 2.
Unconditional SecureKDF instantiation via linearHashKDF ([BS23],
Section 8.10.4, Theorem 8.11, p. 334, and Section 11.5.2, Definition 11.5, p. 449): when keyLen
matches msgLen n on (setup n).support, bound bounds the encoded group element length, and
2 ^ (msgLen n) / qMin n is negligible, linearHashKDF keyLen bound satisfies SecureKDF over
F.withSeed and F.seededSetup setup (F.linearHashSeedLen msgLen bound).
Unconditional SecureKDF instantiation for any constant key length k : ℕ (including all
non-degenerate k > 0, e.g., k = 128 as in [BS23], Section 8.10.4, p. 334): when
1 / qMin n is negligible, linearHashKDF (fun _ => k) bound is a SecureKDF with output length
fun _ => k.
Existence of a polynomial-time non-degenerate SecureKDF for any PrimeOrderGroupFamily
with super-polynomial group order: using the canonical polynomial encoding-length bound from
F.exists_length_encode_le, for every key length k : ℕ (in particular any k > 0) there exist a
unary polynomial-time seed-length function seedLen and a polynomial-time hash function
H : F.withSeed.Desc × List Bool → List Bool such that F.withSeed.SecureKDF (F.seededSetup setup seedLen) H (fun _ => k) holds whenever 1 / qMin n is negligible.
Hashed ElGamal with linearHashKDF is IND-CPA secure under F.DDH setup alone
([BS23], 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, and
DDH.negligible_hashedElGamalCPAGame, no computational hypothesis on the key-derivation hash is
needed when 2 ^ (msgLen n) / qMin n is negligible.