Yao's Weak-to-Strong One-Way Function Hardness Amplification

This module formalizes Yao's hardness amplification theorem ([Yao82]; Goldreich, Vol. 1, §2.3, Theorem 2.3.2; Liu and Pass, Theorem 2.3, §2.1, p. 8 of arXiv:2009.11514v1): if there exists a weak one-way function (WeakOneWay), then there exists a strong one-way function (OneWay).

Construction Overview

1. Output-length normalization: Given hf : WeakOneWay f, apply WeakOneWay.exists_fixedOutputLength to obtain a weak one-way function $g$ with a polynomial-time unary output-length schedule outLen : ℕ → ℕ (∀ x, (g x).length = outLen x.length) and a polynomial $q : \mathbb{N}[X]$ ($\forall N,\, 0 < q(N)$) such that WeakOneWayAt g (fun N => 1 / (q.eval N : ℝ)).
2. Parallel direct product on schedule $m(n)$: At parameter $n \in \mathbb{N}$, set block width $w(n) := n + 1$, block count $k(n) := 2 \cdot q(w(n)) \cdot w(n)$, and input length $m(n) := k(n) \cdot w(n)$. On an input $X \in \{0, 1\}^{m(n)}$, parallelCore k w g n X splits $X$ into $k(n)$ blocks $x_0, \dots, x_{k(n)-1} \in \{0, 1\}^{w(n)}$ via BitString.listRow and concatenates $g(x_0) \mathbin{\Vert} \dots \mathbin{\Vert} g(x_{k(n)-1})$.
3. Direct reduction and probability bound: For any uniform strict PPT inverter $\mathcal{A}$ against familyInversionGame m (parallelCore k w g) and any target polynomial degree $d \in \mathbb{N}$, running $t_d(n) := 4 \cdot q(w(n)) \cdot k(n) \cdot p_d(n)$ independent planted-slot trials (where $p_d(n) = (n + 1)^{d + 1}$) defines a uniform strict PPT inverter $B_d$ against $g$. Using BitString.uniformList_all_listRow_true twice—once across the $k(n)$ input blocks of $X$ and once across the $t_d(n)$ independent seed blocks of $B_d$—together with the exact single-slot planting law BitString.uniformList_replaceRow, the weak one-wayness bound on $g$ forces $\mathcal{A}$'s inversion probability at parameter $n$ to be at most $(1/2)^{n+1} + \frac{1}{2 p_d(n)} \le \frac{1}{p_d(n)}$ for all sufficiently large $n$.
4. Length-universal extension: Applying OneWayReindex.oneWay to the schedule $m(n)$ ($m(n) \ge n + 1$) extends parallelCore k w g to a single strong one-way function on all binary strings.

Main definitions

• Cslib.Crypto.OneWayAmplification.parallelCore: evaluate $f$ in parallel on $k(n)$ blocks of width $w(n)$ and concatenate the outputs.
• Cslib.Crypto.OneWayAmplification.plantedImage: form the $k(n)$-block parallel output with a challenge $y$ planted in slot $j$.

Main results

• Cslib.Crypto.OneWayAmplification.familyInversionGame_parallelCore_negligible: any uniform strict PPT adversary has negligible inversion probability against parallelCore on schedule $m(n) = 2 q(n+1) (n+1)^2$.
• Cslib.Crypto.WeakOneWay.exists_oneWay: every weak one-way function yields a strong one-way function (Liu and Pass, Theorem 2.3, §2.1, p. 8 of arXiv:2009.11514v1; [Yao82]).
• Cslib.Crypto.exists_oneWay_of_exists_weakOneWay: existential form of Theorem 2.3.
• Cslib.Crypto.exists_oneWay_iff_exists_weakOneWay: equivalence of weak and strong one-way functions (Goldreich, Vol. 1, §2.3, Theorem 2.3.2).

References

• Y. Liu and R. Pass, On One-Way Functions and Kolmogorov Complexity, full version arXiv:2009.11514v1 (Section 2.1, Theorem 2.3, p. 8).
• A. C. Yao, Theory and Application of Trapdoor Functions.
• O. Goldreich, Foundations of Cryptography, Volume 1, Section 2.3, Theorem 2.3.2.

Geometric amplification bounds

Parallel evaluation and planted challenges

def Cslib.Crypto.OneWayAmplification.parallelCore (k w : ℕ → ℕ) (f : List Bool → List Bool) (n : ℕ) (X : List Bool) : List Bool

Evaluate f in parallel on k n blocks of width w n extracted from X via BitString.listRow, concatenating the resulting bit strings.

theorem Cslib.Crypto.OneWayAmplification.length_parallelCore {k w outLen : ℕ → ℕ} {f : List Bool → List Bool} (hlen : ∀ (x : List Bool), (f x).length = outLen x.length) (n : ℕ) (X : List Bool) : (parallelCore k w f n X).length = k n * outLen (w n)

When f has fixed output length outLen |x| on inputs of length |x|, parallelCore produces outputs of exact length k n * outLen (w n).

theorem Cslib.Crypto.OneWayAmplification.listRow_parallelCore {k w outLen : ℕ → ℕ} {f : List Bool → List Bool} (hlen : ∀ (x : List Bool), (f x).length = outLen x.length) (n : ℕ) (X : List Bool) {j : ℕ} (hj : j < k n) : BitString.listRow (outLen (w n)) j (parallelCore k w f n X) = f (BitString.listRow (w n) j X)

