Uniform computational indistinguishability

An ensemble supplies a distribution at each security parameter. A distinguisher is one strict PPT program, given the unary parameter and a sample; its clock is polynomial in their combined length. Ensembles need not themselves be efficiently sampleable or have polynomial sample lengths. The distinguishing experiment is therefore a probability law, not an unrestricted sampling primitive in the program language.

The negligible bound may depend on the adversary: one complete algorithm is fixed before asserting decay. Semantic tests are admissible exactly when one such program realizes all their distributions. Both presentations use the shared Game.Indistinguishable definition.

Main definitions

• Cslib.Crypto.IsPPTTest: uniform realization of a family of randomized tests.
• Cslib.Crypto.distinguishingGame: give an ensemble sample to a program.
• Cslib.Crypto.ComputationallyIndistinguishable: security against every uniform strict PPT test.

Main results

• Cslib.Crypto.computationallyIndistinguishable_iff_tests: equivalent semantic-test presentation.
• Cslib.Crypto.ComputationallyIndistinguishable.bind: efficient randomized postprocessing.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 9.
• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 3.2.

Adapted from Crypto/Computational/Basic.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, with arbitrary ensemble laws kept outside the program syntax and the current upstream nonnegative game API.

@[reducible, inline]

abbrev Cslib.Crypto.Distinguisher : Type

A distinguisher receives the unary security parameter and a sampled word.

def Cslib.Crypto.IsPPTTest (test : ℕ → List Bool → PMF Bool) : Prop

One uniform strict PPT algorithm realizes the whole family of randomized tests.

@[simp]

theorem Cslib.Crypto.isPPTTest_eval {adversary : Distinguisher} : (IsPPTTest fun (n : ℕ) (input : List Bool) => (adversary n input).eval) ↔ Probability.IsPPT Turing.MultiTapeTM.encBool adversary

Interpreting a program preserves exactly its uniform PPT restriction.

noncomputable def Cslib.Crypto.distinguishingGame (distribution : PMF (List Bool)) (adversary : List Bool → ProbComp Bool) : Game

Give a sample from a distribution to a distinguisher; this law assumes no efficient sampler.

theorem Cslib.Crypto.eval_bind_eq_distinguishingGame (sample : ProbComp (List Bool)) (adversary : List Bool → ProbComp Bool) : (sample >>= adversary).eval = distinguishingGame sample.eval adversary

An actual sampler followed by a distinguisher realizes the corresponding experiment.

theorem Cslib.Crypto.distinguishingGame_map (distribution : PMF (List Bool)) (adversary : List Bool → ProbComp Bool) (f : Bool → Bool) : (distinguishingGame distribution fun (word : List Bool) => f <$> adversary word) = PMF.map f (distinguishingGame distribution adversary)

Postprocessing the distinguisher's answer postprocesses the experiment's answer.

def Cslib.Crypto.ComputationallyIndistinguishable (X Y : ℕ → PMF (List Bool)) : Prop

Each uniform strict PPT distinguisher has negligible advantage between the two ensembles. Neither ensemble is required to be efficiently sampleable or polynomially bounded in length.

theorem Cslib.Crypto.computationallyIndistinguishable_iff_tests {X Y : ℕ → PMF (List Bool)} : ComputationallyIndistinguishable X Y ↔ Game.Indistinguishable (fun (test : ℕ → List Bool → PMF Bool) (n : ℕ) => (X n).bind (test n)) (fun (test : ℕ → List Bool → PMF Bool) (n : ℕ) => (Y n).bind (test n)) IsPPTTest

Program distinguishers and uniformly realizable semantic tests give the same notion.

theorem Cslib.Crypto.ComputationallyIndistinguishable.refl (X : ℕ → PMF (List Bool)) : ComputationallyIndistinguishable X X

An ensemble is computationally indistinguishable from itself.

theorem Cslib.Crypto.ComputationallyIndistinguishable.symm {X Y : ℕ → PMF (List Bool)} (h : ComputationallyIndistinguishable X Y) : ComputationallyIndistinguishable Y X

Swapping the ensembles preserves computational indistinguishability.

theorem Cslib.Crypto.ComputationallyIndistinguishable.trans {X Y Z : ℕ → PMF (List Bool)} (hXY : ComputationallyIndistinguishable X Y) (hYZ : ComputationallyIndistinguishable Y Z) : ComputationallyIndistinguishable X Z

A two-hop hybrid argument uses the same uniform distinguisher in both hops.

theorem Cslib.Crypto.ComputationallyIndistinguishable.bind {X Y : ℕ → PMF (List Bool)} (h : ComputationallyIndistinguishable X Y) {process : ℕ → List Bool → ProbComp (List Bool)} (hprocess : Probability.IsPPT Turing.MultiTapeTM.encBits process) : ComputationallyIndistinguishable (fun (n : ℕ) => (X n).bind fun (word : List Bool) => (process n word).eval) fun (n : ℕ) => (Y n).bind fun (word : List Bool) => (process n word).eval

Efficient randomized postprocessing preserves computational indistinguishability.

theorem Cslib.Crypto.ComputationallyIndistinguishable.map {X Y : ℕ → PMF (List Bool)} (h : ComputationallyIndistinguishable X Y) {f : ℕ → List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => f p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) : ComputationallyIndistinguishable (fun (n : ℕ) => PMF.map (f n) (X n)) fun (n : ℕ) => PMF.map (f n) (Y n)

Efficient parameter-dependent deterministic postprocessing preserves indistinguishability.

theorem Cslib.Crypto.ComputationallyIndistinguishable.shift {X Y : ℕ → PMF (List Bool)} (h : ComputationallyIndistinguishable X Y) (c : ℕ) : ComputationallyIndistinguishable (fun (n : ℕ) => X (n + c)) fun (n : ℕ) => Y (n + c)

Shifting the security parameter by a fixed additive offset preserves computational indistinguishability.