Weak One-Way Functions, Output Normalization, and Schedule Reindexing

This module defines $\alpha$-weak one-way functions (Cslib.Crypto.WeakOneWayAt) and weak one-way functions (Cslib.Crypto.WeakOneWay) against uniform strict PPT inverters following Y. Liu and R. Pass, On One-Way Functions and Kolmogorov Complexity (Definition 2.2, §2.1, p. 7 of arXiv:2009.11514v1; FOCS 2020, p. 1246), originally due to A. C. Yao and treated in O. Goldreich, Foundations of Cryptography, Volume 1 (§2.2.2, Definition 2.2.2).

In addition to basic monotonicity, < vs. ≤ equivalence bridges, strong-implies-weak specialization (Cslib.Crypto.OneWay.weakOneWay), and negative nonvacuity witnesses (Cslib.Crypto.not_weakOneWay_const), this module provides two structural transformations reused by Yao's direct-product hardness amplification and the Liu–Pass Section 4 converse construction:

1. Fixed-output-length normalization (Cslib.Crypto.WeakOneWay.exists_fixedOutputLength): Every weak one-way function yields a weak one-way function whose output length depends only on the input length, reusing self-delimiting padding from Complexity.Crypto.Computational.OneWay.Normalize.
2. Schedule reindexing (Cslib.Crypto.OneWayReindex.reindex): Given an input-length schedule m : ℕ → ℕ with m n ≥ n + 1 computable in unary polynomial time and a parameter-indexed family core : ℕ → List Bool → List Bool defined on inputs of length m n, OneWayReindex.reindex m core extends the family to all input lengths $M \in \mathbb{N}$ by finding the greatest parameter $n$ with $m(n) \le M$ (GeneratorReindex.parameter), evaluating core n on the $m(n)$-bit prefix, and pairing the core output with the parameter $n$ in unary (wrappedImage). This is a library variant and generalization of the input-truncation padding trick in Liu and Pass, Proof of Theorem 4.1, §4, p. 10 of arXiv:2009.11514v1 (cf. the length-extension convention of Goldreich, Vol. 1, §2.2.3, Proposition 2.2.3), with the parameter $n$ appended to the output so images from distinct parameters are disjoint and the reduction is lossless even for nonmonotone schedules. Both weak one-wayness (OneWayReindex.weakOneWay) and strong one-wayness (OneWayReindex.oneWay) transfer from the parameter-indexed game familyInversionGame to all input lengths.

Main definitions

• Cslib.Crypto.WeakOneWayAt: $\alpha$-weak one-way function against uniform strict PPT inverters (Liu and Pass, Definition 2.2, §2.1, p. 7 of arXiv:2009.11514v1).
• Cslib.Crypto.WeakOneWay: weak one-way function ($\frac{1}{q(\cdot)}$-weak OWF for some positive polynomial $q$, Liu and Pass, Definition 2.2, §2.1, p. 7 of arXiv:2009.11514v1).
• Cslib.Crypto.OneWayReindex.reindex: extend a parameter-indexed family on input lengths m n to all binary strings.
• Cslib.Crypto.OneWayReindex.familyInversionGame: the parameter-indexed inversion experiment on inputs of length m n.

Main results

• Cslib.Crypto.weakOneWay_iff_le, Cslib.Crypto.WeakOneWay.of_le: equivalence between < 1 - 1/q(n) and ≤ 1 - 1/q(n) formulations of WeakOneWay.
• Cslib.Crypto.WeakOneWay.exists_monotone_poly: every weak OWF admits a monotone polynomial bound $q(n) \ge n + 1$.
• Cslib.Crypto.OneWay.weakOneWay: every strong one-way function is a weak one-way function.
• Cslib.Crypto.not_weakOneWay_of_inverse, Cslib.Crypto.not_weakOneWay_const: efficient right-inverses and constant functions refute weak one-wayness.
• Cslib.Crypto.WeakOneWay.normalize, Cslib.Crypto.WeakOneWay.exists_fixedOutputLength: output-length normalization preserves weak one-wayness.
• Cslib.Crypto.OneWayReindex.exists_familyInverter_inversion_le: any PPT inverter against reindex m core at length M ≥ m 0 reduces without probability loss to a uniform PPT inverter in familyInversionGame at parameter GeneratorReindex.parameter m M.
• Cslib.Crypto.OneWayReindex.weakOneWay, Cslib.Crypto.OneWayReindex.oneWay: weak and strong one-wayness transfer from familyInversionGame on m n to reindex m core on all input lengths.

References

