One-Way Function (OWF) Assumption

A one-way function is easy to compute but hard to invert: given f(x), no efficient adversary can find any preimage x' such that f(x') = f(x).

Main definitions

• OWFDef — abstract one-way function
• OWF_Game — the one-wayness game
• OWF_Advantage — inversion probability
• OWFSecure — one-wayness assumption
• OWPDef — one-way permutation (bijective OWF)
• PRGDef — pseudorandom generator definition
• PRG_Advantage — PRG distinguishing advantage
• prg_implies_owf — PRG ⟹ OWF reduction (BS Thm 8.1)

Cross-Validation

Property	This file	Textbook
OWF Game	OWF_Game	BS Def. 8.1 / KL Def. 8.1
OWF Advantage	OWF_Advantage	Pr[Invert]
OWP	OWPDef	BS Def. 8.2 (permutation variant)
PRG	PRGDef	BS Def. 3.1
PRG ⟹ OWF	prg_implies_owf	BS Thm 8.1

Equivalent formalizations:

• EasyCrypt: OW game in OW.ec
• SSProve (Rocq): not formalized

Relationship to other assumptions:

• PRG ⟹ OWF (BS Thm 8.1): prg_implies_owf
• PRF ⟹ OWF (standard)
• RSA is an OWP instance (see RSA.lean)

References

• Boneh & Shoup, A Graduate Course in Applied Cryptography, §8.1, Def. 8.1; §3.1
• Katz & Lindell, Introduction to Modern Cryptography, §8.1, Def. 8.1

One-Way Function

structure CatCrypt.Crypto.Assumptions.OWFDef (W : Type) : Type

Abstract one-way function: a function that is easy to compute but hard to invert.

• f : W → W

  The one-way function

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.OWF_Adversary (W : Type) : Type

OWF adversary: given f(x), attempts to find a preimage.

Equations

• CatCrypt.Crypto.Assumptions.OWF_Adversary W = (W → CatCrypt.Core.SPComp W)

noncomputable def CatCrypt.Crypto.Assumptions.OWF_Game {W : Type} [Fintype W] [Nonempty W] [DecidableEq W] (F : OWFDef W) (A : OWF_Adversary W) : Core.SPComp Bool

OWF game: sample x, give f(x) to adversary, check if the adversary's output x' satisfies f(x') = f(x).

Note: the adversary need not find x itself, just any preimage.

Equations

• CatCrypt.Crypto.Assumptions.OWF_Game F A = do let x ← CatCrypt.Core.SPComp.sample W have y : W := F.f x let x' ← A y CatCrypt.Core.SPComp.pure (decide (F.f x' = y))

noncomputable def CatCrypt.Crypto.Assumptions.OWF_Advantage {W : Type} [Fintype W] [Nonempty W] [DecidableEq W] (F : OWFDef W) (A : OWF_Adversary W) : ENNReal

OWF advantage: probability of finding a preimage.

Equations

• CatCrypt.Crypto.Assumptions.OWF_Advantage F A = CatCrypt.Crypto.prTrue (CatCrypt.Crypto.Assumptions.OWF_Game F A) CatCrypt.Core.Heap.empty

def CatCrypt.Crypto.Assumptions.OWFSecure {W : Type} [Fintype W] [Nonempty W] [DecidableEq W] (F : OWFDef W) (ε : ENNReal) : Prop

One-wayness assumption.

Equations

• CatCrypt.Crypto.Assumptions.OWFSecure F ε = ∀ (A : CatCrypt.Crypto.Assumptions.OWF_Adversary W), CatCrypt.Crypto.Assumptions.OWF_Advantage F A ≤ ε

One-Way Permutation (OWP)

structure CatCrypt.Crypto.Assumptions.OWPDef (W : Type) extends CatCrypt.Crypto.Assumptions.OWFDef W : Type

A one-way permutation: a bijective one-way function.

• f : W → W
• bij : Function.Bijective self.f

  The function is a bijection

IsPure Proofs

theorem CatCrypt.Crypto.Assumptions.OWF_Game_isPure {W : Type} [Fintype W] [Nonempty W] [DecidableEq W] (F : OWFDef W) (A : OWF_Adversary W) (hA : ∀ (y : W), (A y).IsPure) : (OWF_Game F A).IsPure

Pseudorandom Generator (PRG)

A PRG stretches a short seed into a longer (or same-length) output that is computationally indistinguishable from uniform.

structure CatCrypt.Crypto.Assumptions.PRGDef (Seed Output : Type) : Type

Abstract pseudorandom generator: a deterministic function from seeds to outputs.

• stretch : Seed → Output

  The stretch function

noncomputable def CatCrypt.Crypto.Assumptions.prg_real {Seed Output : Type} [Fintype Seed] [Nonempty Seed] (G : PRGDef Seed Output) : Core.SPComp Output

PRG real game: sample a seed, output G(seed).

Equations

• CatCrypt.Crypto.Assumptions.prg_real G = do let seed ← CatCrypt.Core.SPComp.sample Seed CatCrypt.Core.SPComp.pure (G.stretch seed)

noncomputable def CatCrypt.Crypto.Assumptions.prg_ideal {Output : Type} [Fintype Output] [Nonempty Output] : Core.SPComp Output

PRG ideal game: sample output uniformly.

Equations

