Computational security of the Naor–Reingold PRF from DDH

This module completes the efficient lazy-sampling Decisional Diffie–Hellman (DDH) reduction and the universal-hash bit-string pseudorandom-function bridge for the Naor–Reingold PRF over a PrimeOrderGroupFamily ([BS23], Section 10.11, Exercises 10.4, 10.8, 10.11, pp. 424–426, and Section 4.11, Exercise 4.18, p. 172; [NR04], Section 4.1, Construction 4.1, Theorem 4.1, Lemma 4.2, Construction 4.2, Theorem 4.3, and Remark 4.2):

1. Inverse-order bound from DDH: DDH.negligible_expected_inv_order, imported from Complexity.Crypto.Computational.DiffieHellman.Order, makes the setup-averaged inverse group order negligible; it bounds the hashed-PRF error terms below.
2. Word-level adaptive group-PRF games and lazy-sampling IsOraclePPT DDH reduction: naorReingoldFrontierOracle memoizes ddhFixedUWordRerandomize only on the k-bit prefixes queried by an OracleDistinguisher and evaluates the remaining suffix via naorReingoldWordSuffix. Choosing k ← sampleDyadicIndex (inLen n) yields the uniform strict PPT DDH distinguisher naorReingoldToDDHDistinguisher, proving both quantitative single- distinguisher bounds and asymptotic security (DDH.negligible_naorReingoldWordGame, DDH.negligible_naorReingoldProbGame) under F.DDH setup alone.
3. Universal-hash bit-string Naor–Reingold PRF (paraphrase of [NR04], Section 4.1, Construction 4.2, Theorem 4.3, and Remark 4.2, using Lemma 4.2): composing naorReingoldWordEval with linearHashKDF under a public universal-hash seed (F.withSeed and F.seededSetup) maps group outputs into uniform outLen n-bit strings; a multi-query Leftover Hash Lemma bound via PMF.dist_bind_pair_pi_le_sum yields adaptive bit-string PRF security (DDH.negligible_naorReingoldHashedGame, DDH.negligible_naorReingoldHashedProbGame, and DDH.negligible_naorReingoldHashedGame_const).

Main definitions

• Cslib.Crypto.PrimeOrderGroupFamily.sampleNaorReingoldExp: executable modular exponent sampler with statistical slack n + (F.encDesc d).length.
• Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldWordRealGame, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldProbRealGame, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldWordIdealGame: setup-parameterized word-level adaptive Naor–Reingold group-PRF experiments.
• Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldFrontierOracle: memoized prefix DDH rerandomization followed by naorReingoldWordSuffix.
• Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldToDDHDistinguisher: single-challenge uniform strict PPT DDH distinguisher constructed from an adaptive PRF distinguisher.
• Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHashedWordEval, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHashedRealGame, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHashedProbRealGame, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHashedGroupIdealGame, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHashedIdealGame: universal-hash bit-string Naor–Reingold evaluation and setup-parameterized PRF experiments.

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_naorReingoldToDDHDistinguisher: uniform strict PPT certificate for naorReingoldToDDHDistinguisher from any IsOraclePPT distinguisher.
• Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingoldWordGame_le, Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingoldProbRealGame_wordRealGame_le: quantitative single-distinguisher DDH reduction and modular-sampling bounds for the group-PRF.
• Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_naorReingoldWordGame, Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_naorReingoldProbGame: asymptotic adaptive security of the Naor–Reingold group-PRF under F.DDH setup.
• Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_naorReingoldHashedWordEval, Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingoldHashedIdeal_le, Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_naorReingoldHashedGame, Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_naorReingoldHashedProbGame, Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_naorReingoldHashedGame_const: polynomial-time evaluation, multi-query Leftover Hash Lemma bound, and asymptotic bit-string PRF security.

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).
• 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).

Word-level Naor–Reingold group-PRF games and prefix hybrids

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.sampleNaorReingoldExp (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) : ProbComp ℕ

