Documentation

Complexity.Crypto.Computational.PseudorandomFunction.TruthTable

Truth tables of word oracles #

A distinguisher can read the truth table of a word oracle on few inputs: on the 2 ^ m words of length n whose first n - m bits are false (tableQueries), the first bits of the replies form the truth table of a Boolean function on m inputs, the restriction of the oracle (restriction, map_tableQueries). Asking for it is strict oracle PPT (isOraclePPTOn_queryTable).

The restriction of a pseudorandom family is simple: a keyed family computable in polynomial time has polynomial-size circuits, uniformly in the key, so its restrictions do too (exists_complexity_restriction_le). The restriction of a random function is a uniformly random Boolean function (uniformOfFintype_map_restrictTable). These are the two halves of the natural-property distinguisher of Kabanets and Cai [KC00], in the spirit of Razborov and Rudich [RR97], assembled in Complexity.Crypto.Computational.OneWay.MCSP; all declarations here live in the namespace Cslib.Crypto.KabanetsCai.

The truth table lists the values in the order of Cslib.BitString.equivFin, which is the order of the enumeration Cslib.BitString.enumList (Cslib.BitString.enumList_eq_ofFn).

Main definitions #

Main results #

References #

Asking an oracle for a truth table #

source
def Cslib.Crypto.KabanetsCai.queryTableStep (s : List (List Bool) × List Bool) :
Probability.WordOracleComp Unit (List (List Bool) × List Bool)

One step of queryTable: ask the first remaining word, and record the first bit of its reply.

Instances For
    source
    def Cslib.Crypto.KabanetsCai.queryTable (words : List (List Bool)) :
    Probability.WordOracleComp Unit (List Bool)

    Ask the oracle every word of the list, in order, and return the first bits of the replies, false for an empty reply.

    Instances For
      source
      theorem Cslib.Crypto.KabanetsCai.isOraclePPTOn_queryTable :
      Probability.IsOraclePPTOn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits queryTable

      Asking for a table is strict oracle PPT: each step copies one word onto the query buffer and reads one reply bit.

      source
      theorem Cslib.Crypto.KabanetsCai.interpret_queryTable {m : Type → Type u_1} [Monad m] [LawfulMonad m] (random : (n : ℕ) → m (Fin (n + 1))) (oracle : List Bool → List Bool) (words : List (List Bool)) :
      OracleComp.interpret (ProbOracleComp.handler random fun (request : Unit × List Bool) => pure (oracle request.2)) (queryTable words) = pure (List.map (fun (word : List Bool) => (oracle word).headD false) words)

      Against a deterministic oracle, queryTable returns the first bits of the replies.

      Restrictions of word functions #

      source
      def Cslib.Crypto.KabanetsCai.restriction (oracle : List Bool → List Bool) (n m : ℕ) :
      BooleanFunction m

      The Boolean function on m inputs read from a word function on the words of length n whose first n - m bits are false: the first bit of the value, false when it is empty.

      Instances For
        source
        def Cslib.Crypto.KabanetsCai.tableQueries (n m : ℕ) :
        List (List Bool)

        The queries at arity m: the 2 ^ m words of length n with n - m leading false bits, in the order of Cslib.BitString.enumList.

        Instances For
          source
          theorem Cslib.Crypto.KabanetsCai.map_tableQueries (oracle : List Bool → List Bool) (n m : ℕ) :
          List.map (fun (word : List Bool) => (oracle word).headD false) (tableQueries n m) = List.ofFn ((MCSP.truthTable m) (restriction oracle n m))

          The first bits of the answers of a word function to the queries, in order, form the truth table of its restriction.

          source
          theorem Cslib.Crypto.KabanetsCai.exists_complexity_restriction_le {family : List Bool → List Bool → List Bool} (hfamily : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) :
          ∃ (c : ℕ), ∀ (key : List Bool), ∀ m ≤ key.length, Circuits.complexity Circuits.Boolean.interpretation (Circuits.single (restriction (family key) key.length m)) ≤ c * (3 * key.length + 2) ^ c + 2

          Restrictions of a polynomial-time keyed family have polynomial circuits. For one constant c, every key of length n and every m ≤ n, the restriction of the family with that key has a circuit with at most c (3 n + 2) ^ c + 2 gates: a circuit for the first output bit on inputs of length 3 n + 1, with the key and the leading false bits substituted.

          source
          def Cslib.Crypto.KabanetsCai.restrictTable (n m : ℕ) (hn : 0 < n) :
          (BitString n → BitString n) →+ BooleanFunction m

          Reading the first bit of a table at the words of length n with n - m leading false bits is additive in the table.

          Instances For
            source
            theorem Cslib.Crypto.KabanetsCai.restriction_randomFunctionOracle {n m : ℕ} (hn : 0 < n) (hm : m ≤ n) (table : BitString n → BitString n) :
            restriction (randomFunctionOracle n table) n m = (restrictTable n m hn) table

            The restriction of a random-function oracle is the restriction of its table.

            source
            theorem Cslib.Crypto.KabanetsCai.restriction_prfOracle {family : List Bool → List Bool → List Bool} {n m : ℕ} (hm : m ≤ n) (key : List Bool) :
            restriction (prfOracle family n key) n m = restriction (family key) n m

            The restriction of a keyed oracle to valid queries is the restriction of the family.

            source
            theorem Cslib.Crypto.KabanetsCai.uniformOfFintype_map_restrictTable {n m : ℕ} (hn : 0 < n) (hm : m ≤ n) :
            PMF.map (⇑(restrictTable n m hn)) (Probability.PMF.uniformOfFintype (BitString n → BitString n)) = Probability.PMF.uniformOfFintype (BooleanFunction m)

            A random function restricts to a uniformly random function.