XOR combination of independently seeded generators

Split a uniform tape into equal seed blocks, evaluate every indexed generator, and XOR their outputs. A reduction simulates all but one candidate. Replacing that candidate's output by uniform bits makes the combined output uniform, with no assumption on the other candidates.

Main definitions

• generate: evaluate an indexed family on independent seed blocks and XOR its outputs.
• test: the randomized reduction that inserts one supplied candidate output.

Main results

• isPolyTime_generate, isPPTOn_test: uniform certificates with captured programs.
• real_distribution, ideal_distribution: exact laws of the complete combined output.
• advantage_eq, indistinguishable: one secure indexed candidate secures the combination.

References

This is the combination step in Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, final proof of Theorem 1, [Hol06].

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Cslib.Crypto.GeneratorXor.generate (count seedBits outputBits : ℕ) (generator : ℕ → List Bool → List Bool) (seed : List Bool) : List Bool

Evaluate every candidate on its own seed block and XOR the outputs at the declared width.

@[simp]

theorem Cslib.Crypto.GeneratorXor.length_generate (count seedBits outputBits : ℕ) (generator : ℕ → List Bool → List Bool) (seed : List Bool) : (generate count seedBits outputBits generator seed).length = outputBits

The output width is fixed, including on short or malformed input tapes.

theorem Cslib.Crypto.GeneratorXor.isPolyTime_generate {α : Type} {input : α ↪ List Bool} {count seedBits outputBits : α → ℕ} {generator : α → ℕ → List Bool → List Bool} {seed : α → List Bool} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hseedBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (houtputBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime outputBits input Turing.MultiTapeTM.encUnary) (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : (α × ℕ) × List Bool) => generator pair.1.1 pair.1.2 pair.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seed input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => generate (count a) (seedBits a) (outputBits a) (generator a) (seed a)) input Turing.MultiTapeTM.encBits

Combining polynomially many uniformly efficient candidates uses ordinary collection code.

theorem Cslib.Crypto.GeneratorXor.generate_eq_sum (count seedBits outputBits : ℕ) (generator : ℕ → List Bool → List Bool) (seed : List Bool) : generate count seedBits outputBits generator seed = List.ofFn (∑ i : Fin count, BitString.ofList outputBits (generator (↑i) (List.ofFn ((BitString.ofList (count * seedBits) seed).block i))))

The executable combiner is the finite sum of its candidates' bitstring outputs.

theorem Cslib.Crypto.GeneratorXor.generate_distribution (count seedBits outputBits : ℕ) (generator : ℕ → List Bool → List Bool) : PMF.map (generate count seedBits outputBits generator) (BitString.uniformList (count * seedBits)) = PMF.map (fun (seeds : Fin count → BitString seedBits) => List.ofFn (∑ i : Fin count, BitString.ofList outputBits (generator (↑i) (List.ofFn (seeds i))))) (Probability.PMF.uniformOfFintype (Fin count → BitString seedBits))

Uniform seed blocks are independent; the combiner's law is a sum over their finite tuple.

theorem Cslib.Crypto.GeneratorXor.real_distribution (count seedBits outputBits : ℕ) (generator : ℕ → List Bool → List Bool) (i : Fin count) : (do let challenge ← PMF.map (generator ↑i) (BitString.uniformList seedBits) PMF.map (generate count seedBits outputBits fun (j : ℕ) (seed : List Bool) => if j = ↑i then challenge else generator j seed) (BitString.uniformList (count * seedBits))) = PMF.map (generate count seedBits outputBits generator) (BitString.uniformList (count * seedBits))

A real challenge can replace the chosen candidate's output because its seed is independent of every other seed block. The simulator may sample and discard the unused chosen block.

theorem Cslib.Crypto.GeneratorXor.ideal_distribution (count seedBits outputBits : ℕ) (generator : ℕ → List Bool → List Bool) (i : Fin count) : (do let challenge ← BitString.uniformList outputBits PMF.map (generate count seedBits outputBits fun (j : ℕ) (seed : List Bool) => if j = ↑i then challenge else generator j seed) (BitString.uniformList (count * seedBits))) = BitString.uniformList outputBits

One uniform candidate masks the complete XOR, for every fixed choice of the other outputs.

noncomputable def Cslib.Crypto.GeneratorXor.test (count seedBits outputBits : ℕ) (generator : ℕ → List Bool → List Bool) (index : ℕ) (adversary : List Bool → ProbComp Bool) (challenge : List Bool) : ProbComp Bool

Simulate every other candidate and insert the supplied challenge at the chosen index.

theorem Cslib.Crypto.GeneratorXor.isPPTOn_test {α : Type} {input : α ↪ List Bool} {count seedBits outputBits index : α → ℕ} {generator : α → ℕ → List Bool → List Bool} {adversary : α → List Bool → ProbComp Bool} {challenge : α → List Bool} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hseedBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (houtputBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime outputBits input Turing.MultiTapeTM.encUnary) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index input Turing.MultiTapeTM.encUnary) (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : (α × ℕ) × List Bool) => generator pair.1.1 pair.1.2 pair.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hadversary : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (pair : α × List Bool) => adversary pair.1 pair.2) (hchallenge : Turing.MultiTapeTM.ComputableTidilyInPolyTime challenge input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => test (count a) (seedBits a) (outputBits a) (generator a) (index a) (adversary a) (challenge a)

The reduction is a uniform program that captures its index and its distinguisher.

theorem Cslib.Crypto.GeneratorXor.advantage_eq (count seedBits outputBits : ℕ) (generator : ℕ → List Bool → List Bool) (i : Fin count) (adversary : List Bool → ProbComp Bool) : Game.advantage ((PMF.map (generate count seedBits outputBits generator) (BitString.uniformList (count * seedBits))).bind fun (word : List Bool) => (adversary word).eval) ((BitString.uniformList outputBits).bind fun (word : List Bool) => (adversary word).eval) = Game.advantage ((PMF.map (generator ↑i) (BitString.uniformList seedBits)).bind fun (word : List Bool) => (test count seedBits outputBits generator (↑i) adversary word).eval) ((BitString.uniformList outputBits).bind fun (word : List Bool) => (test count seedBits outputBits generator (↑i) adversary word).eval)

XOR combination loses no distinguishing advantage when reducing to a valid candidate.

theorem Cslib.Crypto.GeneratorXor.indistinguishable {generator : ℕ → ℕ → List Bool → List Bool} {count seedBits outputBits choose : ℕ → ℕ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseedBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (houtputBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime outputBits Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : (ℕ × ℕ) × List Bool) => generator input.1.1 input.1.2 input.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hchoose : ∀ᶠ (n : ℕ) in Filter.atTop, choose n < count n) (hsecure : ∀ (adversary : ℕ → ℕ → List Bool → ProbComp Bool), (Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (input : (ℕ × ℕ) × List Bool) => adversary input.1.1 input.1.2 input.2) → Negligible fun (n : ℕ) => Game.advantage ((PMF.map (generator n (choose n)) (BitString.uniformList (seedBits n))).bind fun (word : List Bool) => (adversary n (choose n) word).eval) ((BitString.uniformList (outputBits n)).bind fun (word : List Bool) => (adversary n (choose n) word).eval)) : ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map (generate (count n) (seedBits n) (outputBits n) (generator n)) (BitString.uniformList (count n * seedBits n))) fun (n : ℕ) => BitString.uniformList (outputBits n)

One secure choice in a uniformly efficient family makes the XOR computationally uniform. The combiner evaluates the whole family; only the reduction receives the proof's chosen index.