Security of Boolean experiments

A Game is the distribution of the Boolean output of a security experiment, independent of the language used to write the experiment. A game has a success probability, and two games have a distinguishing advantage: the absolute difference of their success probabilities, as in [BS23], Section 3.1. The convention where the advantage of a single game is its success probability is comparison with certain failure, and the convention measuring bias away from a fair coin is guessingAdvantage.

Families of games indexed by a natural-number security parameter are indistinguishable for a class of adversaries when every admissible adversary has negligible advantage. Adversaries are whole objects, which may themselves be families of tests, and the game at each parameter is obtained from the adversary. Finite cryptographic primitives instantiate these definitions directly, and computational definitions over infinite sample spaces can reuse them.

Main definitions

• Cslib.Crypto.Game: Boolean experiment distributions with nonnegative success and advantage.
• Cslib.Crypto.Game.Indistinguishable: negligible advantage for each admissible adversary.

Main results

• Cslib.Crypto.Game.Indistinguishable.of_reduction: preserve admissibility and transfer security with a polynomial loss and negligible error.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 3.1.

Copied from cslib PR #1069 at 1d14c55a10cfe3fe4463cffa61a7f02f0d56f502.

@[reducible, inline]

abbrev Cslib.Crypto.Game : Type

The distribution of the Boolean output of a security experiment.

@[reducible, inline]

abbrev Cslib.Crypto.Game.succProbability (game : Game) : NNReal

The probability that an experiment succeeds, that is, outputs true.

@[reducible, inline]

abbrev Cslib.Crypto.Game.failProbability (game : Game) : NNReal

The probability that an experiment fails, that is, outputs false.

theorem Cslib.Crypto.Game.succProbability_le_one (game : Game) : game.succProbability ≤ 1

Success probability is at most one.

theorem Cslib.Crypto.Game.succProbability_add_failProbability (game : Game) : game.succProbability + game.failProbability = 1

An experiment either succeeds or fails.

theorem Cslib.Crypto.Game.failProbability_eq (game : Game) : game.failProbability = 1 - game.succProbability

Failure probability is the complement of success probability.

@[simp]

theorem Cslib.Crypto.Game.succProbability_not (game : Game) : succProbability (PMF.map not game) = game.failProbability

Complementing a game's answer exchanges success and failure.

@[reducible, inline]

abbrev Cslib.Crypto.Game.advantage (game1 game2 : Game) : NNReal

The distinguishing advantage between two games is the absolute difference of their success probabilities.

theorem Cslib.Crypto.Game.coe_advantage (game1 game2 : Game) : ↑(game1.advantage game2) = |↑game1.succProbability - ↑game2.succProbability|

As a real number, the advantage is the absolute difference of the success probabilities.

theorem Cslib.Crypto.Game.advantage_le_one (game1 game2 : Game) : game1.advantage game2 ≤ 1

Distinguishing advantage is at most one.

theorem Cslib.Crypto.Game.advantage_self (game : Game) : game.advantage game = 0

Equal games have zero advantage.

theorem Cslib.Crypto.Game.advantage_comm (game1 game2 : Game) : game1.advantage game2 = game2.advantage game1

Swapping the games preserves advantage.

@[simp]

theorem Cslib.Crypto.Game.advantage_not (game1 game2 : Game) : advantage (PMF.map not game1) (PMF.map not game2) = game1.advantage game2

Complementing both answers preserves advantage.

theorem Cslib.Crypto.Game.advantage_triangle (first middle last : Game) : first.advantage last ≤ first.advantage middle + middle.advantage last

The elementary game-hopping inequality.

@[simp]

theorem Cslib.Crypto.Game.advantage_pure_false (game : Game) : game.advantage (PMF.pure false) = game.succProbability

Comparing with certain failure measures the probability of success.

@[reducible, inline]

noncomputable abbrev Cslib.Crypto.Game.guessingAdvantage (game : Game) : NNReal

The advantage of a game over a fair coin, measuring its prediction bias.

theorem Cslib.Crypto.Game.coe_guessingAdvantage (game : Game) : ↑game.guessingAdvantage = |↑game.succProbability - 1 / 2|

As a real number, the guessing advantage is the distance of the success probability from one half.

def Cslib.Crypto.Game.Indistinguishable {Adversary : Type u_1} (game1 game2 : Adversary → ℕ → Game) (Admissible : Adversary → Prop) : Prop

Two families of games are indistinguishable for a class of adversaries when each admissible adversary has negligible advantage. The admissibility predicate applies to the whole adversary before the security parameter is supplied, so it can constrain the adversary across all parameters at once.

def Cslib.Crypto.Game.IndistinguishableWithError {Adversary : Type u_1} (game1 game2 : Adversary → ℕ → Game) (Admissible : Adversary → Prop) (ε : ℕ → NNReal) : Prop

A common concrete bound on the advantage of all admissible adversaries at each parameter.

