The Naor–Reingold pseudorandom function from Decisional Diffie–Hellman

Over a PrimeOrderGroupFamily F, the Naor–Reingold pseudorandom function ([BS23], Section 10.11, Exercise 10.4, p. 424; [NR04], Section 4.1, Construction 4.1 & Theorem 4.1) with key (α₀, α₁, …, αₙ) ∈ (ZMod q)ⁿ⁺¹ maps an n-bit input x ∈ {0, 1}ⁿ to the group element $$F_{\mathrm{NR}}((\alpha_0, \alpha_1, \dots, \alpha_n), (x_1, \dots, x_n)) := \left(\alpha_0 \cdot \prod_{i=1}^n \alpha_i^{x_i}\right) \bullet g.$$

Following Boneh–Shoup Exercises 10.4, 10.8, 10.11, and 4.18, we formalize:

1. Algebraic and augmented-tree characterization (naorReingoldEval, naorReingoldTreeEval):
   • The closed-form exponent product naorReingoldExp and group evaluation naorReingoldEval.
   • The single-step generator naorReingoldPRG ($G_{\mathrm{NR}}(\alpha, u) = (u, \alpha \bullet u)$) and augmented-tree fold naorReingoldTreeEval, together with naorReingoldTreeEval_eq_naorReingoldEval ([BS23], Exercise 10.4(a), p. 424, and Exercise 4.18, p. 172).
   • The word-level evaluator naorReingoldWordEval, its correctness theorem naorReingoldWordEval_eq_encode, and its plain polynomial-time certificate computableInPolyTime_naorReingoldWordEval.
2. Fixed-$u$ DDH random self-reduction and Multi-DDH (I) (ddhFixedURerandomize, multiDDHRerandomizeLaw):
   • Fixed-$u$ rerandomization $(u, v, w) \mapsto (u, \sigma \bullet g + \tau \bullet v, \sigma \bullet u + \tau \bullet w)$ ([BS23], Exercise 10.8, p. 425), its word-level counterpart ddhFixedUWordRerandomize, and the exact distributional laws ddhFixedURerandomizeLaw_real (Exercise 10.8(a)) and ddhFixedURerandomizeLaw_ideal (Exercise 10.8(b)).
   • The $n = 1$ (single shared secret $\alpha$, $|\iota|$ pairs) Multi-DDH (I) reduction multiDDHRerandomizeLaw ([BS23], Exercise 10.11, p. 426), whose wrapper samples $|\iota|$ rerandomized pairs, proving multiDDHRerandomizeLaw_real, multiDDHRerandomizeLaw_ideal, and the quantitative bound advantage_multiDDH_le ($\le \mathrm{DDHadv}[B] + 1 / q$).
3. Naor–Reingold PRF prefix hybrids and distributional security bound (naorReingoldRealGame, naorReingoldIdealGame, naorReingoldHybridGame):
   • The adaptive oracle experiments naorReingoldRealGame, naorReingoldIdealGame, and the depth-$k$ prefix hybrids naorReingoldHybridGame ($0 \le k \le n$), with exact endpoint identities naorReingoldHybridGame_zero and naorReingoldHybridGame_self.
   • The distributional single-level DDH distinguisher naorReingoldLevelDDHDistinguisher (which samples the $2^k$-entry prefix table BitString k) and adjacent-hop bound advantage_naorReingoldHybridGame_succ_le, the $n$-hybrid sum bound advantage_naorReingold_le_sum, and the common-bound corollary advantage_naorReingold_le_mul ($\le n \cdot (\varepsilon + 1 / q)$). The efficient lazy-sampling IsOraclePPT reduction and PseudorandomFunction bridge are proved in NaorReingold.Security and NaorReingold.PRF.

Main definitions

• Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldExp, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldEval: the Naor–Reingold exponent product and PRF evaluation.
• Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldPRG, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldStep, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldTreeEval: the single-step generator $G_{\mathrm{NR}}$ and augmented-tree evaluation.
• Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldWordEval: polynomial-time evaluation on encoded group elements.
• Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedURerandomize, Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedURerandomizeLaw: fixed-$u$ DDH rerandomization (Boneh–Shoup Exercise 10.8).
• Cslib.Crypto.PrimeOrderGroupFamily.multiDDHRealTupleLaw, Cslib.Crypto.PrimeOrderGroupFamily.multiDDHIdealTupleLaw, Cslib.Crypto.PrimeOrderGroupFamily.multiDDHRerandomizeLaw: $n = 1$ Multi-DDH (I) distributions and rerandomization (Boneh–Shoup Exercise 10.11).
• Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldRealGame, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldIdealGame, Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHybridGame: real, ideal, and prefix-hybrid adaptive PRF experiments.

Main results

• Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldTreeEval_eq_naorReingoldEval: augmented-tree characterization of the Naor–Reingold PRF (Boneh–Shoup Exercise 10.4(a)).
• Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_naorReingoldWordEval: plain polynomial-time certificate for word-level Naor–Reingold evaluation.
• Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedURerandomizeLaw_real, Cslib.Crypto.PrimeOrderGroupFamily.ddhFixedURerandomizeLaw_ideal: fixed-$u$ DDH random self-reduction (Boneh–Shoup Exercise 10.8).
• Cslib.Crypto.PrimeOrderGroupFamily.advantage_multiDDH_le: $n = 1$ Multi-DDH (I) reduction to DDH, sampling $|\iota|$ rerandomized pairs (Boneh–Shoup Exercise 10.11).
• Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingoldHybridGame_succ_le, Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingold_le_sum, Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingold_le_mul: distributional prefix-hybrid security bounds for the Naor–Reingold PRF against the explicit $2^k$-pair PMF distinguisher naorReingoldLevelDDHDistinguisher (Boneh–Shoup Exercise 10.4(b); Naor–Reingold Theorem 4.1); see NaorReingold.Security and NaorReingold.PRF for the lazy-sampling IsOraclePPT reduction and PseudorandomFunction bridge.

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

Naor–Reingold PRF and augmented-tree characterization (Exercise 10.4(a) & Exercise 4.18)

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldExp (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α₀ : ZMod (F.order d)) (α : Fin n → ZMod (F.order d)) (x : BitString n) : ZMod (F.order d)

The Naor–Reingold exponent product α₀ * ∏ i : Fin n, if x i then α i else 1 in ZMod (F.order d) ([BS23], Section 10.11, Exercise 10.4, p. 424; [NR04], Section 4.1, Construction 4.1).

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldEval (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α₀ : ZMod (F.order d)) (α : Fin n → ZMod (F.order d)) (x : BitString n) : F.Carrier d

The Naor–Reingold pseudorandom function F_NR((α₀, α₁, …, αₙ), (x₁, …, xₙ)) = (α₀ * ∏ i, αᵢ^{xᵢ}) • g ([BS23], Section 10.11, Exercise 10.4, p. 424; [NR04], Section 4.1, Construction 4.1).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldExp_zero (F : PrimeOrderGroupFamily) (d : F.Desc) (α₀ : ZMod (F.order d)) (α : Fin 0 → ZMod (F.order d)) (x : BitString 0) : F.naorReingoldExp d α₀ α x = α₀

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldEval_zero (F : PrimeOrderGroupFamily) (d : F.Desc) (α₀ : ZMod (F.order d)) (α : Fin 0 → ZMod (F.order d)) (x : BitString 0) : F.naorReingoldEval d α₀ α x = α₀ • F.generator d

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldExp_false (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α₀ : ZMod (F.order d)) (α : Fin n → ZMod (F.order d)) : (F.naorReingoldExp d α₀ α fun (x : Fin n) => false) = α₀

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldEval_false (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α₀ : ZMod (F.order d)) (α : Fin n → ZMod (F.order d)) : (F.naorReingoldEval d α₀ α fun (x : Fin n) => false) = α₀ • F.generator d

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldExp_true (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α₀ : ZMod (F.order d)) (α : Fin n → ZMod (F.order d)) : (F.naorReingoldExp d α₀ α fun (x : Fin n) => true) = α₀ * ∏ i : Fin n, α i

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldEval_true (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α₀ : ZMod (F.order d)) (α : Fin n → ZMod (F.order d)) : (F.naorReingoldEval d α₀ α fun (x : Fin n) => true) = (α₀ * ∏ i : Fin n, α i) • F.generator d

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldPRG (F : PrimeOrderGroupFamily) (d : F.Desc) (α : ZMod (F.order d)) (u : F.Carrier d) : F.Carrier d × F.Carrier d

