Security Experiments

This file defines simple security experiments that succeed unless they terminate with failure. Each experiment carries bundled subprobabilistic semantics, so the experiment can be interpreted through an internal semantic monad instead of requiring a global MonadLiftT _ SPMF instance on the ambient monad.

We also define BoundedAdversary α β as an oracle computation bundled with a query bound.

noncomputable def ProbComp.boolBiasAdvantage (p : ProbComp Bool) : ℝ

Bias advantage of a Boolean-valued game: the gap between the probabilities of the two outputs.

This is the canonical single-game formulation for hidden-bit guessing experiments.

noncomputable def ProbComp.boolDistAdvantage (p q : ProbComp Bool) : ℝ

Distinguishing advantage between two Boolean-valued games, measured on the true branch.

For Boolean outputs this is equivalent to measuring the gap on false; choosing true is just a conventional presentation.

noncomputable def SPMF.boolBiasAdvantage (p : SPMF Bool) : ℝ

Bias advantage of a Boolean-valued subdistribution: the gap between the probabilities of returning true and false.

This is the SPMF analogue of ProbComp.boolBiasAdvantage, used for games that have already been observed under bundled subprobabilistic semantics. Any remaining mass corresponds to failure and therefore contributes to neither Boolean branch.

noncomputable def SPMF.boolDistAdvantage (p q : SPMF Bool) : ℝ

Distinguishing advantage between two Boolean-valued subdistributions, measured on the true branch. SPMF analogue of ProbComp.boolDistAdvantage.

theorem SPMF.boolBiasAdvantage_eq_two_mul_abs_sub_half (p : SPMF Bool) (htotal : Pr[= true | p] + Pr[= false | p] = 1) : p.boolBiasAdvantage = 2 * |Pr[= true | p].toReal - 1 / 2|

Re-express SPMF Boolean bias as twice the absolute deviation of Pr[true] from 1/2, assuming the SPMF is a full distribution (no failure mass).

theorem SPMF.boolBiasAdvantage_eq_boolDistAdvantage_coin_branch (coin p q : SPMF Bool) (hcoin_true : Pr[= true | coin] = 1 / 2) (hcoin_false : Pr[= false | coin] = 1 / 2) (hp : Pr[= true | p] + Pr[= false | p] = 1) (hq : Pr[= true | q] + Pr[= false | q] = 1) : (do let b ← coin let z ← if b = true then p else q pure (b == z)).boolBiasAdvantage = p.boolDistAdvantage q

Hidden-bit decomposition at the SPMF level: the bias of a coin-flip guessing game equals the distinguishing advantage between the two branches, assuming the coin is fair and both branches have full mass (no failure).

This is the SPMF analogue of ProbComp.boolBiasAdvantage_eq_boolDistAdvantage_uniformBool_branch. The ProbComp version holds unconditionally because ProbComp distributions always have total mass

1. For SPMF distributions, the totality hypotheses are required because failure mass breaks the Pr[false] = 1 - Pr[true] identity that the decomposition depends on.

theorem SPMF.boolDistAdvantage_triangle (p q r : SPMF Bool) : p.boolDistAdvantage r ≤ p.boolDistAdvantage q + q.boolDistAdvantage r

Triangle inequality for SPMF Boolean distinguishing advantage.

theorem ProbComp.boolDistAdvantage_triangle (p q r : ProbComp Bool) : p.boolDistAdvantage r ≤ p.boolDistAdvantage q + q.boolDistAdvantage r

Triangle inequality for Boolean distinguishing advantage.

theorem ProbComp.probOutput_true_le_add_ofReal_boolDistAdvantage (p q : ProbComp Bool) : Pr[= true | p] ≤ Pr[= true | q] + ENNReal.ofReal (p.boolDistAdvantage q)

The true-branch probability of one Boolean-valued game is bounded above by the true-branch probability of another game plus their distinguishing advantage.

This is the ENNReal-level interpretation of the real-valued identity a ≤ b + |a - b|, packaged for SSP game-hopping: converting an advantage p q ≤ ε assumption into a direct probability inequality Pr[true|p] ≤ Pr[true|q] + ENNReal.ofReal ε that plugs into chained calc-style bounds.

theorem ProbComp.boolBiasAdvantage_eq_two_mul_abs_sub_half (p : ProbComp Bool) : p.boolBiasAdvantage = 2 * |Pr[= true | p].toReal - 1 / 2|

Re-express Boolean bias as twice the absolute deviation of Pr[true] from 1/2.

theorem ProbComp.boolBiasAdvantage_eq_boolDistAdvantage_uniformBool_branch (real rand : ProbComp Bool) : (do let b ← $ᵗ Bool have __do_jp : Bool → ProbComp Bool := fun (z : Bool) => pure (b == z) if b = true then do let y ← real __do_jp y else do let y ← rand __do_jp y).boolBiasAdvantage = real.boolDistAdvantage rand

