The GGM construction against circuits

The construction of Goldreich, Goldwasser and Micali [GGM86] turns a length-doubling generator G with seeds of k bits into a keyed family of functions: the key labels the root of a binary tree of depth n, the two children of a node labelled s are labelled by the two blocks of k bits of G s (Cslib.BitString.block), and the value at an input x of n bits is the label of the leaf reached by following x (evalBits). This is the list-based Cslib.Crypto.GGM.eval for words of fixed width (ofFn_evalBits). Keeping the first bit of the label gives a keyed family of Boolean functions (booleanFamily), the family used by Razborov and Rudich [RazborovRudich1997, Section 4].

This module proves the nonuniform security of that family with concrete losses. Circuit sizes count every AND, OR, NOT and constant gate of the De Morgan basis, and the tests are deterministic circuits on the whole truth table (Cslib.Crypto.PRG.IsCircuitTest), which query the function at every input. Write C for the circuit complexity of G as a function with 2 k outputs.

• Size of the members. Every function of the family is computed with n (C + 4 k) + 2 gates (complexity_booleanFamily_le).
• Security. If no test with t + 2 ^ n (n C + 1) gates distinguishes G from uniform with advantage more than ε, then no test with t gates distinguishes the truth table of a random member of the family from a uniformly random truth table with advantage more than (2 ^ n - 1) ε (secure_truthTableGenerator_booleanFamily). The proof is the hybrid argument over the levels of the tree. The hybrid at depth j labels the 2 ^ j nodes at depth j uniformly at random; between depths j and j + 1, the 2 ^ j expansions are replaced by uniform strings one at a time (Cslib.Crypto.PRG.abs_expect_comp_sub_expect_le). Fixing all of them but one turns a test of truth tables into a test of that expansion, which computes the subtree below it; every bit of the truth table is then a constant or a bit of an evaluation along at most n levels.
• Asymptotics. A family of generators of polynomial circuit complexity that, for all long seeds, resists circuits of size 2 ^ m with advantage 2 ^ (-m) on seeds of length k ≥ m ^ d (Cslib.Crypto.PRG.IsSubexponentiallySecure) gives, with keys of length (n + 1) ^ (2 d + 1), an exponentially secure family (isExponentiallySecure_booleanFamily). The natural proofs barrier from such generators is Cslib.Circuits.Boolean.not_isUseful_PPoly_of_isNatural_of_generator.

The adaptive hybrids of Cslib.Crypto.GGM.hybridGame concern uniform oracle adversaries and are not used here: a circuit reading the whole truth table queries every leaf, so the hybrids are over complete levels of the tree.

Main definitions

• Cslib.Crypto.GGM.evalBits: evaluation of the GGM tree with labels of fixed width.
• Cslib.Crypto.GGM.booleanFamily: the GGM family of Boolean functions.

Main results

• Cslib.Crypto.GGM.ofFn_evalBits: agreement with the list construction Cslib.Crypto.GGM.eval.
• Cslib.Crypto.GGM.complexity_booleanFamily_le: the members have circuits of size n (C + 4 k) + 2.
• Cslib.Crypto.GGM.secure_truthTableGenerator_booleanFamily: security against circuits, with explicit loss in size and advantage.
• Cslib.Crypto.GGM.isExponentiallySecure_booleanFamily: subexponentially secure generators give exponentially secure families.

References

• O. Goldreich, S. Goldwasser, S. Micali, How to construct random functions
• A. A. Razborov, S. Rudich, Natural proofs

Evaluation with labels of fixed width

def Cslib.Crypto.GGM.evalBits {k : ℕ} (G : PRG.Generator (BitString k) (BitString (2 * k))) {n : ℕ} : BitString k → BitString n → BitString k

Evaluate the GGM tree with labels of width k [GGM86]: starting from the seed, replace the label by the half of its expansion selected by each query bit in turn, from the first bit of the query to the last. The halves are the two blocks of k bits (Cslib.BitString.block), the first for false and the second for true.

@[simp]

theorem Cslib.Crypto.GGM.evalBits_zero {k : ℕ} (G : PRG.Generator (BitString k) (BitString (2 * k))) (seed : BitString k) (x : BitString 0) : evalBits G seed x = seed

theorem Cslib.Crypto.GGM.evalBits_succ {k n : ℕ} (G : PRG.Generator (BitString k) (BitString (2 * k))) (seed : BitString k) (x : BitString (n + 1)) : evalBits G seed x = evalBits G ((G seed).block (finTwoEquiv.symm (x 0))) (Fin.tail x)

def Cslib.Crypto.GGM.listGenerator {k : ℕ} (G : PRG.Generator (BitString k) (BitString (2 * k))) : List Bool → List Bool

A generator of fixed-width strings as a generator of lists: it reads the first k bits of its input, taking missing bits to be false.

theorem Cslib.Crypto.GGM.ofFn_evalBits {k n : ℕ} (G : PRG.Generator (BitString k) (BitString (2 * k))) (seed : BitString k) (x : BitString n) : List.ofFn (evalBits G seed x) = eval (listGenerator G) (List.ofFn seed) (List.ofFn x)

Agreement with the list construction. Evaluation with labels of fixed width is Cslib.Crypto.GGM.eval for the generator read as a generator of lists.

def Cslib.Crypto.GGM.booleanFamily {k : ℕ} [NeZero k] (G : PRG.Generator (BitString k) (BitString (2 * k))) (n : ℕ) (seed : BitString k) : BooleanFunction n