theorem Cslib.Crypto.Game.IndistinguishableWithError.of_admissible {Adversary : Type u_1} {game1 game2 : Adversary → ℕ → Game} {Admissible Restricted : Adversary → Prop} {ε : ℕ → NNReal} (h : IndistinguishableWithError game1 game2 Admissible ε) (hsub : ∀ (adversary : Adversary), Restricted adversary → Admissible adversary) : IndistinguishableWithError game1 game2 Restricted ε

Restricting admissibility preserves a concrete bound.

theorem Cslib.Crypto.Game.Indistinguishable.of_admissible {Adversary : Type u_1} {game1 game2 : Adversary → ℕ → Game} {Admissible Restricted : Adversary → Prop} (h : Indistinguishable game1 game2 Admissible) (hsub : ∀ (adversary : Adversary), Restricted adversary → Admissible adversary) : Indistinguishable game1 game2 Restricted

Restricting admissibility preserves indistinguishability.

theorem Cslib.Crypto.Game.IndistinguishableWithError.mono {Adversary : Type u_1} {game1 game2 : Adversary → ℕ → Game} {Admissible : Adversary → Prop} {ε δ : ℕ → NNReal} (h : IndistinguishableWithError game1 game2 Admissible ε) (hle : ∀ (n : ℕ), ε n ≤ δ n) : IndistinguishableWithError game1 game2 Admissible δ

Enlarging an error budget preserves its guarantee.

theorem Cslib.Crypto.Game.Indistinguishable.refl {Adversary : Type u_1} (game : Adversary → ℕ → Game) (Admissible : Adversary → Prop) : Indistinguishable game game Admissible

A family of games is indistinguishable from itself.

theorem Cslib.Crypto.Game.IndistinguishableWithError.symm {Adversary : Type u_1} {game1 game2 : Adversary → ℕ → Game} {Admissible : Adversary → Prop} {ε : ℕ → NNReal} (h : IndistinguishableWithError game1 game2 Admissible ε) : IndistinguishableWithError game2 game1 Admissible ε

Swapping the games preserves a concrete bound.

theorem Cslib.Crypto.Game.Indistinguishable.symm {Adversary : Type u_1} {game1 game2 : Adversary → ℕ → Game} {Admissible : Adversary → Prop} (h : Indistinguishable game1 game2 Admissible) : Indistinguishable game2 game1 Admissible

Swapping the games preserves indistinguishability.

theorem Cslib.Crypto.Game.IndistinguishableWithError.trans {Adversary : Type u_1} {first middle last : Adversary → ℕ → Game} {Admissible : Adversary → Prop} {ε δ : ℕ → NNReal} (hfirst : IndistinguishableWithError first middle Admissible ε) (hlast : IndistinguishableWithError middle last Admissible δ) : IndistinguishableWithError first last Admissible fun (n : ℕ) => ε n + δ n

Concrete bounds add across a game hop.

theorem Cslib.Crypto.Game.Indistinguishable.trans {Adversary : Type u_1} {first middle last : Adversary → ℕ → Game} {Admissible : Adversary → Prop} (hfirst : Indistinguishable first middle Admissible) (hlast : Indistinguishable middle last Admissible) : Indistinguishable first last Admissible

Indistinguishability composes through an intermediate family of games.

theorem Cslib.Crypto.Game.IndistinguishableWithError.indistinguishable {Adversary : Type u_1} {game1 game2 : Adversary → ℕ → Game} {Admissible : Adversary → Prop} {ε : ℕ → NNReal} (h : IndistinguishableWithError game1 game2 Admissible ε) (hε : Negligible ε) : Indistinguishable game1 game2 Admissible

A negligible common error bound implies indistinguishability.

theorem Cslib.Crypto.Game.Indistinguishable.of_reduction {SourceAdversary : Type u_1} {TargetAdversary : Type u_2} {source1 source2 : SourceAdversary → ℕ → Game} {target1 target2 : TargetAdversary → ℕ → Game} {SourceAdmissible : SourceAdversary → Prop} {TargetAdmissible : TargetAdversary → Prop} (h : Indistinguishable source1 source2 SourceAdmissible) (reduce : TargetAdversary → SourceAdversary) (hadmissible : ∀ (adversary : TargetAdversary), TargetAdmissible adversary → SourceAdmissible (reduce adversary)) (hbound : ∀ (adversary : TargetAdversary), TargetAdmissible adversary → ∃ (loss : ℕ → ℕ) (error : ℕ → NNReal), PolynomiallyBounded loss ∧ Negligible error ∧ ∀ (n : ℕ), (target1 adversary n).advantage (target2 adversary n) ≤ ↑(loss n) * (source1 (reduce adversary) n).advantage (source2 (reduce adversary) n) + error n) : Indistinguishable target1 target2 TargetAdmissible

A reduction turns each target adversary into a source adversary. It transfers indistinguishability from the source games to the target games when it preserves admissibility and bounds the target advantage by the source advantage up to a polynomial loss and a negligible error. The loss and the error may depend on the target adversary, while the reduction maps whole adversaries and does not depend on the security parameter.

@[simp]

theorem Cslib.Crypto.Game.coe_succProbability (game : Game) : ↑game.succProbability = (game true).toReal

As a real number, the success probability is the real-valued probability of true.