Sample a nearly-uniform modular exponent modulo F.order d via F.sampleExp with n + (F.encDesc d).length statistical slack bits so that the statistical error 1 / 2 ^ (n + |encDesc d|) offsets polynomial query counts depending on |encDesc d| (original).

theorem Cslib.Crypto.PrimeOrderGroupFamily.lt_order_of_mem_support_sampleNaorReingoldExp (F : PrimeOrderGroupFamily) {n : ℕ} {d : F.Desc} {v : ℕ} (hv : v ∈ (F.sampleNaorReingoldExp n d).eval.support) : v < F.order d

Every value supported by sampleNaorReingoldExp is strictly less than F.order d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.map_natCast_eval_sampleNaorReingoldExp (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) : PMF.map Nat.cast (F.sampleNaorReingoldExp n d).eval = F.sampleModZModLaw (n + (F.encDesc d).length) d

Projected to ZMod (F.order d), sampleNaorReingoldExp n d has law F.sampleModZModLaw (n + (F.encDesc d).length) d.

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_sampleNaorReingoldExp (F : PrimeOrderGroupFamily) {α : Type} {input : α ↪ List Bool} {param : α → ℕ} {desc : α → F.Desc} (hparam : Turing.MultiTapeTM.ComputableInPolyTime param input Turing.MultiTapeTM.encUnary) (hdesc : Turing.MultiTapeTM.ComputableInPolyTime desc input F.encDesc) : Probability.IsPPTOn input Turing.MultiTapeTM.encNat fun (a : α) => F.sampleNaorReingoldExp (param a) (desc a)

sampleNaorReingoldExp is uniform strict PPT in (n, d).

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldWordOracle (F : PrimeOrderGroupFamily) (d : F.Desc) {m : ℕ} (fn : BitString m → F.Carrier d) (query : List Bool) : List Bool

Deterministic word-level oracle wrapper encoding fn : BitString m → F.Carrier d on valid m-bit queries and returning [] on malformed queries.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldWordRealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (inLen : ℕ → ℕ) (adversary : OracleDistinguisher) (n : ℕ) : Game

Setup-parameterized real Naor–Reingold group-PRF game with exact uniform ZMod (F.order d) exponents ([BS23], Exercise 10.4, p. 424; [NR04], Construction 4.1 & Theorem 4.1).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldProbRealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (inLen : ℕ → ℕ) (adversary : OracleDistinguisher) (n : ℕ) : Game

Setup-parameterized executable Naor–Reingold group-PRF real game sampling modular exponents via sampleNaorReingoldExp (original).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldWordIdealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (inLen : ℕ → ℕ) (adversary : OracleDistinguisher) (n : ℕ) : Game

Setup-parameterized ideal random group-function game against OracleDistinguisher ([BS23], Exercise 10.4, p. 424; [NR04], Theorem 4.1).

Lazy-sampling frontier oracle and IsOraclePPT DDH distinguisher

@[reducible, inline]

abbrev Cslib.Crypto.PrimeOrderGroupFamily.NaorReingoldCache : Type

Association-list cache mapping queried k-bit prefixes to encoded group-element pairs.

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldCacheEncoding : NaorReingoldCache ↪ List Bool

Encoding of NaorReingoldCache.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.sampleNaorReingoldPair (F : PrimeOrderGroupFamily) (n : ℕ) (d : F.Desc) (u v w : List Bool) : ProbComp (List Bool × List Bool)

Executable rerandomized pair sampler for naorReingoldFrontierOracle: draw two exponents via sampleNaorReingoldExp and apply ddhFixedUWordRerandomize.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldFrontierOracle (F : PrimeOrderGroupFamily) (n m k : ℕ) (d : F.Desc) (u v w : List Bool) (αs : List ℕ) (query : List Bool) : StateT NaorReingoldCache ProbComp (List Bool)