• Y. Liu and R. Pass, On One-Way Functions and Kolmogorov Complexity, full version arXiv:2009.11514v1 (Section 2.1, Definition 2.2 and Section 4, Theorem 4.1).
• A. C. Yao, Theory and Application of Trapdoor Functions.
• O. Goldreich, Foundations of Cryptography, Volume 1, Sections 2.2.2–2.2.3.

Weak one-way functions

(Liu and Pass, Definition 2.2, §2.1, p. 7 of arXiv:2009.11514v1)

structure Cslib.Crypto.WeakOneWayAt (f : List Bool → List Bool) (α : ℕ → ℝ) : Prop

Liu and Pass, Definition 2.2, §2.1, p. 7 of arXiv:2009.11514v1: $\alpha$-weak one-way function (WeakOneWayAt). A polynomial-time computable function $f : \{0, 1\}^* \to \{0, 1\}^*$ is an $\alpha$-weak one-way function if for every uniform strict PPT inverter $\mathcal{A}$, for all sufficiently large $n \in \mathbb{N}$, $$\Pr_{x \leftarrow \{0, 1\}^n}[\mathcal{A}(1^n, f(x)) \in f^{-1}(f(x))] < 1 - \alpha(n).$$

• polyTime : Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

  A deterministic polynomial-time algorithm evaluates the function.

• weak (adversary : Inverter) : Probability.IsPPT Turing.MultiTapeTM.encBits adversary → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Game.succProbability (inversionGame f adversary n).eval) < 1 - α n

  Every uniform strict PPT inverter succeeds with probability < 1 - α n eventually.

def Cslib.Crypto.WeakOneWay (f : List Bool → List Bool) : Prop

Liu and Pass, Definition 2.2, §2.1, p. 7 of arXiv:2009.11514v1: Weak one-way function (WeakOneWay). A function $f : \{0, 1\}^* \to \{0, 1\}^*$ is a weak one-way function if there exists a positive polynomial $q \in \mathbb{N}[X]$ ($\forall n,\, 0 < q(n)$) such that $f$ is a $\frac{1}{q(\cdot)}$-weak one-way function.

theorem Cslib.Crypto.WeakOneWay.polyTime {f : List Bool → List Bool} (hf : WeakOneWay f) : Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

Extract the polynomial-time certificate from WeakOneWay.

theorem Cslib.Crypto.WeakOneWayAt.mono {f : List Bool → List Bool} {α₁ α₂ : ℕ → ℝ} (hf : WeakOneWayAt f α₂) (hα : ∀ᶠ (n : ℕ) in Filter.atTop, α₁ n ≤ α₂ n) : WeakOneWayAt f α₁

Monotonicity of WeakOneWayAt in the failure threshold $\alpha$.

theorem Cslib.Crypto.WeakOneWayAt.of_le {f : List Bool → List Bool} {α₁ α₂ : ℕ → ℝ} (hf : Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hα : ∀ᶠ (n : ℕ) in Filter.atTop, α₁ n < α₂ n) (h : ∀ (adversary : Inverter), Probability.IsPPT Turing.MultiTapeTM.encBits adversary → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Game.succProbability (inversionGame f adversary n).eval) ≤ 1 - α₂ n) : WeakOneWayAt f α₁

Establish WeakOneWayAt f α₁ from a non-strict bound ≤ 1 - α₂ n when α₁ n < α₂ n eventually.

theorem Cslib.Crypto.WeakOneWay.of_le {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) {q : Polynomial ℕ} (hq : ∀ (n : ℕ), 0 < Polynomial.eval n q) (h : ∀ (adversary : Inverter), Probability.IsPPT Turing.MultiTapeTM.encBits adversary → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Game.succProbability (inversionGame f adversary n).eval) ≤ 1 - 1 / ↑(Polynomial.eval n q)) : WeakOneWay f

Establish WeakOneWay f from a non-strict bound ≤ 1 - 1 / q(n) for a positive polynomial $q$, by doubling the polynomial to $2 q$.

theorem Cslib.Crypto.weakOneWay_iff_le {f : List Bool → List Bool} : WeakOneWay f ↔ Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits ∧ ∃ (q : Polynomial ℕ), (∀ (n : ℕ), 0 < Polynomial.eval n q) ∧ ∀ (adversary : Inverter), Probability.IsPPT Turing.MultiTapeTM.encBits adversary → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Game.succProbability (inversionGame f adversary n).eval) ≤ 1 - 1 / ↑(Polynomial.eval n q)

Equivalence between the strict (< 1 - 1 / q(n)) and non-strict (≤ 1 - 1 / q(n)) formulations of WeakOneWay.

theorem Cslib.Crypto.WeakOneWay.exists_monotone_poly {f : List Bool → List Bool} (hf : WeakOneWay f) : ∃ (q : Polynomial ℕ), (∀ (n : ℕ), n + 1 ≤ Polynomial.eval n q) ∧ (Monotone fun (x : ℕ) => Polynomial.eval x q) ∧ WeakOneWayAt f fun (n : ℕ) => 1 / ↑(Polynomial.eval n q)