The Naor–Reingold single-step generator G_NR(α, u) := (u, α • u) ([BS23], Section 10.11, Exercise 10.4(a), p. 424).

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldStep (F : PrimeOrderGroupFamily) (d : F.Desc) (u : F.Carrier d) (p : ZMod (F.order d) × Bool) : F.Carrier d

One step of the augmented tree construction ([BS23], Section 4.11, Exercise 4.18, p. 172, and Section 10.11, Exercise 10.4(a), p. 424): select the false (u) or true (α • u) child of naorReingoldPRG d α u.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldStep_eq_prg (F : PrimeOrderGroupFamily) (d : F.Desc) (u : F.Carrier d) (α : ZMod (F.order d)) (b : Bool) : F.naorReingoldStep d u (α, b) = if b = true then (F.naorReingoldPRG d α u).2 else (F.naorReingoldPRG d α u).1

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldTreeFold (F : PrimeOrderGroupFamily) (d : F.Desc) (u : F.Carrier d) (steps : List (ZMod (F.order d) × Bool)) : F.Carrier d

Augmented-tree evaluation of naorReingoldStep along a list of (key, bit) pairs starting from an initial group element u.

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldTreeEval (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α₀ : ZMod (F.order d)) (α : Fin n → ZMod (F.order d)) (x : BitString n) : F.Carrier d

Augmented-tree evaluation of the Naor–Reingold PRF from root α₀ • g along (α i, x i) for i : Fin n ([BS23], Exercise 10.4(a), p. 424, and Exercise 4.18, p. 172).

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldTreeFold_smul (F : PrimeOrderGroupFamily) (d : F.Desc) (β : ZMod (F.order d)) (u : F.Carrier d) (steps : List (ZMod (F.order d) × Bool)) : F.naorReingoldTreeFold d (β • u) steps = (β * (List.map (fun (p : ZMod (F.order d) × Bool) => if p.2 = true then p.1 else 1) steps).prod) • u

Folding naorReingoldStep starting from β • u multiplies the scalar β by the product of selected step exponents.

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldTreeEval_eq_naorReingoldEval (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α₀ : ZMod (F.order d)) (α : Fin n → ZMod (F.order d)) (x : BitString n) : F.naorReingoldTreeEval d α₀ α x = F.naorReingoldEval d α₀ α x

Boneh–Shoup Exercise 10.4(a): the augmented-tree construction naorReingoldTreeEval built from naorReingoldPRG ($G_{\mathrm{NR}}(\alpha, u) = (u, \alpha \bullet u)$) coincides with naorReingoldEval.

Word-level polynomial-time evaluation

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldProdNat (acc : ℕ) (steps : List (ℕ × Bool)) : ℕ

Multiply the selected natural-number exponents in steps starting from acc.

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldProdNat_cast (q acc : ℕ) (steps : List (ℕ × Bool)) : ↑(naorReingoldProdNat acc steps) = ↑acc * (List.map (fun (p : ℕ × Bool) => if p.2 = true then ↑p.1 else 1) steps).prod

Casting naorReingoldProdNat to ZMod q equals acc times the product of selected step exponents in ZMod q.

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldWordSuffix (F : PrimeOrderGroupFamily) (d : F.Desc) (u : List Bool) (αs : List ℕ) (xs : List Bool) : List Bool

Word-level suffix evaluation of the Naor–Reingold tree from an encoded group element u along αs and xs.

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldWordEval (F : PrimeOrderGroupFamily) (d : F.Desc) (α₀ : ℕ) (αs : List ℕ) (xs : List Bool) : List Bool

