MCSP in BPP rules out one-way functions

If the Minimum Circuit Size Problem is decidable in probabilistic polynomial time, then one-way functions do not exist Kabanets and Cai. One-way functions give pseudorandom functions (Cslib.Crypto.OneWay.exists_pseudorandomFunction), and an MCSP decider distinguishes a pseudorandom function from a random one:

• The restriction of a keyed family computable in polynomial time to the 2 ^ m inputs of length n whose first n - m bits are false, read through the first output bit (Cslib.Crypto.KabanetsCai.restriction), has a circuit with at most c (3 n + 2) ^ c + 2 gates for a constant c (Cslib.Crypto.KabanetsCai.exists_complexity_restriction_le).
• A random function restricts to a uniformly random truth table (Cslib.Crypto.KabanetsCai.uniformOfFintype_map_restrictTable), and at most 2 ^ (2 ^ m / 4) of the 2 ^ (2 ^ m) truth tables have circuits with at most ⌊2 ^ m / (5 m)⌋ gates (Cslib.MCSP.ncard_setOf_mem_le, Cslib.Crypto.KabanetsCai.toReal_map_restrictTable_mem_le).

The distinguisher (Cslib.Crypto.KabanetsCai.mcspDistinguisher) takes m = d ⌈log₂ n⌉ for d = c + 2, queries the oracle on the 2 ^ m ≤ (2 n) ^ d words above, assembles the first bits of the replies into a truth table, and runs the bounded-error MCSP decider at threshold ⌊2 ^ m / (5 m)⌋. For large n this threshold is at least the circuit size of every restriction of the family, so the decider accepts the pseudorandom table with probability at least 2 / 3, and a random table with probability at most 1 / 3 + 2 ^ (2 ^ m / 4) / 2 ^ (2 ^ m). The distinguisher is a uniform strict oracle PPT adversary in the model of Cslib.Crypto.PseudorandomFunction (Cslib.Crypto.KabanetsCai.isOraclePPT_mcspDistinguisher), and its advantage is at least 1 / 4 for all large n, which is not negligible.

MCSP is the language Cslib.MCSP of instances (T, s) whose truth table T of 2 ^ m bits has a De Morgan circuit with at most s gates (all gates counted), encoded by the table followed by s in binary (Cslib.MCSP.encInstance); BPP is Cslib.Complexity.BPP for this encoding. The hypothesis is that MCSP is in BPP at all thresholds; the distinguisher only runs the decider at thresholds ⌊2 ^ m / (5 m)⌋. The parts of the distinguisher live in the namespace Cslib.Crypto.KabanetsCai.

Main definitions

• Cslib.Crypto.KabanetsCai.mcspRun: run a bounded-error decider for MCSP on fresh coins.
• Cslib.Crypto.KabanetsCai.mcspDistinguisher: the oracle adversary built from an MCSP decider.

Main results

• Cslib.Crypto.KabanetsCai.toReal_map_restrictTable_mem_le: few restrictions of a random function have small circuits.
• Cslib.Crypto.KabanetsCai.isOraclePPT_mcspDistinguisher: the distinguisher is uniform strict oracle PPT.
• Cslib.Crypto.KabanetsCai.eval_prfRealGame_mcspDistinguisher, Cslib.Crypto.KabanetsCai.eval_prfIdealGame_mcspDistinguisher: in both games the decider runs on the truth table of a restriction.
• Cslib.Crypto.not_pseudorandomFunction_of_MCSP_mem_BPP: if MCSP is in BPP, there are no pseudorandom functions.
• Cslib.Crypto.not_oneWay_of_MCSP_mem_BPP, Cslib.Crypto.not_oneWay_of_MCSP_mem_P: Kabanets–Cai: if MCSP is in BPP, or in P, there are no one-way functions.

References

• V. Kabanets, J.-Y. Cai, Circuit minimization problem
• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions

Few random restrictions have small circuits

theorem Cslib.Crypto.KabanetsCai.toReal_map_restrictTable_mem_le {n m : ℕ} (hn : 0 < n) (hm : m ≤ n) (hm16 : 16 ≤ m) : ((PMF.map (fun (table : BitString n → BitString n) => decide ({ arity := m, table := (MCSP.truthTable m) ((restrictTable n m hn) table), threshold := 2 ^ m / (5 * m) } ∈ MCSP)) (Probability.PMF.uniformOfFintype (BitString n → BitString n))) true).toReal ≤ 2 ^ (2 ^ m / 4) / 2 ^ 2 ^ m

Few restrictions of a random function have small circuits. For 16 ≤ m ≤ n, the restriction of a uniformly random function from n bits to n bits to m inputs has a circuit with at most ⌊2 ^ m / (5 m)⌋ gates with probability at most 2 ^ (2 ^ m / 4) / 2 ^ (2 ^ m).