Every weak one-way function admits a monotone polynomial $q \in \mathbb{N}[X]$ with $q(n) \ge n + 1$ for all $n$ such that WeakOneWayAt f (fun n => 1 / (q.eval n : ℝ)).

theorem Cslib.Crypto.OneWay.weakOneWayAt_half {f : List Bool → List Bool} (hf : OneWay f) : WeakOneWayAt f fun (x : ℕ) => 1 / 2

Every strong one-way function is a $\frac{1}{2}$-weak one-way function.

theorem Cslib.Crypto.OneWay.weakOneWay {f : List Bool → List Bool} (hf : OneWay f) : WeakOneWay f

Every strong one-way function is a weak one-way function.

Negative / nonvacuity witnesses

theorem Cslib.Crypto.not_weakOneWayAt_of_inverse {f : List Bool → List Bool} {α : ℕ → ℝ} (hα : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < α n) (inverse : ℕ → List Bool → List Bool) (hPPT : Probability.IsPPT Turing.MultiTapeTM.encBits fun (n : ℕ) (y : List Bool) => pure (inverse n y)) (hinv : ∀ (x : List Bool), f (inverse x.length (f x)) = f x) : ¬WeakOneWayAt f α

Efficiently finding any preimage, told the input length, refutes WeakOneWayAt whenever $\alpha(n) > 0$ eventually.

theorem Cslib.Crypto.not_weakOneWay_of_inverse {f : List Bool → List Bool} (inverse : ℕ → List Bool → List Bool) (hPPT : Probability.IsPPT Turing.MultiTapeTM.encBits fun (n : ℕ) (y : List Bool) => pure (inverse n y)) (hinv : ∀ (x : List Bool), f (inverse x.length (f x)) = f x) : ¬WeakOneWay f

Efficiently finding any preimage, told the input length, refutes WeakOneWay.

theorem Cslib.Crypto.not_weakOneWay_const (word : List Bool) : ¬WeakOneWay fun (x : List Bool) => word

Constant functions are not weakly one-way: the empty word is always a preimage.

Output-length normalization for weak one-way functions

