Documentation

Complexity.Crypto.Computational.OneWay.BPP

One-way functions put NP outside BPP #

If one-way functions exist then NP ⊄ BPP Goldreich, Chapter 2: the preimage-prefix problem of a one-way function (Cslib.Crypto.preimagePrefix) is not in BPP (Cslib.Crypto.OneWay.preimagePrefix_notMem_BPP).

A decider with error at most 2 ^ (-(L + 1)) on instances of encoded length L exists for every problem in BPP (Cslib.Complexity.mem_BPP_iff_forall_decidesWithErrorExponent). The randomized search (Cslib.Crypto.randomizedPreimageSearch) samples one string of coins and runs the deterministic bit-by-bit search, answering each query with the decider on a prefix of the coins of the length the decider expects. The search with exact answers asks n fixed queries, each with encoded length at least n; whenever the decider answers these correctly, the randomized search follows the exact one (Cslib.Crypto.preimageSearch_congr) and finds a preimage. Each of them is answered wrongly with probability at most 2 ^ (-(n + 1)), so by a union bound the randomized search inverts with probability at least 1 / 2 (Cslib.Crypto.half_le_succProbability_inversionGame), and it is a uniform strict PPT inverter. Since BPP is closed under polynomial-time reductions (Cslib.Complexity.PolyTimeReducible.mem_BPP), the Cook–Levin theorem puts SAT outside BPP as well (Cslib.Crypto.OneWay.SAT_notMem_BPP).

Main definitions #

Main results #

References #

source
def Cslib.Crypto.searchCoinLength (p : Polynomial ℕ) (q : ℕ × List Bool) :
ℕ

The coins read by the randomized search for a preimage of length q.1 of q.2: enough for the decider on every query, whose prefix has at most q.1 bits.

Instances For
    source
    noncomputable def Cslib.Crypto.randomizedPreimageSearch (p : Polynomial ℕ) (V : (ℕ × List Bool × List Bool) × List Bool → Bool) (n : ℕ) (y : List Bool) :
    ProbComp (List Bool)

    The randomized search: sample searchCoinLength p (n, y) coins once, and run the bit-by-bit search, answering every query with V on the prefix of the coins of the length p (L) that V expects on an instance of encoded length L.

    Instances For
      source
      theorem Cslib.Crypto.isPPT_randomizedPreimageSearch {p : Polynomial ℕ} {V : (ℕ × List Bool × List Bool) × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableTidilyInPolyTime V (Turing.MultiTapeTM.encPair encPreimagePrefix Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) :
      Probability.IsPPT Turing.MultiTapeTM.encBits (randomizedPreimageSearch p V)

      The randomized search is a uniform strict PPT inverter when V is polynomial-time.

      source
      theorem Cslib.Crypto.half_le_succProbability_inversionGame {f : List Bool → List Bool} {p : Polynomial ℕ} {V : (ℕ × List Bool × List Bool) × List Bool → Bool} (hV : Complexity.DecidesWithErrorExponent encPreimagePrefix (Polynomial.X + 1) p V (preimagePrefix f)) (n : ℕ) :
      1 / 2 ≤ Game.succProbability (inversionGame f (randomizedPreimageSearch p V) n).eval

      The randomized search inverts with probability at least 1 / 2, for a decider of the preimage-prefix problem with error at most 2 ^ (-(L + 1)) on instances of encoded length L. The union bound runs over the n queries of the exact search, each of encoded length at least n.

      source
      theorem Cslib.Crypto.exists_inverter_of_preimagePrefix_mem_BPP {f : List Bool → List Bool} (h : preimagePrefix f ∈ Complexity.BPP encPreimagePrefix) :
      ∃ (inverter : Inverter), Probability.IsPPT Turing.MultiTapeTM.encBits inverter ∧ ∀ (n : ℕ), 1 / 2 ≤ Game.succProbability (inversionGame f inverter n).eval

      Inversion from BPP. If the preimage-prefix problem of f is in BPP, a uniform strict PPT inverter, told the length of the input, inverts f with probability at least 1 / 2 at every length.

      source
      theorem Cslib.Crypto.OneWay.preimagePrefix_notMem_BPP {f : List Bool → List Bool} (hf : OneWay f) :
      preimagePrefix f ∉ Complexity.BPP encPreimagePrefix

      One-way functions have preimage-prefix problems outside BPP.

      source
      theorem Cslib.Crypto.OneWay.not_NP_subset_BPP {f : List Bool → List Bool} (hf : OneWay f) :
      ¬Complexity.NP encPreimagePrefix ⊆ Complexity.BPP encPreimagePrefix

      One-way functions imply NP ⊄ BPP, for instances of the preimage-prefix problem.

      source
      theorem Cslib.Crypto.OneWay.SAT_notMem_BPP {f : List Bool → List Bool} (hf : OneWay f) :
      Complexity.SAT ∉ Complexity.BPP Complexity.encCNF

      One-way functions imply SAT ∉ BPP: by the Cook–Levin theorem the preimage-prefix problem reduces to SAT, and BPP is closed under polynomial-time reductions.

      source
      theorem Cslib.Crypto.not_oneWay_of_SAT_mem_BPP {f : List Bool → List Bool} (h : Complexity.SAT ∈ Complexity.BPP Complexity.encCNF) :
      ¬OneWay f

      If SAT is in BPP, no function is one-way.