Keyed PRF Security Assumption

A PRFAssumption F packages the standard cryptographic hypothesis that a keyed function family F is a secure pseudorandom function: there is an advantage bound ε such that every single-query adversary distinguishes the keyed evaluation F(k, ·) (with a uniform key) from a fresh uniform output with advantage at most ε.

This is the reusable "PRF is ε-secure" assumption structure that reductions take as a hypothesis. It is parameterized over the abstract PRFScheme of SecurityDefs, so it composes with PRF_Real / PRF_Ideal / PRF_Adv.

Main definitions

• PRFAssumption F — the record ⟨ε, bound⟩ asserting PRF_Adv F x A ≤ ε for all inputs x and adversaries A.
• PRFAssumption.advantage_bound — the packaged advantage bound.

Main results

• PRFAssumption.of_perfect — a perfectly secure PRF (PRF_Adv = 0) satisfies the assumption with ε = 0.

References

• [Bellare & Rogaway, Introduction to Modern Cryptography]
• [Rosulek, The Joy of Cryptography, §6]

structure CatCrypt.Crypto.PRFAssumption (F : SecurityDefs.PRFScheme) : Type

The keyed PRF security assumption: F is an ε-secure pseudorandom function. The field bound witnesses that no single-query adversary beats advantage ε at distinguishing PRF_Real F x from PRF_Ideal F.

• ε : ENNReal

  The PRF advantage bound ε.

• bound (x : F.Input) (A : F.Output → Core.SPComp Bool) : SecurityDefs.PRF_Adv F x A ≤ self.ε

  Every single-query adversary has PRF advantage at most ε.

theorem CatCrypt.Crypto.PRFAssumption.advantage_bound {F : SecurityDefs.PRFScheme} (H : PRFAssumption F) (x : F.Input) (A : F.Output → Core.SPComp Bool) : SecurityDefs.PRF_Adv F x A ≤ H.ε

The packaged advantage bound of a PRF assumption.

def CatCrypt.Crypto.PRFAssumption.of_perfect (F : SecurityDefs.PRFScheme) (h : ∀ (x : F.Input) (A : F.Output → Core.SPComp Bool), SecurityDefs.PRF_Adv F x A = 0) : PRFAssumption F

A perfectly secure PRF (every adversary has advantage exactly 0) satisfies the PRF assumption with ε = 0.

Equations

• CatCrypt.Crypto.PRFAssumption.of_perfect F h = { ε := 0, bound := ⋯ }