theorem Cslib.Crypto.WeakOneWayAt.normalize {f : List Bool → List Bool} {α : ℕ → ℝ} (hf : WeakOneWayAt f α) (bound : ℕ → ℕ) (hbound : Turing.MultiTapeTM.ComputableInPolyTime bound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : WeakOneWayAt (OneWayNormalization.normalize f bound) α

Self-delimiting output padding preserves WeakOneWayAt against uniform strict PPT inverters.

theorem Cslib.Crypto.WeakOneWay.normalize {f : List Bool → List Bool} (hf : WeakOneWay f) (bound : ℕ → ℕ) (hbound : Turing.MultiTapeTM.ComputableInPolyTime bound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : WeakOneWay (OneWayNormalization.normalize f bound)

Self-delimiting output padding preserves WeakOneWay against uniform strict PPT inverters.

theorem Cslib.Crypto.WeakOneWay.exists_fixedOutputLength {f : List Bool → List Bool} (hf : WeakOneWay f) : ∃ (g : List Bool → List Bool) (length : ℕ → ℕ), WeakOneWay g ∧ (∀ (input : List Bool), (g input).length = length input.length) ∧ Turing.MultiTapeTM.ComputableInPolyTime length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

Every weak one-way function yields a weak one-way function whose output length depends only on the input length, with a uniformly polynomial-time unary output-length function.

Schedule reindexing for parameter-indexed one-way families

(Library variant of the padding trick in Liu and Pass, Proof of Theorem 4.1, §4, p. 10 of arXiv:2009.11514v1; cf. Goldreich, Vol. 1, §2.2.3, Proposition 2.2.3)

def Cslib.Crypto.OneWayReindex.wrappedImage (n : ℕ) (y : List Bool) : List Bool

Wrap a parameter n and a core image y into a single binary word via encPair.

@[simp]

theorem Cslib.Crypto.OneWayReindex.wrappedImage_inj {n₁ n₂ : ℕ} {y₁ y₂ : List Bool} : wrappedImage n₁ y₁ = wrappedImage n₂ y₂ ↔ n₁ = n₂ ∧ y₁ = y₂

def Cslib.Crypto.OneWayReindex.reindex (m : ℕ → ℕ) (core : ℕ → List Bool → List Bool) (x : List Bool) : List Bool

Extend a parameter-indexed family core on input lengths m n to all binary strings: find the greatest parameter n with m n ≤ x.length (GeneratorReindex.parameter), evaluate core n on the m n-bit prefix of x, and pair the result with n in unary (wrappedImage). This is a library variant of the input-truncation padding trick in Liu and Pass, Proof of Theorem 4.1, §4, p. 10 of arXiv:2009.11514v1 (cf. Goldreich, Vol. 1, §2.2.3, Proposition 2.2.3) that pairs the parameter n into the output so images from distinct parameters are disjoint.

theorem Cslib.Crypto.OneWayReindex.computableInPolyTime_reindex {m : ℕ → ℕ} {core : ℕ → List Bool → List Bool} (hm : Turing.MultiTapeTM.ComputableInPolyTime m Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hcore : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => core p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (reindex m core) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

Reindexing preserves deterministic polynomial-time computability.

noncomputable def Cslib.Crypto.OneWayReindex.familyInversionGame (m : ℕ → ℕ) (core : ℕ → List Bool → List Bool) (adversary : Inverter) (n : ℕ) : ProbComp Bool

The parameter-indexed inversion game for core at input length m n. Scores core n (candidate.take (m n)) == core n input by truncating the inverter's candidate to m n bits; since composing any inverter with List.take (m n) preserves PPT computability, bounding success in this game is no stronger a security hypothesis than the untruncated game.

theorem Cslib.Crypto.OneWayReindex.exists_familyInverter_inversion_le {m : ℕ → ℕ} {core : ℕ → List Bool → List Bool} (hm : Turing.MultiTapeTM.ComputableInPolyTime m Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hge : ∀ (n : ℕ), n + 1 ≤ m n) (hcore : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => core p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (adversary : Inverter) (hPPT : Probability.IsPPT Turing.MultiTapeTM.encBits adversary) : ∃ (familyAdv : Inverter), Probability.IsPPT Turing.MultiTapeTM.encBits familyAdv ∧ ∀ {M : ℕ}, m 0 ≤ M → Game.succProbability (inversionGame (reindex m core) adversary M).eval ≤ Game.succProbability (familyInversionGame m core familyAdv (GeneratorReindex.parameter m M)).eval

Fundamental schedule-reindexing reduction (OneWayReindex.exists_familyInverter_inversion_le). For any uniform strict PPT inverter adversary against reindex m core, there exists a uniform strict PPT inverter familyAdv against familyInversionGame m core such that for every input length M ≥ m 0, the inversion probability of adversary at length M is at most the inversion probability of familyAdv at parameter GeneratorReindex.parameter m M.

theorem Cslib.Crypto.OneWayReindex.weakOneWay {m : ℕ → ℕ} {core : ℕ → List Bool → List Bool} (hm : Turing.MultiTapeTM.ComputableInPolyTime m Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hge : ∀ (n : ℕ), n + 1 ≤ m n) (hcore : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => core p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) {q : Polynomial ℕ} (hq : ∀ (n : ℕ), 0 < Polynomial.eval n q) (hweak : ∀ (adversary : Inverter), Probability.IsPPT Turing.MultiTapeTM.encBits adversary → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Game.succProbability (familyInversionGame m core adversary n).eval) ≤ 1 - 1 / ↑(Polynomial.eval n q)) : WeakOneWay (reindex m core)

Weak one-wayness under schedule reindexing (library generalization of the padding trick in Liu and Pass, Proof of Theorem 4.1, §4, p. 10 of arXiv:2009.11514v1; cf. Goldreich, Vol. 1, §2.2.3, Proposition 2.2.3). If a parameter-indexed family core on input lengths m n (with m n ≥ n + 1) satisfies the weak one-way bound ≤ 1 - 1 / q(n) in familyInversionGame for a positive polynomial q, then reindex m core is a weak one-way function on all input lengths.

theorem Cslib.Crypto.OneWayReindex.oneWay {m : ℕ → ℕ} {core : ℕ → List Bool → List Bool} (hm : Turing.MultiTapeTM.ComputableInPolyTime m Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hge : ∀ (n : ℕ), n + 1 ≤ m n) (hcore : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => core p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hsecure : ∀ (adversary : Inverter), Probability.IsPPT Turing.MultiTapeTM.encBits adversary → Negligible fun (n : ℕ) => Game.succProbability (familyInversionGame m core adversary n).eval) : OneWay (reindex m core)

Strong one-wayness under schedule reindexing (library generalization of the padding trick in Liu and Pass, Proof of Theorem 4.1, §4, p. 10 of arXiv:2009.11514v1; cf. Goldreich, Vol. 1, §2.2.3, Proposition 2.2.3). If every uniform strict PPT inverter has negligible success probability in familyInversionGame m core, then reindex m core is a strong one-way function on all input lengths.