The GGM family of Boolean functions [RR97]: the function with key seed maps an input of n bits to the first bit of the label it reaches in the GGM tree.

Circuits for tree evaluation

theorem Cslib.Crypto.GGM.complexity_evalBits_le {k n : ℕ} (G : PRG.Generator (BitString k) (BitString (2 * k))) (x : BitString n) : (Circuits.complexity Circuits.Boolean.interpretation fun (seed : Fin k → Bool) => evalBits G seed x) ≤ n * Circuits.complexity Circuits.Boolean.interpretation ⇑G

Evaluation along a fixed query of length n costs at most n copies of a circuit for the generator: as a function of the seed, each step is the generator followed by a wiring.

theorem Cslib.Crypto.GGM.complexity_evalBits_block_le {k n : ℕ} (G : PRG.Generator (BitString k) (BitString (2 * k))) (b : Fin 2) (x : BitString n) (i : Fin k) : Circuits.complexity Circuits.Boolean.interpretation (Circuits.single fun (y : Fin (2 * k) → Bool) => evalBits G (BitString.block y b) x i) ≤ n * Circuits.complexity Circuits.Boolean.interpretation ⇑G

One bit of the evaluation along a fixed query of length n, as a function of a string of length 2 k whose selected block is the seed, costs at most n copies of a circuit for the generator.

theorem Cslib.Crypto.GGM.synthesis_evalBits {k n N : ℕ} (G : PRG.Generator (BitString k) (BitString (2 * k))) {s : Set (BooleanFunction N)} (seed : BitString N → BitString k) (query : BitString N → BitString n) (hseed : ∀ (i : Fin k), (fun (z : BitString N) => seed z i) ∈ s) (hquery : ∀ (i : Fin n), (fun (z : BitString N) => query z i) ∈ s) : Circuits.Synthesis Circuits.Boolean.interpretation s (Set.range fun (i : Fin k) (z : Fin N → Bool) => evalBits G (seed z) (query z) i) (n * (Circuits.complexity Circuits.Boolean.interpretation ⇑G + 4 * k))

Circuits for tree evaluation. If the bits of a seed and of a query of length n are available, the bits of the label reached are synthesized with, per query bit, a smallest circuit for the generator and k multiplexers of four gates.

theorem Cslib.Crypto.GGM.complexity_booleanFamily_le {k : ℕ} [NeZero k] (G : PRG.Generator (BitString k) (BitString (2 * k))) (n : ℕ) (seed : BitString k) : Circuits.complexity Circuits.Boolean.interpretation (Circuits.single (booleanFamily G n seed)) ≤ n * (Circuits.complexity Circuits.Boolean.interpretation ⇑G + 4 * k) + 2

The members of the GGM family have small circuits: two constants for the key, then per input bit a smallest circuit for the generator and k multiplexers of four gates.

Uniform labels

The GGM hybrids

Security of the GGM family against circuits

theorem Cslib.Crypto.GGM.secure_truthTableGenerator_booleanFamily {k n : ℕ} [NeZero k] {G : PRG.Generator (BitString k) (BitString (2 * k))} {t : ℕ} {ε : NNReal} (hG : G.Secure (PRG.IsCircuitTest (t + 2 ^ n * (n * Circuits.complexity Circuits.Boolean.interpretation ⇑G + 1))) ε) : (PRG.truthTableGenerator (booleanFamily G n)).Secure (PRG.IsCircuitTest t) ((2 ^ n - 1) * ε)

The GGM family is pseudorandom against circuits [GGM86], [RR97]. Let G be a length-doubling generator with labels of width k ≥ 1 whose circuit complexity is C. If no test computed with t + 2 ^ n (n C + 1) gates distinguishes the output of G from uniform with advantage more than ε, then no test computed with t gates distinguishes the truth table of the GGM function on n inputs with a uniformly random key from a uniformly random truth table with advantage more than (2 ^ n - 1) ε.

The proof is the hybrid argument over the levels of the tree, where the hybrid at depth j labels the nodes at depth j uniformly at random. Between depths j and j + 1 the 2 ^ j expansions are replaced by uniform strings one at a time; fixing the others, a test of truth tables computes the subtree below the remaining one with at most 2 ^ n (n C + 1) more gates.

Asymptotic security

theorem Cslib.Crypto.GGM.isExponentiallySecure_booleanFamily {G : (k : ℕ) → PRG.Generator (BitString k) (BitString (2 * k))} {d : ℕ} (hsize : PolynomiallyBounded fun (k : ℕ) => Circuits.complexity Circuits.Boolean.interpretation ⇑(G k)) (hG : PRG.IsSubexponentiallySecure G d) : PRG.IsExponentiallySecure fun (n : ℕ) => booleanFamily (G ((n + 1) ^ (2 * d + 1))) n

The GGM family from a subexponentially secure generator is exponentially secure [GGM86], [RazborovRudich1997, Section 4]. Let G be a family of length-doubling generators of polynomial circuit complexity, subexponentially secure with exponent 1 / d. With keys of length (n + 1) ^ (2 d + 1), the GGM functions on n inputs are pseudorandom against circuits of size 2 ^ (c n) with error 2 ^ (-c n) for every c and all large n: the generator on these keys resists circuits of size 2 ^ (n ^ 2).