Pseudorandomness against circuits

Concrete security of generators (Cslib.Crypto.PRG.Generator.Secure) is relative to a class of admissible tests. This module supplies the nonuniform class: the deterministic tests computed by De Morgan circuits with at most t gates (IsCircuitTest), where every AND, OR, NOT and constant gate counts. It states the security notions used by the natural proofs barrier [RazborovRudich1997, Section 4]:

• a keyed family of Boolean functions is pseudorandom against circuits when the generator mapping a key to the truth table of its function is (truthTableGenerator). The tests read the whole truth table, that is they query the function at every input. The family is exponentially secure when it resists circuits of size 2 ^ (c n) with error 2 ^ (-c n) for every c (IsExponentiallySecure);
• a family of length-doubling generators is subexponentially secure when, for all long seeds of length k, it resists circuits of size 2 ^ m with error 2 ^ (-m) for m ^ d ≤ k (IsSubexponentiallySecure). Security against circuits of size 2 ^ (k ^ ε) with error 2 ^ (-k ^ ε) gives it for d ε ≥ 1 (IsSubexponentiallySecure.of_rpow).

It also proves the hybrid argument for independent samples in the form of averages (abs_expect_comp_sub_expect_le): replacing |ι| independent outputs of a function by uniform values, one coordinate at a time, costs at most |ι| times the cost of one replacement with all other coordinates fixed.

Main definitions

• Cslib.Crypto.PRG.IsCircuitTest: the tests computed by circuits with at most t gates.
• Cslib.Crypto.PRG.truthTableGenerator: a keyed family of Boolean functions, as a generator of truth tables.
• Cslib.Crypto.PRG.IsExponentiallySecure: keyed families pseudorandom against circuits of size 2 ^ (c n) with error 2 ^ (-c n), for every c.
• Cslib.Crypto.PRG.IsSubexponentiallySecure: length-doubling generators resisting circuits of size 2 ^ (k ^ (1 / d)).

Main results

• Cslib.Crypto.PRG.IsSubexponentiallySecure.of_rpow: security against circuits of size 2 ^ (k ^ ε) gives subexponential security.
• Cslib.Crypto.PRG.abs_expect_comp_sub_expect_le: the hybrid argument for independent samples.

References

• A. A. Razborov, S. Rudich, Natural proofs

Tests computed by circuits

def Cslib.Crypto.PRG.IsCircuitTest {m : ℕ} (t : ℕ) (adversary : Adversary (BitString m)) : Prop

The tests on m-bit strings computed by De Morgan circuits with at most t gates: the deterministic tests whose circuit complexity is at most t. As the admissible adversaries of Cslib.Crypto.PRG.Generator.Secure, they express security against circuits of size t.

def Cslib.Crypto.PRG.truthTableGenerator {Key : Type u_1} {n : ℕ} (F : Key → BooleanFunction n) : Generator Key (BitString (2 ^ n))

The generator mapping a key to the truth table of the function F key. Its security against IsCircuitTest t is the pseudorandomness of the keyed family F against circuits with at most t gates that read the whole truth table, that is that query the function at every input.

@[simp]

theorem Cslib.Crypto.PRG.truthTableGenerator_apply {Key : Type u_1} {n : ℕ} (F : Key → BooleanFunction n) (key : Key) : (truthTableGenerator F) key = (MCSP.truthTable n) (F key)

def Cslib.Crypto.PRG.IsExponentiallySecure {Key : ℕ → Type u_1} [(n : ℕ) → Fintype (Key n)] [∀ (n : ℕ), Nonempty (Key n)] (F : (n : ℕ) → Key n → BooleanFunction n) : Prop

A keyed family F of Boolean functions is exponentially secure against circuits when, for every c, eventually no test computed with at most 2 ^ (c n) gates distinguishes the truth table of F n key, for a uniformly random key, from a uniformly random truth table with advantage more than 2 ^ (-c n). This is the hypothesis of the natural proofs barrier [RazborovRudich1997, Section 4]. The tests read the whole truth table, that is they query the function at every input.

def Cslib.Crypto.PRG.IsSubexponentiallySecure (G : (k : ℕ) → Generator (BitString k) (BitString (2 * k))) (d : ℕ) : Prop

A family of length-doubling generators is subexponentially secure against circuits, with exponent 1 / d, when for all sufficiently long seeds, of length k, no test computed with at most 2 ^ m gates has advantage more than 2 ^ (-m) against G k, for every m with m ^ d ≤ k. Up to rounding, G k resists circuits of size 2 ^ (k ^ ε) with advantage 2 ^ (-k ^ ε) for ε = 1 / d, the hypothesis of [RazborovRudich1997, Section 4].

theorem Cslib.Crypto.PRG.IsSubexponentiallySecure.of_rpow {G : (k : ℕ) → Generator (BitString k) (BitString (2 * k))} {ε : ℝ} {d : ℕ} (hd : 1 ≤ ↑d * ε) (hG : ∀ᶠ (k : ℕ) in Filter.atTop, (G k).Secure (IsCircuitTest ⌊2 ^ ↑k ^ ε⌋₊) (2 ^ ↑k ^ ε)⁻¹) : IsSubexponentiallySecure G d

A generator family that, for all long seeds, resists circuits of size 2 ^ (k ^ ε) with advantage 2 ^ (-k ^ ε), for some ε > 0, is subexponentially secure with exponent 1 / d for every d ≥ 1 / ε.

The hybrid argument for independent samples

theorem Cslib.Crypto.PRG.abs_expect_comp_sub_expect_le {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] (g : α → β) (T : (ι → β) → ℝ) {ε : ℝ} (hT : ∀ (c : ι → β) (i : ι), |(Finset.univ.expect fun (a : α) => T (Function.update c i (g a))) - Finset.univ.expect fun (b : β) => T (Function.update c i b)| ≤ ε) : |(Finset.univ.expect fun (s : ι → α) => T fun (i : ι) => g (s i)) - Finset.univ.expect fun (y : ι → β) => T y| ≤ ↑(Fintype.card ι) * ε

The hybrid argument for independent samples. Let T be a statistic of ι-indexed tuples in β. If, with all other coordinates fixed, replacing g a for a uniform a by a uniform b at one coordinate changes the average of T by at most ε, then replacing every coordinate changes it by at most |ι| ε. For T the acceptance probability of a test, this is the security of independent copies of a generator g with loss |ι|.