One-way functions separate P from NP

If one-way functions exist then P ≠ NP Goldreich, Chapter 2, Katz and Lindell, Exercise 8.11. For a function f computable in polynomial time, the preimage-prefix problem (Cslib.Crypto.preimagePrefix) asks, given n in unary, an image y and a word u, whether some input x of length n that starts with u satisfies f x = y. It is in NP, with the missing bits of x as certificate (Cslib.Crypto.preimagePrefix_mem_NP).

A decision procedure for it finds preimages bit by bit (Cslib.Crypto.preimageSearch): starting from the empty prefix, extend the prefix by false if a preimage of length n still starts with the extension, and by true otherwise. After n steps the prefix is itself a preimage of y whenever y has a preimage of length n (Cslib.Crypto.apply_preimageSearch), and the search runs in polynomial time when the decision procedure does. So if the problem is in P, a deterministic polynomial-time algorithm inverts f on every image (Cslib.Crypto.exists_inverse_of_preimagePrefix_mem_P), which a one-way function forbids (Cslib.Crypto.OneWay.preimagePrefix_notMem_P). By the Cook–Levin theorem, SAT is then not in P either (Cslib.Crypto.OneWay.SAT_notMem_P).

One-wayness is the uniform notion of Cslib.Crypto.OneWay: the inverter is uniform strict PPT and receives the unary length of the sampled input. The inverter built here is deterministic; the randomized version, for a decision procedure in BPP, is in Complexity.Crypto.Computational.OneWay.BPP.

Main definitions

• Cslib.Crypto.preimagePrefix: the preimage-prefix problem of a function.
• Cslib.Crypto.preimageSearch: the bit-by-bit search for a preimage with a decision procedure.

Main results

• Cslib.Crypto.isVerifier_preimagePrefixVerifier, Cslib.Crypto.preimagePrefix_mem_NP: the preimage-prefix problem of a polynomial-time function is in NP.
• Cslib.Crypto.apply_preimageSearch, Cslib.Crypto.preimageSearch_congr: with correct answers the search finds a preimage, and only the answers to its own n queries matter.
• Cslib.Crypto.computableTidilyInPolyTime_preimageSearch, Cslib.Crypto.computableTidilyInPolyTime_preimageSearch_of_input: the search is polynomial-time when the decision procedure is.
• Cslib.Crypto.exists_inverse_of_preimagePrefix_mem_P: if it is in P, a deterministic polynomial-time algorithm finds a preimage of every image.
• Cslib.Crypto.not_oneWay_of_lengthInverse: an efficient deterministic inverter that is told the input length refutes one-wayness (Cslib.Crypto.not_oneWay_of_inverse for inverters certified on the pair encoding).
• Cslib.Crypto.OneWay.preimagePrefix_notMem_P, Cslib.Crypto.OneWay.P_ne_NP, Cslib.Crypto.OneWay.SAT_notMem_P, Cslib.Crypto.not_oneWay_of_SAT_mem_P: one-way functions imply P ≠ NP.

References

• O. Goldreich, Foundations of Cryptography, Volume 1
• J. Katz, Y. Lindell, Introduction to Modern Cryptography

def Cslib.Crypto.preimagePrefix (f : List Bool → List Bool) : Set (ℕ × List Bool × List Bool)

The preimage-prefix problem of f: the instances (n, y, u) such that some input x of length n that starts with u satisfies f x = y.

@[reducible, inline]

abbrev Cslib.Crypto.encPreimagePrefix : ℕ × List Bool × List Bool ↪ List Bool

The encoding of instances of the preimage-prefix problem: the length n in unary, then the image and the prefix.

Membership in NP

def Cslib.Crypto.preimagePrefixVerifier (f : List Bool → List Bool) (p : (ℕ × List Bool × List Bool) × List Bool) : Bool

The verifier of the preimage-prefix problem: the certificate supplies the bits after the prefix.

theorem Cslib.Crypto.isVerifier_preimagePrefixVerifier (f : List Bool → List Bool) : Complexity.IsVerifier encPreimagePrefix Polynomial.X (preimagePrefixVerifier f) (preimagePrefix f)

The verifier accepts some certificate of the length of the encoded instance exactly for the members.

