Multi-Query PRF Security via Hybrid Argument

This file provides the standard q-fold hybrid argument for bounding the advantage of a q-query PRF adversary:

`Adv_q(F) ≤ q · Adv_1(F)`

Overview

Given a PRF F : K → D → R, the q-query PRF game answers q queries. The hybrid argument interpolates between real and ideal:

• Hybrid 0: All queries answered by F(k, ·) (real)
• Hybrid i: First i queries answered by random function, rest by F(k, ·)
• Hybrid q: All queries answered by random function (ideal)

Each adjacent pair of hybrids differs by exactly one query, and the advantage of distinguishing them is bounded by the single-query PRF advantage. The total advantage is then at most q · ε₁.

Key Theorems

• prf_multi_query_bound — Adv(hyb 0, hyb q) ≤ q · ε via advantage_hybrid_uniform
• prf_multi_query_perfect — Zero advantage when each step is perfectly secure
• prf_multi_query_nested — Nested hybrid: Adv ≤ m · q · ε

References

• [Bellare & Rogaway, Introduction to Modern Cryptography]
• [Rosulek, The Joy of Cryptography, Claim 6.1]

Abstract PRF Specification

structure CatCrypt.Crypto.MultiQueryPRF.PRFSpec (K D R : Type) [Fintype K] [Nonempty K] [Fintype R] [Nonempty R] : Type

Abstract PRF specification parameterized by key, domain, and range types.

• eval : K → D → R

  The PRF evaluation function

Single-Query PRF Games

noncomputable def CatCrypt.Crypto.MultiQueryPRF.prf_query_real {K D R : Type} [Fintype K] [Nonempty K] [Fintype R] [Nonempty R] (F : PRFSpec K D R) (x : D) : Core.SPComp R

Single-query real PRF game: sample key, return F(k, x)

Equations

• CatCrypt.Crypto.MultiQueryPRF.prf_query_real F x = do let k ← CatCrypt.Core.SPComp.sample K CatCrypt.Core.SPComp.pure (F.eval k x)

noncomputable def CatCrypt.Crypto.MultiQueryPRF.prf_query_ideal {D R : Type} [Fintype R] [Nonempty R] (_x : D) : Core.SPComp R

Single-query ideal PRF game: return random R

Equations

• CatCrypt.Crypto.MultiQueryPRF.prf_query_ideal _x = CatCrypt.Core.SPComp.sample R

noncomputable def CatCrypt.Crypto.MultiQueryPRF.prf_adv1 {K D R : Type} [Fintype K] [Nonempty K] [Fintype R] [Nonempty R] (F : PRFSpec K D R) (x : D) (A : R → Core.SPComp Bool) : ENNReal

Single-query PRF advantage for query x

Equations

• CatCrypt.Crypto.MultiQueryPRF.prf_adv1 F x A = CatCrypt.Crypto.AdvantageA (CatCrypt.Crypto.MultiQueryPRF.prf_query_real F x) (CatCrypt.Crypto.MultiQueryPRF.prf_query_ideal x) A

Multi-Query Hybrid Games

The q-query hybrid game is parameterized by a natural number i.
We use an **abstract** hybrid sequence indexed by ℕ, where:
- G 0 = all-real game
- G q = all-ideal game
- G i differs from G (i+1) in exactly one query position

The concrete construction of these hybrids depends on the query model.
Here we provide the general-purpose bound that works for any such sequence.

theorem CatCrypt.Crypto.MultiQueryPRF.prf_multi_query_bound {α : Type} (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (q : ℕ) (ε : ENNReal) (hstep : ∀ i < q, AdvantageA (G i) (G (i + 1)) A ≤ ε) : AdvantageA (G 0) (G q) A ≤ ↑q * ε

Multi-query PRF security bound: the q-query advantage is at most q · ε.

Given a sequence of q hybrid games G where each adjacent pair differs by at most ε, the total advantage is at most q · ε.

In the PRF setting:

• G 0 = real game (all queries answered by PRF)
• G q = ideal game (all queries answered randomly)
• Each G i → G (i+1) changes one query from real to random

theorem CatCrypt.Crypto.MultiQueryPRF.prf_multi_query_dep_bound {α : Type} (real ideal : Core.SPComp α) (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (q : ℕ) (ε : ℕ → ENNReal) (hleft : real = G 0) (hright : ideal = G q) (hstep : ∀ i < q, AdvantageA (G i) (G (i + 1)) A ≤ ε i) : AdvantageA real ideal A ≤ ∑ i ∈ Finset.range q, ε i

Multi-query PRF with dependent step bounds: different queries may have different single-query advantages.

theorem CatCrypt.Crypto.MultiQueryPRF.prf_multi_query_perfect {α : Type} (G : ℕ → Core.SPComp α) (q : ℕ) (hperf : ∀ i < q, Relational.rHoare Relational.eqPre (G i) (G (i + 1)) Relational.eqPost) (A : α → Core.SPComp Bool) : AdvantageA (G 0) (G q) A = 0

Perfect multi-query PRF: when all steps are perfectly indistinguishable, the multi-query advantage is 0.

theorem CatCrypt.Crypto.MultiQueryPRF.prf_multi_query_nested {α : Type} (G : ℕ → Core.SPComp α) (A : α → Core.SPComp Bool) (m q : ℕ) (ε : ENNReal) (hstep : ∀ i < m, AdvantageA (G i) (G (i + 1)) A ≤ ↑q * ε) : AdvantageA (G 0) (G m) A ≤ ↑m * ↑q * ε

Nested multi-query bound: for a two-level hybrid argument (e.g., multi-instance × multi-query), the total advantage is m · q · ε.