Uniform PseudorandomFunction Instantiation of Naor–Reingold from DDH

This module connects the setup-parameterized universal-hash Naor–Reingold security theorems of Complexity.Crypto.Computational.NaorReingold.Security to the uniform bit-string primitives Cslib.Crypto.PseudorandomGenerator and Cslib.Crypto.PseudorandomFunction over any deterministic polynomial-time prime-order group family desc : ℕ → F.Desc:

1. Key-expanded Naor–Reingold bit-string PRF (naorReingoldSeededPRF, DDH.pseudorandomFunction_naorReingoldSeeded) (paraphrase of [NR04], Section 4.1, Construction 4.2 and Theorem 4.3, combined with PRG key expansion so a uniform n-bit secret key supplies both the n + 1 modular exponents and the two-universal hash seed required by Cslib.Crypto.PseudorandomFunction): given an expanding PRG expand : List Bool → List Bool producing at least (n + 1) * expWidth n + n * (2 * bound (desc n) + 1) bits from an n-bit key with expWidth n ≥ (F.order (desc n)).size + n, naorReingoldSeededPRF slices expand key into n + 1 binary exponents α₀, α₁, …, αₙ and a universal-hash seed and evaluates naorReingoldHashedWordEval. When F.DDH (fun n => PMF.pure (desc n)) holds and 2 ^ n / F.order (desc n) is negligible, naorReingoldSeededPRF satisfies Cslib.Crypto.PseudorandomFunction.
2. Direct algebraic PRG from DDH alone (DDH.exists_pseudorandomGenerator): evaluating 1-bit universal-hash Naor–Reingold (outLen = 1, whose Leftover Hash Lemma error decays via DDH.negligible_expected_inv_order without any external order-growth hypothesis) at seedLen n + 1 distinct binary inputs Cslib.BitString.lowBits (inBits n) i stretches a uniform seedLen n-bit seed by one bit, and Cslib.Crypto.GeneratorReindex.pseudorandomGenerator reindexes it to a Cslib.Crypto.PseudorandomGenerator at every seed length n.
3. End-to-end PseudorandomFunction from DDH (DDH.exists_naorReingoldPseudorandomFunction, DDH.exists_pseudorandomFunction): amplifying the DDH PRG via Cslib.Crypto.PseudorandomGenerator.amplify instantiates naorReingoldSeededPRF directly from F.DDH (fun n => PMF.pure (desc n)) and Negligible (fun n => 2 ^ n / F.order (desc n)); combining DDH.exists_pseudorandomGenerator with the Goldreich–Goldwasser–Micali construction PseudorandomGenerator.exists_pseudorandomFunction ([GGM86]) also yields ∃ family, PseudorandomFunction family from F.DDH (fun n => PMF.pure (desc n)) alone.

Main definitions

• Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldSeededPRF: keyed bit-string family evaluating naorReingoldHashedWordEval on exponents and hash seed expanded from an n-bit secret key.

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_naorReingoldSeededPRF: polynomial-time evaluation of naorReingoldSeededPRF.
• Cslib.Crypto.PrimeOrderGroupFamily.DDH.pseudorandomFunction_naorReingoldSeeded: PseudorandomFunction security of naorReingoldSeededPRF from DDH, a key-expanding PRG, and negligible 2 ^ n / F.order (desc n).
• Cslib.Crypto.PrimeOrderGroupFamily.DDH.exists_pseudorandomGenerator: existence of a uniform one-bit-stretch PseudorandomGenerator from F.DDH (fun n => PMF.pure (desc n)) alone.
• Cslib.Crypto.PrimeOrderGroupFamily.DDH.exists_naorReingoldPseudorandomFunction: existence of parameters instantiating naorReingoldSeededPRF as a PseudorandomFunction from DDH and negligible 2 ^ n / F.order (desc n).
• Cslib.Crypto.PrimeOrderGroupFamily.DDH.exists_pseudorandomFunction: existence of a uniform PseudorandomFunction from F.DDH (fun n => PMF.pure (desc n)) alone via DDH.exists_pseudorandomGenerator and the Goldreich–Goldwasser–Micali construction ([GGM86]).

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 4.11 (Exercise 4.18, p. 172) and Section 10.11 (Exercises 10.4, 10.8, and 10.11, pp. 424–426).
• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions.
• M. Naor, O. Reingold, Number-Theoretic Constructions of Efficient Pseudo-Random Functions, Section 4.1 (Construction 4.1, Theorem 4.1, Lemma 4.2, Construction 4.2, Theorem 4.3, and Remark 4.2).