theorem Cslib.Crypto.computableTidilyInPolyTime_preimagePrefixVerifier {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (preimagePrefixVerifier f) (Turing.MultiTapeTM.encPair encPreimagePrefix Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The verifier is polynomial-time when f is.

theorem Cslib.Crypto.preimagePrefix_mem_NP {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : preimagePrefix f ∈ Complexity.NP encPreimagePrefix

The preimage-prefix problem is in NP for every function computable in polynomial time.

Search to decision

def Cslib.Crypto.preimageSearchStep (D : ℕ × List Bool × List Bool → Bool) (q : ℕ × List Bool) (u : List Bool) : List Bool

One step of the search for a preimage of length q.1 of q.2: extend the prefix u by false when D says that a preimage starts with u ++ [false], and by true otherwise.

def Cslib.Crypto.preimageSearch (D : ℕ × List Bool × List Bool → Bool) (q : ℕ × List Bool) : List Bool

The bit-by-bit search for a preimage of length q.1 of q.2, with the decision procedure D for the preimage-prefix problem: q.1 steps of preimageSearchStep.

theorem Cslib.Crypto.length_iterate_preimageSearchStep (D : ℕ × List Bool × List Bool → Bool) (q : ℕ × List Bool) (i : ℕ) : ((preimageSearchStep D q)^[i] []).length = i

The search extends the prefix by one bit at each step.

theorem Cslib.Crypto.preimageSearchStep_mem {f : List Bool → List Bool} {D : ℕ × List Bool × List Bool → Bool} (hD : ∀ (p : ℕ × List Bool × List Bool), p ∈ preimagePrefix f ↔ D p = true) {n : ℕ} {y u : List Bool} (hu : (n, y, u) ∈ preimagePrefix f) (hlen : u.length < n) : (n, y, preimageSearchStep D (n, y) u) ∈ preimagePrefix f

A correct step keeps the prefix extendable to a preimage.

theorem Cslib.Crypto.apply_preimageSearch {f : List Bool → List Bool} {D : ℕ × List Bool × List Bool → Bool} (hD : ∀ (p : ℕ × List Bool × List Bool), p ∈ preimagePrefix f ↔ D p = true) (x : List Bool) : f (preimageSearch D (x.length, f x)) = f x

Search to decision. With a decision procedure for the preimage-prefix problem, the search for a preimage of length x.length of f x finds a preimage of f x.

theorem Cslib.Crypto.iterate_preimageSearchStep_congr {D D' : ℕ × List Bool × List Bool → Bool} {q : ℕ × List Bool} (i : ℕ) : (∀ j < i, D' (q.1, q.2, (preimageSearchStep D q)^[j] [] ++ [false]) = D (q.1, q.2, (preimageSearchStep D q)^[j] [] ++ [false])) → (preimageSearchStep D' q)^[i] [] = (preimageSearchStep D q)^[i] []

The search with D' follows the search with D as long as D' answers the queries of the search with D as D does.

theorem Cslib.Crypto.preimageSearch_congr {D D' : ℕ × List Bool × List Bool → Bool} {q : ℕ × List Bool} (h : ∀ j < q.1, D' (q.1, q.2, (preimageSearchStep D q)^[j] [] ++ [false]) = D (q.1, q.2, (preimageSearchStep D q)^[j] [] ++ [false])) : preimageSearch D' q = preimageSearch D q

A decision procedure that answers the queries of the search with D as D does finds the same word. Only these q.1 queries matter, not correctness on all instances.

theorem Cslib.Crypto.computableTidilyInPolyTime_preimageSearch_of_input {γ : Type} {encIn : γ ↪ List Bool} {D : γ → ℕ × List Bool × List Bool → Bool} {q : γ → ℕ × List Bool} (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : γ × ℕ × List Bool × List Bool) => D p.1 p.2) (Turing.MultiTapeTM.encPair encIn encPreimagePrefix) Turing.MultiTapeTM.encBool) (hq : Turing.MultiTapeTM.ComputableTidilyInPolyTime q encIn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => preimageSearch (D x) (q x)) encIn Turing.MultiTapeTM.encBits

The search is polynomial-time when the decision procedure is, also for a decision procedure D x and a target q x that depend on the input x.

theorem Cslib.Crypto.computableTidilyInPolyTime_preimageSearch {D : ℕ × List Bool × List Bool → Bool} (hD : Turing.MultiTapeTM.ComputableTidilyInPolyTime D encPreimagePrefix Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (preimageSearch D) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits

The search is polynomial-time when the decision procedure is.

theorem Cslib.Crypto.exists_inverse_of_preimagePrefix_mem_P {f : List Bool → List Bool} (h : preimagePrefix f ∈ Complexity.P encPreimagePrefix) : ∃ (inverse : ℕ × List Bool → List Bool), Turing.MultiTapeTM.ComputableTidilyInPolyTime inverse (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits ∧ ∀ (x : List Bool), f (inverse (x.length, f x)) = f x

Inversion from the preimage-prefix problem. If the preimage-prefix problem of f is in P, a deterministic polynomial-time algorithm, told the length of the input, finds a preimage of every image.

One-way functions

theorem Cslib.Crypto.not_oneWay_of_lengthInverse {f : List Bool → List Bool} (inverse : ℕ × List Bool → List Bool) (hinverse : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverse (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (h : ∀ (x : List Bool), f (inverse (x.length, f x)) = f x) : ¬OneWay f

Efficient inversion refutes one-wayness. A deterministic polynomial-time algorithm that, told the length of the input, finds a preimage of every image, inverts with probability one. This is Cslib.Crypto.not_oneWay_of_inverse for an inverter certified on the pair encoding.

theorem Cslib.Crypto.OneWay.preimagePrefix_notMem_P {f : List Bool → List Bool} (hf : OneWay f) : preimagePrefix f ∉ Complexity.P encPreimagePrefix

One-way functions have hard preimage-prefix problems: the preimage-prefix problem of a one-way function is not in P.

theorem Cslib.Crypto.OneWay.P_ne_NP {f : List Bool → List Bool} (hf : OneWay f) : Complexity.P encPreimagePrefix ≠ Complexity.NP encPreimagePrefix

One-way functions imply P ≠ NP, for instances of the preimage-prefix problem.

theorem Cslib.Crypto.OneWay.SAT_notMem_P {f : List Bool → List Bool} (hf : OneWay f) : Complexity.SAT ∉ Complexity.P Complexity.encCNF

One-way functions imply SAT ∉ P: by the Cook–Levin theorem, the preimage-prefix problem reduces to SAT.

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

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