Extracting the j-th output block of width outLen (w n) from parallelCore recovers f (BitString.listRow (w n) j X).

theorem Cslib.Crypto.OneWayAmplification.parallelCore_eq_imp_row_eq {k w outLen : ℕ → ℕ} {f : List Bool → List Bool} (hlen : ∀ (x : List Bool), (f x).length = outLen x.length) {n : ℕ} {X X' : List Bool} (heq : parallelCore k w f n X' = parallelCore k w f n X) {j : ℕ} (hj : j < k n) : f (BitString.listRow (w n) j X') = f (BitString.listRow (w n) j X)

Any preimage under parallelCore k w f n must invert every individual block j < k n.

theorem Cslib.Crypto.OneWayAmplification.parallelCore_take (k w : ℕ → ℕ) (f : List Bool → List Bool) (n : ℕ) (X : List Bool) : parallelCore k w f n (List.take (k n * w n) X) = parallelCore k w f n X

Truncating the input of parallelCore k w f n to k n * w n bits leaves the output unchanged.

def Cslib.Crypto.OneWayAmplification.plantedImage (k w : ℕ → ℕ) (f : List Bool → List Bool) (n j : ℕ) (y Z : List Bool) : List Bool

Construct the k n-block output of parallelCore with a challenge y planted in slot j and the remaining slots filled by f (BitString.listRow (w n) i Z).

theorem Cslib.Crypto.OneWayAmplification.length_plantedImage {k w outLen : ℕ → ℕ} {f : List Bool → List Bool} (hlen : ∀ (x : List Bool), (f x).length = outLen x.length) (n j : ℕ) {y : List Bool} (hy : y.length = outLen (w n)) (Z : List Bool) : (plantedImage k w f n j y Z).length = k n * outLen (w n)

When y has length outLen (w n), plantedImage has length k n * outLen (w n).

theorem Cslib.Crypto.OneWayAmplification.parallelCore_replaceRow {k w : ℕ → ℕ} (f : List Bool → List Bool) (n j : ℕ) {x : List Bool} (hx : x.length = w n) (Z : List Bool) : parallelCore k w f n (BitString.replaceRow (w n) (k n) j x Z) = plantedImage k w f n j (f x) Z

Evaluating parallelCore on BitString.replaceRow (w n) (k n) j x Z produces plantedImage with y = f x planted in slot j.

Candidate selection, mega-trials, and repeated trials

Polynomial-time certificates for the reduction

Quantitative probability bounds at a fixed security parameter

theorem Cslib.Crypto.OneWayAmplification.familyInversionGame_parallelCore_negligible {f : List Bool → List Bool} {outLen : ℕ → ℕ} (houtLen : Turing.MultiTapeTM.ComputableInPolyTime outLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hlen : ∀ (x : List Bool), (f x).length = outLen x.length) {q : Polynomial ℕ} (hq_pos : ∀ (N : ℕ), 0 < Polynomial.eval N q) (hweak : WeakOneWayAt f fun (N : ℕ) => 1 / ↑(Polynomial.eval N q)) (A : Inverter) (hA : Probability.IsPPT Turing.MultiTapeTM.encBits A) : Negligible fun (n : ℕ) => Game.succProbability (OneWayReindex.familyInversionGame (fun (n : ℕ) => 2 * Polynomial.eval (n + 1) q * (n + 1) * (n + 1)) (parallelCore (fun (n : ℕ) => 2 * Polynomial.eval (n + 1) q * (n + 1)) (fun (n : ℕ) => n + 1) f) A n).eval

Any uniform strict PPT adversary has negligible inversion probability against parallelCore on schedule m n = (2 * q.eval (n + 1) * (n + 1)) * (n + 1) when f has fixed output length outLen and is (1 / q(·))-weak one-way.

theorem Cslib.Crypto.WeakOneWay.exists_oneWay {f : List Bool → List Bool} (hf : WeakOneWay f) : ∃ (F : List Bool → List Bool), OneWay F

Yao's Weak-to-Strong One-Way Function Hardness Amplification (Liu and Pass, Theorem 2.3, §2.1, p. 8 of arXiv:2009.11514v1; [Yao82]; Goldreich, Vol. 1, §2.3, Theorem 2.3.2): if f is a weak one-way function (WeakOneWay f), then there exists a strong one-way function F : List Bool → List Bool (OneWay F).

theorem Cslib.Crypto.exists_oneWay_of_exists_weakOneWay (h : ∃ (f : List Bool → List Bool), WeakOneWay f) : ∃ (F : List Bool → List Bool), OneWay F

Existential Form of Yao's Hardness Amplification (Liu and Pass, Theorem 2.3, §2.1, p. 8 of arXiv:2009.11514v1): if there exists a weak one-way function, then there exists a strong one-way function.

theorem Cslib.Crypto.exists_oneWay_iff_exists_weakOneWay : (∃ (F : List Bool → List Bool), OneWay F) ↔ ∃ (f : List Bool → List Bool), WeakOneWay f

Equivalence of Weak and Strong One-Way Functions (Goldreich, Vol. 1, §2.3, Theorem 2.3.2; weak-to-strong direction Liu and Pass, Theorem 2.3, §2.1, p. 8 of arXiv:2009.11514v1 and [Yao82]; strong-to-weak direction OneWay.weakOneWay): strong one-way functions exist if and only if weak one-way functions exist.