One-way functions and permutations

A polynomial-time function on binary words is one-way when, given its value on a uniform n-bit input and the unary parameter n, every uniform PPT inverter has negligible probability of finding any preimage. Recovering the sampled input is not required, and the inverter's answer is not restricted to the sampled input's length.

OneWayPermutation additionally requires a length-preserving bijection. Its inverse exists as a mathematical function; no efficiency of that inverse is assumed. Such a permutation preserves the uniform distribution at every input length. These are definitions, not assertions that one-way functions or permutations exist.

Main definitions

• Cslib.Crypto.inversionGame: sample a challenge and test the inverter's candidate preimage.
• Cslib.Crypto.OneWay, Cslib.Crypto.OneWayPermutation: uniform computational assumptions.

Main results

• Cslib.Crypto.OneWay.inversion_negligible: negligible success for each efficient inverter.
• Cslib.Crypto.OneWayPermutation.uniformList_append_bit: the ideal one-bit extension is uniform.
• Cslib.Crypto.not_oneWay_of_le_succProbability: inverting with probability bounded away from zero at every length refutes one-wayness.
• Cslib.Crypto.not_oneWay_of_inverse, not_oneWay_const: efficient preimages refute one-wayness.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 9.2.

Adapted from Crypto/Computational/OneWay.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using finite fair-bit programs, tidy deterministic certificates and the upstream nonnegative game API.

@[reducible, inline]

abbrev Cslib.Crypto.Inverter : Type

An inverter receives the unary parameter and the image of the sampled input.

noncomputable def Cslib.Crypto.inversionGame (f : List Bool → List Bool) (adversary : Inverter) (n : ℕ) : ProbComp Bool

The inversion experiment accepts any preimage of its challenge.

theorem Cslib.Crypto.isPPTOn_inversionGame {f : List Bool → List Bool} {adversary : Inverter} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (ha : Probability.IsPPT Turing.MultiTapeTM.encBits adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (inversionGame f adversary)

Run the complete inversion experiment on its unary parameter.

theorem Cslib.Crypto.isPPT_inversionGame {f : List Bool → List Bool} {adversary : Inverter} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (ha : Probability.IsPPT Turing.MultiTapeTM.encBits adversary) : Probability.IsPPT Turing.MultiTapeTM.encBool fun (n : ℕ) (x : List Bool) => inversionGame f adversary n

The inversion experiment is uniformly PPT, independently of the unused auxiliary input.

structure Cslib.Crypto.OneWay (f : List Bool → List Bool) : Prop

One plain polynomial-time algorithm evaluates the function. Every uniform strict PPT inverter has negligible success over the uniform input and its own independent random coins.

• polyTime : Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

  A deterministic polynomial-time algorithm evaluates the function.

• secure : Game.Indistinguishable (fun (adversary : Inverter) (n : ℕ) => (inversionGame f adversary n).eval) (fun (x : Inverter) (x_1 : ℕ) => PMF.pure false) (Probability.IsPPT Turing.MultiTapeTM.encBits)

  Inversion is indistinguishable from certain failure in the common game calculus.

theorem Cslib.Crypto.oneWay_iff_tidy {f : List Bool → List Bool} : OneWay f ↔ Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits ∧ Game.Indistinguishable (fun (adversary : Inverter) (n : ℕ) => (inversionGame f adversary n).eval) (fun (x : Inverter) (x_1 : ℕ) => PMF.pure false) (Probability.IsPPT Turing.MultiTapeTM.encBits)

Recover the tidy presentation for proofs without changing the security contract.

theorem Cslib.Crypto.OneWay.inversion_negligible {f : List Bool → List Bool} (h : OneWay f) (adversary : Inverter) (hPPT : Probability.IsPPT Turing.MultiTapeTM.encBits adversary) : Negligible fun (n : ℕ) => Game.succProbability (inversionGame f adversary n).eval

The shared game definition gives the usual negligible inversion probability.

theorem Cslib.Crypto.OneWay.of_inversion_negligible {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (h : ∀ (adversary : Inverter), Probability.IsPPT Turing.MultiTapeTM.encBits adversary → Negligible fun (n : ℕ) => Game.succProbability (inversionGame f adversary n).eval) : OneWay f

Establish one-wayness by bounding every efficient inverter's success probability.

structure Cslib.Crypto.OneWayPermutation (f : List Bool → List Bool) : Prop

A length-preserving permutation that is one-way against every uniform PPT inverter.

• oneWay : OneWay f

  Evaluation is polynomial time, and inversion has negligible success.

• length_eq (word : List Bool) : (f word).length = word.length

  The permutation acts separately on words of each length.

• bijective : Function.Bijective f

  Every word has exactly one preimage; finding it need not be efficient.

theorem Cslib.Crypto.OneWayPermutation.uniformList_map {f : List Bool → List Bool} (hf : OneWayPermutation f) (n : ℕ) : PMF.map f (BitString.uniformList n) = BitString.uniformList n

A one-way permutation preserves the uniform distribution at each input length.

theorem Cslib.Crypto.OneWayPermutation.uniformList_append_bit {f : List Bool → List Bool} (hf : OneWayPermutation f) (n : ℕ) : ((BitString.uniformList n).bind fun (word : List Bool) => PMF.map (fun (bit : Bool) => f word ++ [bit]) (Probability.PMF.uniformOfFintype Bool)) = BitString.uniformList (n + 1)

A permuted uniform seed followed by an independent fair bit is exactly uniform at the expanded length. Security is needed when replacing the independent bit by a hard-core predicate.

theorem Cslib.Crypto.inversionGame_eq_of_injective (f : List Bool → List Bool) (hf : Function.Injective f) (adversary : Inverter) (n : ℕ) : inversionGame f adversary n = do let input ← BitString.sampleList n let candidate ← adversary n (f input) pure (candidate == input)

For an injective function, accepting any preimage is equivalent to recovering the sampled input. The general inversion experiment does not make this assumption.

theorem Cslib.Crypto.eval_inversionGame_of_rightInverse (f : List Bool → List Bool) (inverse : ℕ → List Bool → List Bool) (h : ∀ (x : List Bool), f (inverse x.length (f x)) = f x) (n : ℕ) : (inversionGame f (fun (n : ℕ) (y : List Bool) => pure (inverse n y)) n).eval = PMF.pure true

An inverter that, told the input length, always returns a preimage makes the experiment always succeed.

theorem Cslib.Crypto.not_oneWay_of_le_succProbability {f : List Bool → List Bool} {c : NNReal} (hc : c ≠ 0) (inverter : Inverter) (hPPT : Probability.IsPPT Turing.MultiTapeTM.encBits inverter) (h : ∀ (n : ℕ), c ≤ Game.succProbability (inversionGame f inverter n).eval) : ¬OneWay f

Inverting with probability bounded away from zero refutes one-wayness: an efficient inverter whose success probability is at least a fixed c > 0 at every length.

theorem Cslib.Crypto.not_oneWay_of_inverse (f : List Bool → List Bool) (inverse : ℕ → List Bool → List Bool) (hPPT : Probability.IsPPT Turing.MultiTapeTM.encBits fun (n : ℕ) (y : List Bool) => pure (inverse n y)) (hinv : ∀ (x : List Bool), f (inverse x.length (f x)) = f x) : ¬OneWay f

Efficiently finding any preimage, told the input length, contradicts one-wayness.

theorem Cslib.Crypto.not_oneWay_const (word : List Bool) : ¬OneWay fun (x : List Bool) => word

Constant functions are not one-way: the empty word is always a preimage.