Running a bounded-error decider for MCSP

noncomputable def Cslib.Crypto.KabanetsCai.mcspRun (p : Polynomial ℕ) (V : MCSP.Instance × List Bool → Bool) (x : MCSP.Instance) : ProbComp Bool

Run a decider with random coins for MCSP on one instance, with fresh uniform coins of the length the bounded-error condition prescribes.

theorem Cslib.Crypto.KabanetsCai.isPPTOn_mcspRun {p : Polynomial ℕ} {V : MCSP.Instance × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableTidilyInPolyTime V (Turing.MultiTapeTM.encPair MCSP.encInstance Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Probability.IsPPTOn MCSP.encInstance Turing.MultiTapeTM.encBool (mcspRun p V)

theorem Cslib.Crypto.KabanetsCai.toReal_eval_mcspRun (p : Polynomial ℕ) (V : MCSP.Instance × List Bool → Bool) (x : MCSP.Instance) : ((mcspRun p V x).eval true).toReal = ↑{r : Fin (Polynomial.eval (MCSP.encInstance x).length p) → Bool | V (x, List.ofFn r) = true}.card / 2 ^ Polynomial.eval (MCSP.encInstance x).length p

The acceptance probability of mcspRun is the fraction of accepting coin strings.

theorem Cslib.Crypto.KabanetsCai.two_thirds_le_toReal_eval_mcspRun {p : Polynomial ℕ} {V : MCSP.Instance × List Bool → Bool} (hV : Complexity.DecidesWithBoundedError MCSP.encInstance p V MCSP) {x : MCSP.Instance} (hx : x ∈ MCSP) : 2 / 3 ≤ ((mcspRun p V x).eval true).toReal

A bounded-error decider accepts a member of MCSP with probability at least 2 / 3.

theorem Cslib.Crypto.KabanetsCai.toReal_eval_mcspRun_le_one_third {p : Polynomial ℕ} {V : MCSP.Instance × List Bool → Bool} (hV : Complexity.DecidesWithBoundedError MCSP.encInstance p V MCSP) {x : MCSP.Instance} (hx : x ∉ MCSP) : ((mcspRun p V x).eval true).toReal ≤ 1 / 3

A bounded-error decider accepts a non-member of MCSP with probability at most 1 / 3.

The distinguisher

def Cslib.Crypto.KabanetsCai.tableArity (d n : ℕ) : ℕ

The number of inputs of the truth tables read at parameter n: d ⌈log₂ n⌉.

def Cslib.Crypto.KabanetsCai.tableInstance (m : ℕ) (answers : List Bool) : MCSP.Instance

The MCSP instance read from a list of answers at arity m, with threshold 2 ^ m / (5 m).

noncomputable def Cslib.Crypto.KabanetsCai.mcspDistinguisher (p : Polynomial ℕ) (V : MCSP.Instance × List Bool → Bool) (d : ℕ) : OracleDistinguisher

The Kabanets–Cai distinguisher. At parameter n, ask the oracle for the truth table of its restriction to m = d ⌈log₂ n⌉ inputs and run the bounded-error decider V for MCSP at threshold 2 ^ m / (5 m).

theorem Cslib.Crypto.KabanetsCai.tableInstance_map_tableQueries (oracle : List Bool → List Bool) (n m : ℕ) : tableInstance m (List.map (fun (word : List Bool) => (oracle word).headD false) (tableQueries n m)) = { arity := m, table := (MCSP.truthTable m) (restriction oracle n m), threshold := 2 ^ m / (5 * m) }

The answers of a deterministic oracle to the queries form the truth table of its restriction.

theorem Cslib.Crypto.KabanetsCai.interpret_mcspDistinguisher {p : Polynomial ℕ} {V : MCSP.Instance × List Bool → Bool} (d : ℕ) (oracle : List Bool → List Bool) (n : ℕ) : OracleComp.interpret (ProbOracleComp.handler ProbComp.unifFin fun (request : Unit × List Bool) => pure (oracle request.2)) (mcspDistinguisher p V d n []) = mcspRun p V { arity := tableArity d n, table := (MCSP.truthTable (tableArity d n)) (restriction oracle n (tableArity d n)), threshold := 2 ^ tableArity d n / (5 * tableArity d n) }

Against a deterministic oracle, the distinguisher runs the decider on the truth table of the oracle's restriction.

The distinguisher is uniform strict oracle PPT

theorem Cslib.Crypto.KabanetsCai.computableTidilyInPolyTime_tableArity (d : ℕ) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (tableArity d) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The arity is computed in unary from the unary parameter.

theorem Cslib.Crypto.KabanetsCai.computableTidilyInPolyTime_two_pow_tableArity (d : ℕ) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (n : ℕ) => 2 ^ tableArity d n) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The table size 2 ^ m is computed in unary from the unary parameter.

theorem Cslib.Crypto.KabanetsCai.computableTidilyInPolyTime_tableQueries (d : ℕ) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : ℕ × List Bool) => tableQueries input.1 (tableArity d input.1)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