Word-level evaluation of the Naor–Reingold PRF on (d, α₀, αs, xs).

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldWordSuffix_encode (F : PrimeOrderGroupFamily) (d : F.Desc) (u : F.Carrier d) (αs : List ℕ) (xs : List Bool) : F.naorReingoldWordSuffix d (F.encode d u) αs xs = F.encode d (F.naorReingoldTreeFold d u (List.map (fun (p : ℕ × Bool) => (↑p.1, p.2)) (αs.zip xs)))

On an encoded group element F.encode d u, naorReingoldWordSuffix computes the encoding of naorReingoldTreeFold.

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldWordEval_eq_encode (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α₀ : ℕ) (α : Fin n → ℕ) (x : BitString n) : F.naorReingoldWordEval d α₀ (List.ofFn α) (List.ofFn x) = F.encode d (F.naorReingoldEval d (↑α₀) (fun (i : Fin n) => ↑(α i)) x)

Correctness of naorReingoldWordEval on an n-element exponent list αs and n-bit query xs.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_naorReingoldProdNat : Turing.MultiTapeTM.ComputableInPolyTime (fun (input : ℕ × List (ℕ × Bool)) => naorReingoldProdNat input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encNat

naorReingoldProdNat is computable in polynomial time.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_naorReingoldWordSuffix (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime (fun (input : F.Desc × List Bool × List ℕ × List Bool) => F.naorReingoldWordSuffix input.1 input.2.1 input.2.2.1 input.2.2.2) (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBits

naorReingoldWordSuffix is computable in polynomial time.

theorem Cslib.Crypto.PrimeOrderGroupFamily.computableInPolyTime_naorReingoldWordEval (F : PrimeOrderGroupFamily) : Turing.MultiTapeTM.ComputableInPolyTime (fun (input : F.Desc × ℕ × List ℕ × List Bool) => F.naorReingoldWordEval input.1 input.2.1 input.2.2.1 input.2.2.2) (Turing.MultiTapeTM.encPair F.encDesc (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBits

naorReingoldWordEval is computable in polynomial time.

Naor–Reingold PRF prefix hybrids and security reduction (Exercise 10.4(b))

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldSuffixExp (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (k : ℕ) (α : Fin n → ZMod (F.order d)) (x : BitString n) : ZMod (F.order d)

Suffix exponent product ∏ i : Fin n, if k ≤ i.1 ∧ x i then α i else 1 from depth k to n.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldSuffixExp_zero (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α₀ : ZMod (F.order d)) (α : Fin n → ZMod (F.order d)) (x : BitString n) : α₀ * F.naorReingoldSuffixExp d 0 α x = F.naorReingoldExp d α₀ α x

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldSuffixExp_self (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (α : Fin n → ZMod (F.order d)) (x : BitString n) : F.naorReingoldSuffixExp d n α x = 1

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldSuffixExp_eq_mul_succ (F : PrimeOrderGroupFamily) (d : F.Desc) {n k : ℕ} (hk : k < n) (α : Fin n → ZMod (F.order d)) (x : BitString n) : F.naorReingoldSuffixExp d k α x = (if x ⟨k, hk⟩ = true then α ⟨k, hk⟩ else 1) * F.naorReingoldSuffixExp d (k + 1) α x

Splitting naorReingoldSuffixExp at depth k < n into the k-th bit factor and the depth k + 1 suffix.

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldSuffixExp_succ_update (F : PrimeOrderGroupFamily) (d : F.Desc) {n k : ℕ} (hk : k < n) (α : Fin n → ZMod (F.order d)) (a : ZMod (F.order d)) (x : BitString n) : F.naorReingoldSuffixExp d (k + 1) (Function.update α ⟨k, hk⟩ a) x = F.naorReingoldSuffixExp d (k + 1) α x

Updating α at ⟨k, hk⟩ does not affect naorReingoldSuffixExp at depth k + 1.

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHybridEval (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (k : ℕ) (B : BitString k → ZMod (F.order d)) (α : Fin n → ZMod (F.order d)) (x : BitString n) : F.Carrier d

Hybrid function at depth k: look up the k-bit prefix in B : BitString k → ZMod (F.order d) and multiply by the remaining suffix exponent product from k to n.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldEvalWithFn (F : PrimeOrderGroupFamily) (d : F.Desc) (n : ℕ) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) (fn : BitString n → F.Carrier d) : PMF Bool

Run an adaptive oracle distinguisher adv against a deterministic function fn : BitString n → F.Carrier d.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldRealGame (F : PrimeOrderGroupFamily) (d : F.Desc) (n : ℕ) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) : Game

The real Naor–Reingold PRF experiment at group d and input length n ([BS23], Section 10.11, Exercise 10.4, p. 424).

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldIdealGame (F : PrimeOrderGroupFamily) (d : F.Desc) (n : ℕ) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) : Game

The ideal random-function experiment at group d and input length n: a uniformly random function BitString n → F.Carrier d represented via B ← PMF.uniformOfFintype (BitString n → ZMod (F.order d)) and the bijection β ↦ β • g.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHybridGame (F : PrimeOrderGroupFamily) (d : F.Desc) (n k : ℕ) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) : Game

The depth-k Naor–Reingold prefix-hybrid experiment ($0 \le k \le n$): queries share a uniform random function B : BitString k → ZMod (F.order d) on k-bit prefixes and evaluate the remaining suffix bits with α : Fin n → ZMod (F.order d) ([BS23], Exercise 10.4 & Exercise 4.18).

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHybridGame_zero (F : PrimeOrderGroupFamily) (d : F.Desc) (n : ℕ) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) : F.naorReingoldHybridGame d n 0 adv = F.naorReingoldRealGame d n adv

At depth 0, naorReingoldHybridGame is the real Naor–Reingold PRF experiment.

@[simp]

theorem Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHybridGame_self (F : PrimeOrderGroupFamily) (d : F.Desc) (n : ℕ) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) : F.naorReingoldHybridGame d n n adv = F.naorReingoldIdealGame d n adv

At depth n, naorReingoldHybridGame is the ideal random-function experiment.

def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldTableEval (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (k : ℕ) (hk : k < n) (T : BitString k → F.Carrier d × F.Carrier d) (α : Fin n → ZMod (F.order d)) (x : BitString n) : F.Carrier d

Evaluating the level-k child table T : BitString k → F.Carrier d × F.Carrier d followed by the depth-(k + 1) suffix exponent product.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldLevelTest (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (k : ℕ) (hk : k < n) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) (_u : F.Carrier d) (T : BitString k → F.Carrier d × F.Carrier d) : PMF Bool

Level-k Multi-DDH test induced by a Naor–Reingold PRF adversary adv: draw suffix exponents α ← PMF.uniformOfFintype (Fin n → ZMod (F.order d)) and run adv against naorReingoldTableEval.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldLevelDDHDistinguisher (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (k : ℕ) (hk : k < n) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) (t : F.Carrier d × F.Carrier d × F.Carrier d) : PMF Bool

Single-level DDH distinguisher at depth k < n: given a candidate DDH triple (u, v, w), rerandomize it into a BitString k-indexed family via multiDDHRerandomizeLaw and run naorReingoldLevelTest.

theorem Cslib.Crypto.PrimeOrderGroupFamily.multiDDHRealTupleLaw_naorReingoldLevelTest (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (k : ℕ) (hk : k < n) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) : ((Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (α_k : ZMod (F.order d)) => (F.multiDDHRealTupleLaw d (BitString k) α_k).bind (F.naorReingoldLevelTest d k hk adv (α_k • F.generator d))) = F.naorReingoldHybridGame d n k adv

Under multiDDHRealTupleLaw, naorReingoldLevelTest reproduces naorReingoldHybridGame at depth k.

theorem Cslib.Crypto.PrimeOrderGroupFamily.multiDDHIdealTupleLaw_naorReingoldLevelTest (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (k : ℕ) (hk : k < n) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) : ((Probability.PMF.uniformOfFintype (ZMod (F.order d))).bind fun (α_k : ZMod (F.order d)) => (F.multiDDHIdealTupleLaw d (BitString k)).bind (F.naorReingoldLevelTest d k hk adv (α_k • F.generator d))) = F.naorReingoldHybridGame d n (k + 1) adv

Under multiDDHIdealTupleLaw, naorReingoldLevelTest reproduces naorReingoldHybridGame at depth k + 1.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingoldHybridGame_succ_le (F : PrimeOrderGroupFamily) (d : F.Desc) {n : ℕ} (k : ℕ) (hk : k < n) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) : (F.naorReingoldHybridGame d n k adv).advantage (F.naorReingoldHybridGame d n (k + 1) adv) ≤ Game.advantage ((F.ddhRealTupleLaw d).bind (F.naorReingoldLevelDDHDistinguisher d k hk adv)) ((F.ddhIdealTupleLaw d).bind (F.naorReingoldLevelDDHDistinguisher d k hk adv)) + (↑(F.order d))⁻¹

Single-level Naor–Reingold prefix-hybrid bound: for every k < n, the advantage between naorReingoldHybridGame at depth k and depth k + 1 is at most the DDH distinguishing advantage of naorReingoldLevelDDHDistinguisher d k hk adv plus (F.order d)⁻¹.

noncomputable def Cslib.Crypto.PrimeOrderGroupFamily.naorReingoldHopDDHDistinguisher (F : PrimeOrderGroupFamily) (d : F.Desc) (n k : ℕ) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) (t : F.Carrier d × F.Carrier d × F.Carrier d) : PMF Bool

Total- parameterized level DDH distinguisher (returning PMF.pure false when k ≥ n).

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingold_le_sum (F : PrimeOrderGroupFamily) (d : F.Desc) (n : ℕ) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) : (F.naorReingoldRealGame d n adv).advantage (F.naorReingoldIdealGame d n adv) ≤ ∑ k ∈ Finset.range n, Game.advantage ((F.ddhRealTupleLaw d).bind (F.naorReingoldHopDDHDistinguisher d n k adv)) ((F.ddhIdealTupleLaw d).bind (F.naorReingoldHopDDHDistinguisher d n k adv)) + ↑n * (↑(F.order d))⁻¹

Naor–Reingold PRF distributional prefix-hybrid bound (∑ k < n bound, [BS23], Exercise 10.4; [NR04], Theorem 4.1): the distinguishing advantage between naorReingoldRealGame and naorReingoldIdealGame is bounded by the sum over k ∈ Finset.range n of the DDH distinguishing advantages of the explicit 2^k-pair PMF distinguisher naorReingoldLevelDDHDistinguisher (naorReingoldHopDDHDistinguisher) plus n * (F.order d)⁻¹.

theorem Cslib.Crypto.PrimeOrderGroupFamily.advantage_naorReingold_le_mul (F : PrimeOrderGroupFamily) (d : F.Desc) (n : ℕ) (adv : OracleComp (fun (x : BitString n) => F.Carrier d) Bool) (ε : NNReal) (hε : ∀ k < n, Game.advantage ((F.ddhRealTupleLaw d).bind (F.naorReingoldHopDDHDistinguisher d n k adv)) ((F.ddhIdealTupleLaw d).bind (F.naorReingoldHopDDHDistinguisher d n k adv)) ≤ ε) : (F.naorReingoldRealGame d n adv).advantage (F.naorReingoldIdealGame d n adv) ≤ ↑n * (ε + (↑(F.order d))⁻¹)

Common-bound Naor–Reingold PRF distributional prefix-hybrid bound ([BS23], Exercise 10.4; [NR04], Theorem 4.1): if for every k < n the explicit 2^k-pair PMF distinguisher naorReingoldHopDDHDistinguisher d n k adv has DDH advantage at most ε, then the Naor–Reingold PRF advantage is at most n * (ε + (F.order d)⁻¹).