Stateful level-k frontier oracle for Naor–Reingold ([BS23], Exercises 10.4(b) & 4.18(b); [NR04], Theorem 4.1): on a valid m-bit query, memoize a freshly rerandomized DDH pair on query.take k, select the query[k] child, and evaluate the remaining suffix with naorReingoldWordSuffix. Malformed queries return [] without modifying the cache.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldToDDHDistinguisher (F : PrimeOrderGroupFamily) (inLen : ℕ → ℕ) (adversary : OracleDistinguisher) (n : ℕ) (input : F.Desc × List Bool × List Bool × List Bool) : ProbComp Bool

Single-challenge uniform strict PPT DDH distinguisher constructed from an adaptive PRF distinguisher adversary: sample a hybrid level k ← sampleDyadicIndex (inLen n), draw suffix exponents αs, and run adversary against naorReingoldFrontierOracle from an empty cache ([BS23], Exercises 10.4(b) & 10.11; [NR04], Theorem 4.1).

theorem Cslib.Crypto.PrimeOrderGroupFamily.isPPTOn_naorReingoldToDDHDistinguisher (F : PrimeOrderGroupFamily) {inLen : ℕ → ℕ} (hinLen : Turing.MultiTapeTM.ComputableInPolyTime inLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)))) Turing.MultiTapeTM.encBool fun (input : ℕ × F.Desc × List Bool × List Bool × List Bool) => F.naorReingoldToDDHDistinguisher inLen adversary input.1 input.2

naorReingoldToDDHDistinguisher is uniform strict PPT whenever inLen is computable in polynomial time in unary and adversary satisfies IsOraclePPT encBool ([BS23], Exercise 10.4(b); [NR04], Theorem 4.1).

Quantitative and asymptotic DDH security of the Naor–Reingold group-PRF

theorem Cslib.Crypto.PrimeOrderGroupFamily.iid_uniformOfFintype {α : Type u_1} [Fintype α] [Nonempty α] (k : ℕ) : Probability.PMF.iid (Probability.PMF.uniformOfFintype α) k = Probability.PMF.uniformOfFintype (Fin k → α)

