One negligible bound for a bounded family of tests

Sample a dyadic index and calibrate its test with a fresh sample from the selected reference ensemble. The resulting advantage is the average of the indexed squared advantages, so positive and negative gaps cannot cancel. This supplies one negligible bound for all indices in a polynomially bounded range, even if the chosen index is not computable.

Both ensembles must have uniform efficient samplers: calibration samples a direction and runs the selected real-or-ideal reference experiment, followed by the challenge. The adversary is one uniformly efficient indexed program, not a family of separate certificates. Runtime charges include the unary index, reference sample and challenge.

Main definitions

• Cslib.Crypto.UniformChoice.test: the calibrated indexed reduction.

Main results

• Cslib.Crypto.UniformChoice.advantage_eq: exact average of squared advantages.
• Cslib.Crypto.ComputationallyIndistinguishable.uniform_bound: one bound for every allowed index.

References

This uniform sampling argument supplies the parameter conversion used with T. Holenstein, Pseudorandom Generators from One-Way Functions, Section 5.

Adapted from Crypto/Computational/UniformChoice.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed machine certificates and the nonnegative game API.

noncomputable def Cslib.Crypto.UniformChoice.test (bound : ℕ) (real ideal : ProbComp (List Bool)) (adversary : ℕ → List Bool → ProbComp Bool) (challenge : List Bool) : ProbComp Bool

Sample an index and calibrate its test using a fresh real-or-ideal reference sample.

theorem Cslib.Crypto.UniformChoice.isPPTOn_test {α : Type} {input : α ↪ List Bool} {bound : α → ℕ} {real ideal : α → ProbComp (List Bool)} {adversary : α → ℕ → List Bool → ProbComp Bool} {challenge : α → List Bool} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hreal : Probability.IsPPTOn input Turing.MultiTapeTM.encBits real) (hideal : Probability.IsPPTOn input Turing.MultiTapeTM.encBits ideal) (hadversary : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (a : (α × ℕ) × List Bool) => adversary a.1.1 a.1.2 a.2) (hchallenge : Turing.MultiTapeTM.ComputableTidilyInPolyTime challenge input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => test (bound a) (real a) (ideal a) (adversary a) (challenge a)

The reduction charges sampling, reference data and both captured adversary calls.

theorem Cslib.Crypto.UniformChoice.eval_bind_test (bound : ℕ) (real ideal source : ProbComp (List Bool)) (adversary : ℕ → List Bool → ProbComp Bool) : (source >>= test bound real ideal adversary).eval = do let index ← Probability.PMF.uniformOfFintype (Fin (Probability.dyadicSize bound)) (calibratedTest (real >>= adversary ↑index) (ideal >>= adversary ↑index) (source >>= adversary ↑index)).eval

The challenge commutes with the independent index and calibration trial.

theorem Cslib.Crypto.UniformChoice.advantage_eq (bound : ℕ) (real ideal : ProbComp (List Bool)) (adversary : ℕ → List Bool → ProbComp Bool) : Game.advantage (real >>= test bound real ideal adversary).eval (ideal >>= test bound real ideal adversary).eval = (∑ index : Fin (Probability.dyadicSize bound), Game.advantage (real >>= adversary ↑index).eval (ideal >>= adversary ↑index).eval ^ 2) / ↑(Probability.dyadicSize bound)

Averaging calibrated tests averages their squared advantages without sign cancellation.

theorem Cslib.Crypto.UniformChoice.advantage_sq_le (bound : ℕ) (real ideal : ProbComp (List Bool)) (adversary : ℕ → List Bool → ProbComp Bool) {index : ℕ} (hindex : index ≤ bound) : Game.advantage (real >>= adversary index).eval (ideal >>= adversary index).eval ^ 2 ≤ ↑(Probability.dyadicSize bound) * Game.advantage (real >>= test bound real ideal adversary).eval (ideal >>= test bound real ideal adversary).eval

A particular index is used only in this inequality; it need not be computed by the test.

theorem Cslib.Crypto.ComputationallyIndistinguishable.uniform_bound {real ideal : ℕ → ProbComp (List Bool)} {bound : ℕ → ℕ} (hsecure : ComputationallyIndistinguishable (fun (n : ℕ) => (real n).eval) fun (n : ℕ) => (ideal n).eval) (hreal : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits real) (hideal : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits ideal) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (adversary : ℕ → ℕ → List Bool → ProbComp Bool) (hadversary : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (a : (ℕ × ℕ) × List Bool) => adversary a.1.1 a.1.2 a.2) : ∃ (ε : ℕ → NNReal), Negligible ε ∧ ∀ (n index : ℕ), index ≤ bound n → Game.advantage (real n >>= adversary n index).eval (ideal n >>= adversary n index).eval ≤ ε n

Efficient samplers allow one negligible bound for every polynomially bounded index of one uniform test. Choosing the index requires no computability assumption.