A hidden-bit guessing game over two Boolean branches has bias exactly equal to the distinguishing advantage between those two branches.

theorem ProbComp.boolBiasAdvantage_bind_uniformBool_eq_boolDistAdvantage {α : Type} (pref : ProbComp α) (real rand : α → ProbComp Bool) : (do let a ← pref let b ← $ᵗ Bool have __do_jp : Bool → ProbComp Bool := fun (z : Bool) => pure (b == z) if b = true then do let y ← real a __do_jp y else do let y ← rand a __do_jp y).boolBiasAdvantage = (do let a ← pref real a).boolDistAdvantage do let a ← pref rand a

Version of boolBiasAdvantage_eq_boolDistAdvantage_uniformBool_branch with a shared sampled prefix before the real/random branch is chosen.

noncomputable def ProbComp.guessAdvantage (p : ProbComp Unit) : ℝ

The advantage of a game p, assumed to be a probabilistic computation ending with a guard statement, is the absolute difference between the probability of success and 1/2.

theorem ProbComp.guessAdvantage_eq_half_sub_probFailure (p : ProbComp Unit) : p.guessAdvantage = |1 / 2 - Pr[⊥ | p].toReal|

theorem ProbComp.guessAdvantage_eq_half_of_sub (p : ProbComp Unit) : p.guessAdvantage = 2⁻¹ * |Pr[⊥ | p].toReal - Pr[= () | p].toReal|

noncomputable def ProbComp.distAdvantage (p q : ProbComp Unit) : ℝ

The advantage between two games p and q, modeled as probabilistic computations returning Unit, is the absolute difference between their probabilities of success.

@[simp]

theorem ProbComp.distAdvantage_self (p : ProbComp Unit) : p.distAdvantage p = 0

theorem ProbComp.distAdvantage_comm (p q : ProbComp Unit) : p.distAdvantage q = q.distAdvantage p

theorem ProbComp.distAdvantage_eq_abs_sub_probFailure (p q : ProbComp Unit) : p.distAdvantage q = |Pr[⊥ | p].toReal - Pr[⊥ | q].toReal|

theorem ProbComp.distAdvantage_nonneg (p q : ProbComp Unit) : 0 ≤ p.distAdvantage q

theorem ProbComp.distAdvantage_triangle (p q r : ProbComp Unit) : p.distAdvantage r ≤ p.distAdvantage q + q.distAdvantage r

theorem ProbComp.distAdvantage_le_sum_range {n : ℕ} (games : ℕ → ProbComp Unit) : (games 0).distAdvantage (games n) ≤ ∑ i ∈ Finset.range n, (games i).distAdvantage (games (i + 1))

theorem ProbComp.distAdvantage_eq_tvDist (p q : ProbComp Unit) : p.distAdvantage q = tvDist p q

structure BoundedAdversary {ι : Type u} [DecidableEq ι] (spec : OracleSpec ι) (α β : Type u) : Type u

A security adversary bundling a computation with a bound on the number of queries it makes, where the bound must be shown to satisfy IsQueryBound. We also require an explicit list of all oracles used in the computation, which is necessary in order to make certain reductions computable.

• run : α → OracleComp spec β
• qb : ι → ℕ
• qb_isQueryBound (x : α) : (self.run x).IsPerIndexQueryBound self.qb
• activeOracles : List ι
• mem_activeOracles_iff (i : ι) : i ∈ self.activeOracles ↔ self.qb i ≠ 0

structure SecExp (m : Type → Type w) [Monad m] extends SPMFSemantics m : Type (max (u_1 + 1) w)

Structure to represent a security experiment. The experiment is considered successful unless it terminates with failure.

A SecExp carries bundled SPMFSemantics directly. This keeps the semantic assumptions attached to the experiment itself: the surface monad can be interpreted through some internal semantic monad, and only then observed as a subdistribution for measuring success and failure probabilities.

• Sem : Type → Type u_1
• instMonadSem : Monad self.Sem
• interpret : m →ᵐ self.Sem
• observe {α : Type} : self.Sem α → SPMF α
• main : m Unit

  Main experiment body. Success is interpreted as terminating without failure.

noncomputable def SecExp.advantage {m : Type → Type w} [Monad m] (exp : SecExp m) : ENNReal

Advantage of a failure-based security experiment: one minus its failure probability.

@[simp]

theorem SecExp.advantage_eq_zero_iff {m : Type → Type w} [Monad m] (exp : SecExp m) : exp.advantage = 0 ↔ Pr[⊥ | exp.evalDist exp.main] = 1

A failure-based experiment has zero advantage exactly when it fails with probability 1.

@[simp]

theorem SecExp.advantage_eq_one_iff {m : Type → Type w} [Monad m] (exp : SecExp m) : exp.advantage = 1 ↔ Pr[⊥ | exp.evalDist exp.main] = 0

A failure-based experiment has advantage 1 exactly when it never fails.