Tape Parsing and Uniform-Tape Indistinguishability

Key-Expanded Naor–Reingold PseudorandomFunction

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldSeededPRF (F : PrimeOrderGroupFamily) (desc : ℕ → F.Desc) (bound : F.Desc → ℕ) (expWidth : ℕ → ℕ) (expand : List Bool → List Bool) (key query : List Bool) : List Bool

Keyed bit-string family evaluating the universal-hash Naor–Reingold construction naorReingoldHashedWordEval after expanding key via expand into key.length + 1 expWidth key.length-bit binary exponents and a key.length * (2 * bound (desc key.length) + 1)-bit two-universal hash seed (paraphrase of [NR04], Section 4.1, Construction 4.2, combined with PRG key expansion so a uniform n-bit secret key suffices for Cslib.Crypto.PseudorandomFunction).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.length_naorReingoldSeededPRF (F : PrimeOrderGroupFamily) (desc : ℕ → F.Desc) (bound : F.Desc → ℕ) (expWidth : ℕ → ℕ) (expand : List Bool → List Bool) (key query : List Bool) : (F.naorReingoldSeededPRF desc bound expWidth expand key query).length = key.length

naorReingoldSeededPRF always outputs a bit string of length key.length.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_naorReingoldSeededPRF (F : PrimeOrderGroupFamily) {desc : ℕ → F.Desc} {bound : F.Desc → ℕ} {expWidth : ℕ → ℕ} {expand : List Bool → List Bool} (hdesc : Turing.MultiTapeTM.ComputableInPolyTime desc Turing.MultiTapeTM.encUnary F.encDesc) (hbound : Turing.MultiTapeTM.ComputableInPolyTime bound F.encDesc Turing.MultiTapeTM.encUnary) (hexpWidth : Turing.MultiTapeTM.ComputableInPolyTime expWidth Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hexpand : Turing.MultiTapeTM.ComputableInPolyTime expand Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => F.naorReingoldSeededPRF desc bound expWidth expand p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

naorReingoldSeededPRF is computable in deterministic polynomial time when desc, bound, expWidth, and expand are polynomial-time computable.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.pseudorandomFunction_naorReingoldSeeded {F : PrimeOrderGroupFamily} {desc : ℕ → F.Desc} {bound : F.Desc → ℕ} {expWidth targetLen : ℕ → ℕ} {expand : List Bool → List Bool} (hDDH : F.DDH fun (n : ℕ) => PMF.pure (desc n)) (hdesc : Turing.MultiTapeTM.ComputableInPolyTime desc Turing.MultiTapeTM.encUnary F.encDesc) (hbound_poly : Turing.MultiTapeTM.ComputableInPolyTime bound F.encDesc Turing.MultiTapeTM.encUnary) (hbound : ∀ (n : ℕ) (x : F.Carrier (desc n)), (F.encode (desc n) x).length ≤ bound (desc n)) (hexpWidth_poly : Turing.MultiTapeTM.ComputableInPolyTime expWidth Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hexpWidth : ∀ (n : ℕ), (F.order (desc n)).size + n ≤ expWidth n) (hexpand : PseudorandomGenerator expand targetLen) (htarget : ∀ (n : ℕ), (n + 1) * expWidth n + n * (2 * bound (desc n) + 1) ≤ targetLen n) (hneg : Negligible fun (n : ℕ) => 2 ^ n / ↑(F.order (desc n))) : PseudorandomFunction (F.naorReingoldSeededPRF desc bound expWidth expand)

Uniform PseudorandomFunction security of naorReingoldSeededPRF (paraphrase of [NR04], Section 4.1, Construction 4.2 and Theorem 4.3, combined with PRG key expansion): if desc : ℕ → F.Desc is a deterministic polynomial-time group family satisfying F.DDH (fun n => PMF.pure (desc n)) with 2 ^ n / F.order (desc n) negligible, expWidth n ≥ (F.order (desc n)).size + n, and expand is a PseudorandomGenerator stretching n-bit keys to at least (n + 1) * expWidth n + n * (2 * bound (desc n) + 1) bits, then naorReingoldSeededPRF is a uniform PseudorandomFunction.

Direct Algebraic PseudorandomGenerator from DDH Alone

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.exists_pseudorandomGenerator {F : PrimeOrderGroupFamily} {desc : ℕ → F.Desc} (hDDH : F.DDH fun (n : ℕ) => PMF.pure (desc n)) (hdesc : Turing.MultiTapeTM.ComputableInPolyTime desc Turing.MultiTapeTM.encUnary F.encDesc) : ∃ (generator : List Bool → List Bool), PseudorandomGenerator generator fun (n : ℕ) => n + 1

Existence of a uniform PseudorandomGenerator from DDH alone: for any deterministic polynomial-time prime-order group family desc : ℕ → F.Desc satisfying F.DDH (fun n => PMF.pure (desc n)), evaluating 1-bit universal-hash Naor–Reingold at distinct binary inputs and reindexing via GeneratorReindex.pseudorandomGenerator yields a uniform PseudorandomGenerator with one-bit stretch at every seed length.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.exists_naorReingoldPseudorandomFunction {F : PrimeOrderGroupFamily} {desc : ℕ → F.Desc} (hDDH : F.DDH fun (n : ℕ) => PMF.pure (desc n)) (hdesc : Turing.MultiTapeTM.ComputableInPolyTime desc Turing.MultiTapeTM.encUnary F.encDesc) (hneg : Negligible fun (n : ℕ) => 2 ^ n / ↑(F.order (desc n))) : ∃ (bound : F.Desc → ℕ) (expWidth : ℕ → ℕ) (expand : List Bool → List Bool), PseudorandomFunction (F.naorReingoldSeededPRF desc bound expWidth expand)

Existence of an explicit Naor–Reingold PseudorandomFunction from DDH: for any deterministic polynomial-time prime-order group family desc : ℕ → F.Desc satisfying F.DDH (fun n => PMF.pure (desc n)) with 2 ^ n / F.order (desc n) negligible, there exist polynomial-time parameters bound, expWidth, and expand such that F.naorReingoldSeededPRF desc bound expWidth expand is a uniform PseudorandomFunction.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.exists_pseudorandomFunction {F : PrimeOrderGroupFamily} {desc : ℕ → F.Desc} (hDDH : F.DDH fun (n : ℕ) => PMF.pure (desc n)) (hdesc : Turing.MultiTapeTM.ComputableInPolyTime desc Turing.MultiTapeTM.encUnary F.encDesc) : ∃ (family : List Bool → List Bool → List Bool), PseudorandomFunction family

Existence of a uniform PseudorandomFunction from DDH alone: any deterministic polynomial-time prime-order group family desc : ℕ → F.Desc satisfying F.DDH (fun n => PMF.pure (desc n)) yields a uniform PseudorandomFunction by combining the 1-bit-stretch Naor–Reingold generator DDH.exists_pseudorandomGenerator with the Goldreich–Goldwasser–Micali tree construction PseudorandomGenerator.exists_pseudorandomFunction ([GGM86]). For the direct Naor–Reingold PRF family under Negligible (2 ^ n / F.order (desc n)), see DDH.exists_naorReingoldPseudorandomFunction.