The k-fold independent product of PMF.uniformOfFintype α is PMF.uniformOfFintype (Fin k → α).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingoldWordGame_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (inLen : ℕ → ℕ) (adversary : OracleDistinguisher) (n : ℕ) (Q : F.Desc → ℕ) {ε : NNReal} (hQ : ∀ d ∈ (setup n).support, ProbOracleComp.IsQueryBounded (adversary n (F.encDesc d)) (Q d)) (hε : ∀ d ∈ (setup n).support, ↑(inLen n + 2 * Q d) / 2 ^ (n + (F.encDesc d).length) ≤ ε) : (F.naorReingoldWordRealGame setup inLen adversary n).advantage (F.naorReingoldWordIdealGame setup inLen adversary n) ≤ ↑(Probability.dyadicSize (inLen n)) * ((F.ddhRealGame setup (F.naorReingoldToDDHDistinguisher inLen adversary) n).advantage (F.ddhIdealGame setup (F.naorReingoldToDDHDistinguisher inLen adversary) n) + 2 * ε + (∑' (d : F.Desc), (setup n) d * (↑(F.order d))⁻¹).toNNReal)

Quantitative single-distinguisher DDH security bound for the Naor–Reingold group-PRF ([BS23], Exercises 10.4 & 10.11; [NR04], Theorem 4.1): if adversary makes at most Q d queries on d ∈ (setup n).support with modular-sampling slack bounded by ε, then its PRF distinguishing advantage is at most dyadicSize (inLen n) times the single-challenge DDH advantage of naorReingoldToDDHDistinguisher plus 2 * ε plus the setup-averaged inverse group order.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingoldProbRealGame_wordRealGame_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (inLen : ℕ → ℕ) (adversary : OracleDistinguisher) (n : ℕ) : (F.naorReingoldProbRealGame setup inLen adversary n).advantage (F.naorReingoldWordRealGame setup inLen adversary n) ≤ ↑(inLen n + 1) / 2 ^ n

Modular-sampling distance between naorReingoldProbRealGame and naorReingoldWordRealGame: replacing (inLen n + 1) calls to sampleNaorReingoldExp by exact uniform ZMod (F.order d) exponents changes the output distribution by at most (inLen n + 1) / 2 ^ n.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_naorReingoldWordGame {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} {inLen : ℕ → ℕ} (hDDH : F.DDH setup) (hinLen : Turing.MultiTapeTM.ComputableInPolyTime inLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Negligible fun (n : ℕ) => (F.naorReingoldWordRealGame setup inLen adversary n).advantage (F.naorReingoldWordIdealGame setup inLen adversary n)

Asymptotic DDH security of the Naor–Reingold group-PRF (naorReingoldWordRealGame) ([BS23], Exercise 10.4; [NR04], Theorem 4.1): if F.DDH setup holds and inLen is computable in polynomial time in unary, no IsOraclePPT adversary can distinguish naorReingoldWordRealGame from naorReingoldWordIdealGame with non-negligible advantage.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_naorReingoldProbGame {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} {inLen : ℕ → ℕ} (hDDH : F.DDH setup) (hinLen : Turing.MultiTapeTM.ComputableInPolyTime inLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Negligible fun (n : ℕ) => (F.naorReingoldProbRealGame setup inLen adversary n).advantage (F.naorReingoldWordIdealGame setup inLen adversary n)

Asymptotic DDH security of the executable Naor–Reingold group-PRF (naorReingoldProbRealGame) ([BS23], Exercise 10.4; [NR04], Theorem 4.1): if F.DDH setup holds and inLen is computable in polynomial time in unary, no IsOraclePPT adversary can distinguish naorReingoldProbRealGame from naorReingoldWordIdealGame with non-negligible advantage.

Universal-hash bit-string Naor–Reingold PRF

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHashedWordEval (F : PrimeOrderGroupFamily) (outLen : ℕ) (bound : F.Desc → ℕ) (d : F.Desc) (seed : List Bool) (α₀ : ℕ) (αs : List ℕ) (xs : List Bool) : List Bool

Word-level universal-hash Naor–Reingold evaluation (paraphrase of [NR04], Section 4.1, Construction 4.2): evaluate naorReingoldWordEval and hash the resulting encoded group element into {0, 1}^{outLen} with linearHashKDF.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.length_naorReingoldHashedWordEval (F : PrimeOrderGroupFamily) (outLen : ℕ) (bound : F.Desc → ℕ) (d : F.Desc) (seed : List Bool) (α₀ : ℕ) (αs : List ℕ) (xs : List Bool) : (F.naorReingoldHashedWordEval outLen bound d seed α₀ αs xs).length = outLen

naorReingoldHashedWordEval always outputs outLen bits.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_naorReingoldHashedWordEval (F : PrimeOrderGroupFamily) {bound : F.Desc → ℕ} (hbound : Turing.MultiTapeTM.ComputableInPolyTime bound F.encDesc Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (input : ℕ × F.Desc × List Bool × ℕ × List ℕ × List Bool) => F.naorReingoldHashedWordEval input.1 bound input.2.1 input.2.2.1 input.2.2.2.1 input.2.2.2.2.1 input.2.2.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits))))) Turing.MultiTapeTM.encBits

naorReingoldHashedWordEval is computable in polynomial time when outLen is given in unary and bound is computable in polynomial time in unary from d.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHashedRealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (inLen outLen : ℕ → ℕ) (bound : F.Desc → ℕ) (adversary : OracleDistinguisher) (n : ℕ) : Game

Setup-parameterized real universal-hash Naor–Reingold bit-string PRF game with exact uniform ZMod (F.order d) exponents and public hash seed (d, seed) encoded via F.withSeed.encDesc (paraphrase of [NR04], Section 4.1, Construction 4.2, Theorem 4.3, and Remark 4.2).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHashedProbRealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (inLen outLen : ℕ → ℕ) (bound : F.Desc → ℕ) (adversary : OracleDistinguisher) (n : ℕ) : Game

