Normalizing the output length of a one-way function

Self-delimiting padding using an output-size bound makes the output length depend only on the input length. Equality of padded images implies equality of the original images, even for a candidate of a different length. A uniform strict PPT reduction therefore preserves one-wayness. This supplies the fixed-output-width interface used by the pseudoentropy construction without assuming that the original function is length-preserving, injective or regular.

Main definitions

• Cslib.Crypto.OneWayNormalization.normalize: pad each image using an input-length bound.

Main results

• Cslib.Crypto.OneWay.normalize: output normalization preserves one-wayness.
• Cslib.Crypto.OneWay.exists_fixedOutputLength: every OWF yields an OWF with a uniformly polynomial-time output-length function.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Definition 1 and Section 4.

Adapted from Crypto/Computational/OneWay/Normalize.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. This is the word-encoding reduction to the write-up's fixed-output-width setting, using the shared tidy machine calculus and nonnegative game API.

def Cslib.Crypto.OneWayNormalization.normalize (f : List Bool → List Bool) (bound : ℕ → ℕ) (input : List Bool) : List Bool

Normalize a word function using a bound supplied in unary.

theorem Cslib.Crypto.OneWayNormalization.computableTidilyInPolyTime_normalize {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) {bound : ℕ → ℕ} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (normalize f bound) Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

Output normalization preserves deterministic polynomial time.

theorem Cslib.Crypto.OneWayNormalization.inversion_le (f : List Bool → List Bool) (bound : ℕ → ℕ) (adversary : Inverter) (n : ℕ) : Game.succProbability (inversionGame (normalize f bound) adversary n).eval ≤ Game.succProbability (inversionGame f (fun (n : ℕ) (image : List Bool) => adversary n (BitString.padWord (bound n) image)) n).eval

Any inverter for the normalized function gives an inverter for the original function. Only its challenge is padded; the candidate is returned unchanged, at any length.

theorem Cslib.Crypto.OneWay.normalize {f : List Bool → List Bool} (hf : OneWay f) (bound : ℕ → ℕ) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : OneWay (OneWayNormalization.normalize f bound)

Self-delimiting output padding preserves one-wayness against uniform strict PPT inverters.

theorem Cslib.Crypto.OneWay.exists_fixedOutputLength {f : List Bool → List Bool} (hf : OneWay f) : ∃ (g : List Bool → List Bool) (length : ℕ → ℕ), OneWay g ∧ (∀ (input : List Bool), (g input).length = length input.length) ∧ Turing.MultiTapeTM.ComputableTidilyInPolyTime length Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

Every OWF yields an OWF whose output length depends only on the input length. Both evaluation and this unary output-length function are uniformly polynomial time.