Documentation

Complexity.Crypto.Computational.PRGToOneWay

One-way functions from pseudorandom generators #

An inverter for a generator G gives a test: on a word y, run the inverter and accept when it returns a preimage of y (PRGToOneWay.test). On a generated word this test succeeds exactly as often as the inverter wins the inversion game. On a uniform word of length ℓ n it can only accept words in the image of G restricted to the seeds whose image has length ℓ n, so it accepts with probability at most the number of those seeds divided by 2 ^ ℓ n (PRGToOneWay.succProbability_uniformList_test_le). When this fraction is negligible the generator is therefore one-way (PseudorandomGenerator.oneWay_of_card_le).

When ℓ n ≥ 2 n, every such seed has length at most ℓ n - n, which gives the fraction 2 ^ (1 - n), so every length-doubling generator is one-way (PseudorandomGenerator.oneWay). The same holds when ℓ is injective and 2 ^ (n - ℓ n) is negligible (PseudorandomGenerator.oneWay_of_injective). A generator of arbitrary stretch is first truncated to one bit of stretch and then amplified to stretch n ↦ 2 n + 1, so every pseudorandom generator yields a one-way function (PseudorandomGenerator.exists_oneWay). With the converse OneWay.exists_pseudorandomGenerator this shows that one-way functions exist if and only if pseudorandom generators exist [HILL99] (exists_oneWay_iff_exists_pseudorandomGenerator).

Main definitions #

Main results #

References #

source
def Cslib.Crypto.PRGToOneWay.test (generator : List Bool → List Bool) (adversary : Inverter) :
Distinguisher

The test built from an inverter: on a word y, run the inverter and accept when it returns a preimage of y under the generator.

Instances For
    source
    theorem Cslib.Crypto.PRGToOneWay.isPPT_test {generator : List Bool → List Bool} {adversary : Inverter} (hgenerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime generator Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hadversary : Probability.IsPPT Turing.MultiTapeTM.encBits adversary) :
    Probability.IsPPT Turing.MultiTapeTM.encBool (test generator adversary)

    The test is PPT when the generator is polynomial time and the inverter is PPT.

    source
    theorem Cslib.Crypto.PRGToOneWay.inversionGame_eq_prgRealGame (generator : List Bool → List Bool) (adversary : Inverter) (n : ℕ) :
    inversionGame generator adversary n = prgRealGame generator (test generator adversary) n

    On generated words the test is exactly the inversion game.

    source
    theorem Cslib.Crypto.PRGToOneWay.succProbability_uniformList_test_le {generator : List Bool → List Bool} {ℓ : ℕ → ℕ} (hlen : ∀ (word : List Bool), (generator word).length = ℓ word.length) (adversary : Inverter) (n : ℕ) (P : Finset (List Bool)) (hP : ∀ (x : List Bool), ℓ x.length = ℓ n → x ∈ P) (ε : NNReal) (hε : ↑P.card ≤ ε * 2 ^ ℓ n) :
    (distinguishingGame (BitString.uniformList (ℓ n)) (test generator adversary n)).succProbability ≤ ε

    The ideal game. If every word whose image has length ℓ n lies in a finite set P with |P| ≤ ε 2 ^ ℓ n, the test accepts a uniform word of length ℓ n with probability at most ε: it can only accept words of G '' P.

    source
    theorem Cslib.Crypto.PseudorandomGenerator.oneWay_of_card_le {generator : List Bool → List Bool} {ℓ : ℕ → ℕ} (hgenerator : PseudorandomGenerator generator ℓ) {ε : ℕ → NNReal} (hε : Negligible ε) (P : ℕ → Finset (List Bool)) (hP : ∀ (n : ℕ) (x : List Bool), ℓ x.length = ℓ n → x ∈ P n) (hcard : ∀ (n : ℕ), ↑(P n).card ≤ ε n * 2 ^ ℓ n) :
    OneWay generator

    A pseudorandom generator is one-way when, for a negligible ε, the words whose image has length ℓ n lie in a set of at most ε n 2 ^ ℓ n words: an inverter succeeding on generated words would give a test accepting generated words much more often than uniform ones.

    source
    theorem Cslib.Crypto.PseudorandomGenerator.oneWay {generator : List Bool → List Bool} {ℓ : ℕ → ℕ} (hgenerator : PseudorandomGenerator generator ℓ) (hℓ : ∀ (n : ℕ), 2 * n ≤ ℓ n) :
    OneWay generator

    Length-doubling pseudorandom generators are one-way. If 2 n ≤ ℓ n for all n, a pseudorandom generator with output length ℓ is a one-way function: the seeds whose image has length ℓ n have length at most ℓ n - n, so a uniform word of length ℓ n is in the image with probability at most 2 ^ (1 - n).

    source
    theorem Cslib.Crypto.PseudorandomGenerator.oneWay_of_injective {generator : List Bool → List Bool} {ℓ : ℕ → ℕ} (hgenerator : PseudorandomGenerator generator ℓ) (hinj : Function.Injective ℓ) (hgap : Negligible fun (n : ℕ) => (1 / 2) ^ (ℓ n - n)) :
    OneWay generator

    A pseudorandom generator whose output length ℓ is injective and whose gap 2 ^ (n - ℓ n) is negligible is one-way: the seeds whose image has length ℓ n are then exactly those of length n. This covers stretches such as ℓ n = n + (Nat.log 2 n + 1) ^ 2, which is strictly increasing and eventually below 2 n.

    source
    theorem Cslib.Crypto.PseudorandomGenerator.exists_oneWay {generator : List Bool → List Bool} {ℓ : ℕ → ℕ} (hgenerator : PseudorandomGenerator generator ℓ) :
    ∃ (f : List Bool → List Bool), OneWay f

    Every pseudorandom generator yields a one-way function. Truncate the generator to one bit of stretch, amplify it to stretch n ↦ 2 n + 1, and apply PseudorandomGenerator.oneWay.

    source
    theorem Cslib.Crypto.exists_oneWay_iff_exists_pseudorandomGenerator :
    (∃ (f : List Bool → List Bool), OneWay f) ↔ ∃ (generator : List Bool → List Bool) (ℓ : ℕ → ℕ), PseudorandomGenerator generator ℓ

    One-way functions exist if and only if pseudorandom generators exist [HILL99]. The forward direction is OneWay.exists_pseudorandomGenerator, the converse PseudorandomGenerator.exists_oneWay.