• CatCrypt.Crypto.Assumptions.prg_ideal = CatCrypt.Core.SPComp.sample Output

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.PRG_Adversary (Output : Type) : Type

PRG adversary: a distinguisher that receives a sample and outputs a bit.

Equations

• CatCrypt.Crypto.Assumptions.PRG_Adversary Output = (Output → CatCrypt.Core.SPComp Bool)

noncomputable def CatCrypt.Crypto.Assumptions.PRG_Advantage {Seed Output : Type} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : PRGDef Seed Output) (A : PRG_Adversary Output) : ENNReal

PRG advantage: ability to distinguish G(seed) from random.

Equations

• CatCrypt.Crypto.Assumptions.PRG_Advantage G A = CatCrypt.Crypto.AdvantageA (CatCrypt.Crypto.Assumptions.prg_real G) CatCrypt.Crypto.Assumptions.prg_ideal A

def CatCrypt.Crypto.Assumptions.PRGSecure {Seed Output : Type} [Fintype Seed] [Nonempty Seed] [Fintype Output] [Nonempty Output] (G : PRGDef Seed Output) (ε : ENNReal) : Prop

PRG security assumption.

Equations

• CatCrypt.Crypto.Assumptions.PRGSecure G ε = ∀ (A : CatCrypt.Crypto.Assumptions.PRG_Adversary Output), CatCrypt.Crypto.Assumptions.PRG_Advantage G A ≤ ε

PRG ⟹ OWF Reduction

If G : Seed → Output is a PRG (pseudorandom generator), then G is also a one-way function on Seed (when Output = Seed). The reduction: an OWF inverter for G would distinguish real from random, since the preimage reveals the seed.

BS Thm 8.1: if G is a secure PRG, then G is a secure OWF.

Reduction idea. Given an OWF adversary A_owf that inverts G, construct a PRG distinguisher A_prg as follows:

1. Receive challenge y (either G(s) for random s, or truly random)
2. Run A_owf(y) to get candidate seed s'
3. Output decide (G(s') = y)

If y = G(s) (real case), then A_owf succeeds with noticeable probability, so A_prg outputs true. If y is random, G(s') = y is unlikely since G's image is sparse in the output space.

The bound: OWF_Advantage G A_owf ≤ PRG_Advantage G A_prg.

def CatCrypt.Crypto.Assumptions.owf_of_prg {S : Type} (stretch : S → S) : OWFDef S

Construct an OWF from a PRG stretch function (same-type case).

Given PRG G : S → S, define f = G. For PRGs with distinct seed/output types, the one-wayness notion applies on the seed space viewed as the domain.

Equations

• CatCrypt.Crypto.Assumptions.owf_of_prg stretch = { f := stretch }

noncomputable def CatCrypt.Crypto.Assumptions.prg_distinguisher_of_owf_inverter {W : Type} [DecidableEq W] (G : PRGDef W W) (A_owf : OWF_Adversary W) : PRG_Adversary W

Construct a PRG distinguisher from an OWF inverter.

Given an OWF adversary A_owf that tries to invert G:

1. Receive challenge y
2. Run A_owf(y) to get candidate preimage s'
3. Output true iff G(s') = y

In the real game (y = G(s)), A_owf succeeds iff it finds a preimage. In the ideal game (y random), the output is essentially random.

Equations

• CatCrypt.Crypto.Assumptions.prg_distinguisher_of_owf_inverter G A_owf y = do let s' ← A_owf y CatCrypt.Core.SPComp.pure (decide (G.stretch s' = y))

class CatCrypt.Crypto.Assumptions.PRGImpliesOWF {W : Type} [Fintype W] [Nonempty W] [DecidableEq W] (G : PRGDef W W) : Prop

PRG ⟹ OWF reduction bound (Bertie pattern, BS Thm 8.1).

The tight bound requires image sparsity: for same-type PRGs (W → W), the OWF advantage includes a |im(G)|/|W| term for the probability of inverting a truly random value. This is provided as a typeclass.

• bound (A_owf : OWF_Adversary W) : OWF_Advantage (owf_of_prg G.stretch) A_owf ≤ PRG_Advantage G (prg_distinguisher_of_owf_inverter G A_owf)

theorem CatCrypt.Crypto.Assumptions.prg_implies_owf {W : Type} [Fintype W] [Nonempty W] [DecidableEq W] (G : PRGDef W W) [PRGImpliesOWF G] (A_owf : OWF_Adversary W) : OWF_Advantage (owf_of_prg G.stretch) A_owf ≤ PRG_Advantage G (prg_distinguisher_of_owf_inverter G A_owf)

theorem CatCrypt.Crypto.Assumptions.prg_secure_implies_owf_secure {W : Type} [Fintype W] [Nonempty W] [DecidableEq W] (G : PRGDef W W) [PRGImpliesOWF G] (ε : ENNReal) (h_prg : PRGSecure G ε) : OWFSecure (owf_of_prg G.stretch) ε

Corollary: PRG security implies OWF security.

If G is ε-PRG-secure, then owf_of_prg G.stretch is ε-OWF-secure.

RSA as OWP

The RSA function (modular exponentiation x ↦ x^e mod N for suitable (N, e)) is conjectured to be a one-way permutation. The formal connection is via RSADef in Assumptions/RSA.lean. An OWPDef instance for RSA would require proving Function.Bijective for the RSA map, which needs number-theoretic facts about the RSA group structure.