Padding expanding generators to a common input length

Run an expander on the required seed prefix, retain the unused input bits, and truncate the result to one bit more than the common input length. Independent uniform padding preserves the distinguishing advantage exactly through an efficient reduction.

This is used to give the entropy guesses in the OWF-to-PRG construction a common seed length before amplification and XOR combination.

Main definitions

• generate: pad a raw expanding function to one bit of stretch at a common input length.
• test: reduce a padded-output test to a test of the raw output.

Main results

• isPolyTime_generate, isPPTOn_test: certify the construction and its security reduction.
• length_generate: exactly one bit of stretch for correctly sized inputs.
• advantage_eq: the reduction preserves distinguishing advantage exactly.

References

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.GeneratorPadding.generate (seedBits commonBits : ℕ) (generator : List Bool → List Bool) (seed : List Bool) : List Bool

Retain the unused uniform input bits and keep exactly one bit of stretch.

theorem Cslib.Crypto.GeneratorPadding.isPolyTime_generate {α : Type} {input : α ↪ List Bool} {seedBits commonBits : α → ℕ} {generator : α → List Bool → List Bool} {seed : α → List Bool} (hseedBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (hcommon : Turing.MultiTapeTM.ComputableTidilyInPolyTime commonBits input Turing.MultiTapeTM.encUnary) (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α × List Bool) => generator a.1 a.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seed input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => generate (seedBits a) (commonBits a) (generator a) (seed a)) input Turing.MultiTapeTM.encBits

Padding uses only the supplied generator, word slicing, and concatenation.

theorem Cslib.Crypto.GeneratorPadding.length_generate {seedBits commonBits : ℕ} {generator : List Bool → List Bool} (hfits : seedBits ≤ commonBits) (hexpands : ∀ (seed : List Bool), seed.length = seedBits → seedBits < (generator seed).length) {seed : List Bool} (hseed : seed.length = commonBits) : (generate seedBits commonBits generator seed).length = commonBits + 1

One bit of raw expansion suffices, also when no padding is needed.

theorem Cslib.Crypto.GeneratorPadding.generate_distribution {seedBits commonBits : ℕ} (generator : List Bool → List Bool) (hfits : seedBits ≤ commonBits) : PMF.map (generate seedBits commonBits generator) (BitString.uniformList commonBits) = do let word ← PMF.map generator (BitString.uniformList seedBits) PMF.map (fun (padding : List Bool) => List.take (commonBits + 1) (word ++ padding)) (BitString.uniformList (commonBits - seedBits))

The unused suffix of a uniform padded seed is fresh independent randomness.

theorem Cslib.Crypto.GeneratorPadding.ideal_distribution {seedBits outputBits commonBits : ℕ} (hexpands : seedBits < outputBits) : (do let word ← BitString.uniformList outputBits PMF.map (fun (padding : List Bool) => List.take (commonBits + 1) (word ++ padding)) (BitString.uniformList (commonBits - seedBits))) = BitString.uniformList (commonBits + 1)

Uniform raw output and independent padding give exactly the desired uniform output.

noncomputable def Cslib.Crypto.GeneratorPadding.test (seedBits commonBits : ℕ) (adversary : List Bool → ProbComp Bool) (word : List Bool) : ProbComp Bool

A distinguisher for padded output is an ordinary randomized postprocessing of raw output.

theorem Cslib.Crypto.GeneratorPadding.isPPTOn_test {α : Type} {input : α ↪ List Bool} {seedBits commonBits : α → ℕ} {adversary : α → List Bool → ProbComp Bool} {word : α → List Bool} (hseedBits : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (hcommon : Turing.MultiTapeTM.ComputableTidilyInPolyTime commonBits input Turing.MultiTapeTM.encUnary) (hadversary : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (a : α × List Bool) => adversary a.1 a.2) (hword : Turing.MultiTapeTM.ComputableTidilyInPolyTime word input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => test (seedBits a) (commonBits a) (adversary a) (word a)

The reduction charges the padding and the call to the captured adversary.

theorem Cslib.Crypto.GeneratorPadding.advantage_eq {seedBits outputBits commonBits : ℕ} (generator : List Bool → List Bool) (adversary : List Bool → ProbComp Bool) (hfits : seedBits ≤ commonBits) (hexpands : seedBits < outputBits) : Game.advantage ((PMF.map (generate seedBits commonBits generator) (BitString.uniformList commonBits)).bind fun (word : List Bool) => (adversary word).eval) ((BitString.uniformList (commonBits + 1)).bind fun (word : List Bool) => (adversary word).eval) = Game.advantage ((PMF.map generator (BitString.uniformList seedBits)).bind fun (word : List Bool) => (test seedBits commonBits adversary word).eval) ((BitString.uniformList outputBits).bind fun (word : List Bool) => (test seedBits commonBits adversary word).eval)

Padding preserves the tested distinguishing advantage exactly.