Setup-parameterized executable real universal-hash Naor–Reingold bit-string PRF game sampling exponents via sampleNaorReingoldExp (original).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHashedIdealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (inLen outLen : ℕ → ℕ) (bound : F.Desc → ℕ) (adversary : OracleDistinguisher) (n : ℕ) : Game

Setup-parameterized ideal bit-string random-function game for universal-hash Naor–Reingold: sample (d, seed) ← F.seededSetup setup (F.linearHashSeedLen outLen bound) n, draw an independent uniform random function f : BitString (inLen n) → BitString (outLen n), and pass F.withSeed.encDesc (d, seed) to adversary (paraphrase of [NR04], Section 4.1, Theorem 4.3 and Remark 4.2).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHashedGroupIdealGame (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (inLen outLen : ℕ → ℕ) (bound : F.Desc → ℕ) (adversary : OracleDistinguisher) (n : ℕ) : Game

Intermediate hybrid game for universal-hash Naor–Reingold: sample (d, seed) via seededSetup, draw an independent uniform random group-valued table B : BitString (inLen n) → ZMod (F.order d), and hash each queried group element B x • g with linearHashKDF (paraphrase of [NR04], Section 4.1, Theorem 4.3 and Remark 4.2, using Lemma 4.2).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingoldHashedIdeal_le (F : PrimeOrderGroupFamily) (setup : ℕ → PMF F.Desc) (inLen outLen : ℕ → ℕ) (bound : F.Desc → ℕ) (adversary : OracleDistinguisher) (n Q qMin : ℕ) (hq0 : 0 < qMin) (hbound : ∀ d ∈ (setup n).support, ∀ (x : F.Carrier d), (F.encode d x).length ≤ bound d) (hq : ∀ d ∈ (setup n).support, qMin ≤ F.order d) (hQ : ∀ d ∈ (setup n).support, ∀ (seed : BitString (outLen n * (2 * bound d + 1))), ProbOracleComp.IsQueryBounded (adversary n (F.withSeed.encDesc (d, List.ofFn seed))) Q) : (F.naorReingoldHashedGroupIdealGame setup inLen outLen bound adversary n).advantage (F.naorReingoldHashedIdealGame setup inLen outLen bound adversary n) ≤ ↑Q * (NNReal.sqrt (2 ^ outLen n / ↑qMin) / 2)

Multi-query Leftover Hash Lemma bound for hashed Naor–Reingold (paraphrase of [NR04], Section 4.1, Lemma 4.2; [BS23], Section 8.10.4, Theorem 8.11, p. 334): if adversary makes at most Q queries on (setup n).support and qMin ≤ F.order d, then replacing hashed random group elements by a uniform random function BitString (inLen n) → BitString (outLen n) changes the output distribution by at most Q * (√(2 ^ (outLen n) / qMin) / 2).

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_naorReingoldHashedGame {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} {inLen outLen : ℕ → ℕ} {bound : F.Desc → ℕ} {descBound qMin : ℕ → ℕ} (hDDH : F.DDH setup) (hinLen : Turing.MultiTapeTM.ComputableInPolyTime inLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (houtLen : Turing.MultiTapeTM.ComputableInPolyTime outLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hbound_poly : Turing.MultiTapeTM.ComputableInPolyTime bound F.encDesc Turing.MultiTapeTM.encUnary) (hdesc_poly : PolynomiallyBounded descBound) (hdesc : ∀ (n : ℕ), ∀ d ∈ (setup n).support, (F.encDesc d).length ≤ descBound n) (hbound : ∀ (n : ℕ), ∀ d ∈ (setup n).support, ∀ (x : F.Carrier d), (F.encode d x).length ≤ bound d) (hq0 : ∀ (n : ℕ), 0 < qMin n) (hq : ∀ (n : ℕ), ∀ d ∈ (setup n).support, qMin n ≤ F.order d) (hneg : Negligible fun (n : ℕ) => 2 ^ outLen n / ↑(qMin n)) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Negligible fun (n : ℕ) => (F.naorReingoldHashedRealGame setup inLen outLen bound adversary n).advantage (F.naorReingoldHashedIdealGame setup inLen outLen bound adversary n)

Asymptotic DDH security of the universal-hash Naor–Reingold bit-string PRF (paraphrase of [NR04], Section 4.1, Construction 4.2, Theorem 4.3, and Remark 4.2): under F.DDH setup, when group descriptions on (setup n).support have polynomially bounded bit-length, bound bounds encoded group elements, and 2 ^ (outLen n) / qMin n is negligible, no IsOraclePPT adversary can distinguish naorReingoldHashedRealGame from naorReingoldHashedIdealGame.

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_naorReingoldHashedProbGame {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} {inLen outLen : ℕ → ℕ} {bound : F.Desc → ℕ} {descBound qMin : ℕ → ℕ} (hDDH : F.DDH setup) (hinLen : Turing.MultiTapeTM.ComputableInPolyTime inLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (houtLen : Turing.MultiTapeTM.ComputableInPolyTime outLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hbound_poly : Turing.MultiTapeTM.ComputableInPolyTime bound F.encDesc Turing.MultiTapeTM.encUnary) (hdesc_poly : PolynomiallyBounded descBound) (hdesc : ∀ (n : ℕ), ∀ d ∈ (setup n).support, (F.encDesc d).length ≤ descBound n) (hbound : ∀ (n : ℕ), ∀ d ∈ (setup n).support, ∀ (x : F.Carrier d), (F.encode d x).length ≤ bound d) (hq0 : ∀ (n : ℕ), 0 < qMin n) (hq : ∀ (n : ℕ), ∀ d ∈ (setup n).support, qMin n ≤ F.order d) (hneg : Negligible fun (n : ℕ) => 2 ^ outLen n / ↑(qMin n)) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Negligible fun (n : ℕ) => (F.naorReingoldHashedProbRealGame setup inLen outLen bound adversary n).advantage (F.naorReingoldHashedIdealGame setup inLen outLen bound adversary n)

Asymptotic DDH security of the executable universal-hash Naor–Reingold bit-string PRF (naorReingoldHashedProbRealGame) (paraphrase of [NR04], Section 4.1, Construction 4.2, Theorem 4.3, and Remark 4.2).

theorem Cslib.Crypto.PrimeOrderGroupFamily.DDH.negligible_naorReingoldHashedGame_const {F : PrimeOrderGroupFamily} {setup : ℕ → PMF F.Desc} {inLen : ℕ → ℕ} {bound : F.Desc → ℕ} {descBound : ℕ → ℕ} (c : ℕ) (hDDH : F.DDH setup) (hinLen : Turing.MultiTapeTM.ComputableInPolyTime inLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hbound_poly : Turing.MultiTapeTM.ComputableInPolyTime bound F.encDesc Turing.MultiTapeTM.encUnary) (hdesc_poly : PolynomiallyBounded descBound) (hdesc : ∀ (n : ℕ), ∀ d ∈ (setup n).support, (F.encDesc d).length ≤ descBound n) (hbound : ∀ (n : ℕ), ∀ d ∈ (setup n).support, ∀ (x : F.Carrier d), (F.encode d x).length ≤ bound d) {adversary : OracleDistinguisher} (hadversary : Probability.IsOraclePPT Turing.MultiTapeTM.encBool adversary) : Negligible fun (n : ℕ) => (F.naorReingoldHashedRealGame setup inLen (fun (x : ℕ) => c) bound adversary n).advantage (F.naorReingoldHashedIdealGame setup inLen (fun (x : ℕ) => c) bound adversary n)

Constant-output-length hashed Naor–Reingold security under F.DDH setup alone (original, combining DDH.negligible_expected_inv_order with Theorem 4.3, Remark 4.2, and Lemma 4.2 of [NR04]): for any constant output length c : ℕ (including c = 1), F.DDH setup automatically supplies the inverse-order decay needed by the Leftover Hash Lemma, requiring no external qMin hypothesis.