The queries are computed in polynomial time from the unary parameter.

theorem Cslib.Crypto.KabanetsCai.computableTidilyInPolyTime_tableInstance (d : ℕ) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : (ℕ × List Bool) × List Bool) => tableInstance (tableArity d pair.1.1) pair.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) MCSP.encInstance

The instance read from the answers is computed in polynomial time.

theorem Cslib.Crypto.KabanetsCai.isOraclePPT_mcspDistinguisher {p : Polynomial ℕ} {V : MCSP.Instance × List Bool → Bool} (d : ℕ) (hV : Turing.MultiTapeTM.ComputableTidilyInPolyTime V (Turing.MultiTapeTM.encPair MCSP.encInstance Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : Probability.IsOraclePPT Turing.MultiTapeTM.encBool (mcspDistinguisher p V d)

The Kabanets–Cai distinguisher is uniform strict oracle PPT, for a polynomial-time decider V: it makes 2 ^ m ≤ (2 (n + 1)) ^ d queries of length n and runs V on a truth table of 2 ^ m bits.

The advantage of the distinguisher

theorem Cslib.Crypto.KabanetsCai.eval_prfRealGame_mcspDistinguisher {p : Polynomial ℕ} {V : MCSP.Instance × List Bool → Bool} (family : List Bool → List Bool → List Bool) {d n : ℕ} (hm : tableArity d n ≤ n) : (prfRealGame family (mcspDistinguisher p V d) n).eval = (BitString.uniformList n).bind fun (key : List Bool) => (mcspRun p V { arity := tableArity d n, table := (MCSP.truthTable (tableArity d n)) (restriction (family key) n (tableArity d n)), threshold := 2 ^ tableArity d n / (5 * tableArity d n) }).eval

In the real game, the decider runs on the truth table of the restriction of the family with a uniform key.

theorem Cslib.Crypto.KabanetsCai.eval_prfIdealGame_mcspDistinguisher {p : Polynomial ℕ} {V : MCSP.Instance × List Bool → Bool} {d n : ℕ} (hn : 0 < n) (hm : tableArity d n ≤ n) : (prfIdealGame (mcspDistinguisher p V d) n).eval = (Probability.PMF.uniformOfFintype (BitString n → BitString n)).bind fun (table : BitString n → BitString n) => (mcspRun p V { arity := tableArity d n, table := (MCSP.truthTable (tableArity d n)) ((restrictTable n (tableArity d n) hn) table), threshold := 2 ^ tableArity d n / (5 * tableArity d n) }).eval

In the ideal game, the decider runs on the truth table of the restriction of a uniformly random function.

theorem Cslib.Crypto.KabanetsCai.eventually_tableArity (c : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < n ∧ 16 ≤ tableArity (c + 2) n ∧ tableArity (c + 2) n ≤ n ∧ c * (3 * n + 2) ^ c + 2 ≤ 2 ^ tableArity (c + 2) n / (5 * tableArity (c + 2) n)

For large n, the arity m = d ⌈log₂ n⌉ with d = c + 2 satisfies 16 ≤ m ≤ n, and the threshold 2 ^ m / (5 m) is at least c (3 n + 2) ^ c + 2.

theorem Cslib.Crypto.not_pseudorandomFunction_of_MCSP_mem_BPP (h : MCSP ∈ Complexity.BPP MCSP.encInstance) (family : List Bool → List Bool → List Bool) : ¬PseudorandomFunction family

MCSP in BPP rules out pseudorandom functions. If a bounded-error polynomial-time decider for MCSP exists, then every keyed family computable in polynomial time is distinguished from a random function by a uniform strict oracle PPT adversary (mcspDistinguisher) with advantage at least 1 / 4 for all large n.

theorem Cslib.Crypto.not_oneWay_of_MCSP_mem_BPP (h : MCSP ∈ Complexity.BPP MCSP.encInstance) (f : List Bool → List Bool) : ¬OneWay f

Kabanets–Cai Kabanets and Cai: if MCSP is in BPP, with instances encoded by their truth table and threshold, then no function is one-way.

theorem Cslib.Crypto.not_oneWay_of_MCSP_mem_P (h : MCSP ∈ Complexity.P MCSP.encInstance) (f : List Bool → List Bool) : ¬OneWay f

Kabanets–Cai for deterministic deciders: if MCSP is in P, no function is one-way.