From 1b9f06b1b9e82957fcf6a0c3d074a5adc09f5f03 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 4 Oct 2026 00:43:35 -0400 Subject: [PATCH 1/2] feat(Crypto): add security games MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds `Cslib.Crypto.Game`. A `Game` is a `PMF Bool`, the distribution of a Boolean experiment, and `advantage` is the absolute difference of acceptance probabilities ([BonehShoup2023] §3.1). It satisfies the triangle inequality used in game hopping. `Game.Secure real ideal Admissible` says that every admissible adversary has negligible advantage, with admissibility checked before the security parameter is chosen. `Game.SecureWithError` asks instead for a common concrete bound at each parameter. Both come with monotonicity, symmetry, transitivity, and reduction lemmas. Stating these once lets finite primitives such as the PRG games and computational definitions over infinite sample spaces share one advantage convention. --- Cslib.lean | 1 + Cslib/Crypto/Game.lean | 174 +++++++++++++++++++++++++++++++++++++++++ Cslib/Crypto/README.md | 2 + 3 files changed, 177 insertions(+) create mode 100644 Cslib/Crypto/Game.lean diff --git a/Cslib.lean b/Cslib.lean index 999815edf..280744c4a 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -99,6 +99,7 @@ public import Cslib.Computability.URM.Defs public import Cslib.Computability.URM.Execution public import Cslib.Computability.URM.StandardForm public import Cslib.Computability.URM.StraightLine +public import Cslib.Crypto.Game public import Cslib.Crypto.Negligible public import Cslib.Crypto.Primitives.PRG.Asymptotic public import Cslib.Crypto.Primitives.PRG.Basic diff --git a/Cslib/Crypto/Game.lean b/Cslib/Crypto/Game.lean new file mode 100644 index 000000000..67dcadfe2 --- /dev/null +++ b/Cslib/Crypto/Game.lean @@ -0,0 +1,174 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Cslib.Crypto.Negligible +public import Cslib.Probability.PMF + +/-! +# Security of Boolean experiments + +A `Game` is the distribution of a Boolean experiment. Its acceptance probability, distinguishing +advantage, and asymptotic security are independent of the language used to write the experiment. +`Game.Secure` restricts whole adversaries, which may themselves be families of tests. Finite +cryptographic primitives instantiate these definitions directly, and computational definitions +over infinite sample spaces can reuse them. + +The advantage convention is the absolute difference of acceptance probabilities, as in +[BonehShoup2023], Section 3.1. Negligibility is Mathlib's superpolynomial decay. +-/ + +@[expose] public section + +namespace Cslib.Crypto + +open scoped NNReal + +/-- The distribution of the Boolean result of a security experiment. -/ +abbrev Game := PMF Bool + +namespace Game + +/-- The probability that an experiment accepts. -/ +noncomputable abbrev winProbability (game : Game) : ℝ := (game true).toReal + +/-- The absolute difference of two experiments' acceptance probabilities. -/ +noncomputable abbrev advantage (real ideal : Game) : ℝ := + |real.winProbability - ideal.winProbability| + +/-- Distinguishing advantage is nonnegative. -/ +theorem advantage_nonneg (real ideal : Game) : 0 ≤ advantage real ideal := abs_nonneg _ + +/-- Equal experiments have zero advantage. -/ +@[simp] theorem advantage_self (game : Game) : advantage game game = 0 := by + simp [advantage] + +/-- Swapping the experiments preserves advantage. -/ +theorem advantage_comm (real ideal : Game) : advantage real ideal = advantage ideal real := + abs_sub_comm _ _ + +/-- Complementing a game's answer exchanges acceptance and rejection. -/ +@[simp] theorem winProbability_not (game : Game) : + winProbability (game.map Bool.not) = 1 - winProbability game := by + rw [eq_sub_iff_add_eq', ← Probability.PMF.sum_toReal game, Fintype.sum_bool] + simp [winProbability, PMF.map_apply, tsum_fintype] + +/-- Complementing both answers preserves advantage. -/ +@[simp] theorem advantage_not (real ideal : Game) : + advantage (real.map Bool.not) (ideal.map Bool.not) = advantage real ideal := by + rw [advantage, advantage, winProbability_not, winProbability_not, sub_sub_sub_cancel_left, + abs_sub_comm] + +/-- The elementary game-hopping inequality. -/ +theorem advantage_triangle (first middle last : Game) : + advantage first last ≤ advantage first middle + advantage middle last := abs_sub_le _ _ _ + +/-- Distinguishing advantage is at most one. -/ +theorem advantage_le_one (real ideal : Game) : advantage real ideal ≤ 1 := by + have hle (game : Game) : winProbability game ≤ 1 := by + simpa using ENNReal.toReal_mono ENNReal.one_ne_top (PMF.coe_le_one game true) + exact abs_sub_le_of_nonneg_of_le ENNReal.toReal_nonneg (hle real) ENNReal.toReal_nonneg + (hle ideal) + +/-- Comparing with certain rejection measures the probability of winning. -/ +@[simp] theorem advantage_pure_false (game : Game) : + advantage game (PMF.pure false) = winProbability game := by + simp [advantage, winProbability] + +/-- Comparing with a fair coin measures absolute prediction bias. -/ +@[simp] theorem advantage_uniform_bool (game : Game) : + advantage game (PMF.uniformOfFintype Bool) = |winProbability game - 1 / 2| := by + simp [advantage, winProbability, PMF.uniformOfFintype_apply] + +/-- 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 Secure {Adversary : Type*} (real ideal : Adversary → ℕ → Game) + (Admissible : Adversary → Prop) : Prop := + ∀ adversary, Admissible adversary → + Negligible (fun n => advantage (real adversary n) (ideal adversary n)) + +/-- A common bound on the advantage of all admissible adversaries at each parameter. -/ +def SecureWithError {Adversary : Type*} (real ideal : Adversary → ℕ → Game) + (Admissible : Adversary → Prop) (ε : ℕ → ℝ≥0) : Prop := + ∀ adversary, Admissible adversary → + ∀ n, advantage (real adversary n) (ideal adversary n) ≤ ε n + +/-- Restricting admissibility preserves a concrete security bound. -/ +theorem SecureWithError.of_admissible {Adversary : Type*} + {real ideal : Adversary → ℕ → Game} {Admissible Restricted : Adversary → Prop} + {ε : ℕ → ℝ≥0} (h : SecureWithError real ideal Admissible ε) + (hsub : ∀ adversary, Restricted adversary → Admissible adversary) : + SecureWithError real ideal Restricted ε := fun adversary ha => h adversary (hsub adversary ha) + +/-- Enlarging an error budget preserves its security guarantee. -/ +theorem SecureWithError.mono {Adversary : Type*} {real ideal : Adversary → ℕ → Game} + {Admissible : Adversary → Prop} {ε δ : ℕ → ℝ≥0} + (h : SecureWithError real ideal Admissible ε) (hle : ∀ n, ε n ≤ δ n) : + SecureWithError real ideal Admissible δ := + fun adversary ha n => (h adversary ha n).trans (by exact_mod_cast hle n) + +/-- Swapping the experiments preserves the same concrete error. -/ +theorem SecureWithError.symm {Adversary : Type*} {real ideal : Adversary → ℕ → Game} + {Admissible : Adversary → Prop} {ε : ℕ → ℝ≥0} + (h : SecureWithError real ideal Admissible ε) : SecureWithError ideal real Admissible ε := + fun adversary ha n => (advantage_comm _ _).trans_le (h adversary ha n) + +/-- Concrete security bounds add across a game hop. -/ +theorem SecureWithError.trans {Adversary : Type*} {first middle last : Adversary → ℕ → Game} + {Admissible : Adversary → Prop} {ε δ : ℕ → ℝ≥0} + (hfirst : SecureWithError first middle Admissible ε) + (hlast : SecureWithError middle last Admissible δ) : + SecureWithError first last Admissible (fun n => ε n + δ n) := fun adversary ha n => + (advantage_triangle _ _ _).trans (add_le_add (hfirst adversary ha n) (hlast adversary ha n)) + +/-- Restricting the admissible adversaries preserves security. -/ +theorem Secure.of_admissible {Adversary : Type*} {real ideal : Adversary → ℕ → Game} + {Admissible Restricted : Adversary → Prop} (h : Secure real ideal Admissible) + (hsub : ∀ adversary, Restricted adversary → Admissible adversary) : + Secure real ideal Restricted := fun adversary ha => h adversary (hsub adversary ha) + +/-- An experiment is secure relative to itself. -/ +theorem Secure.refl {Adversary : Type*} (game : Adversary → ℕ → Game) + (Admissible : Adversary → Prop) : Secure game game Admissible := + fun _ _ => by simp + +/-- Swapping the experiments preserves security. -/ +theorem Secure.symm {Adversary : Type*} {real ideal : Adversary → ℕ → Game} + {Admissible : Adversary → Prop} (h : Secure real ideal Admissible) : + Secure ideal real Admissible := + fun adversary ha => (h adversary ha).congr fun _ => advantage_comm _ _ + +/-- Security composes through an intermediate experiment. -/ +theorem Secure.trans {Adversary : Type*} {first middle last : Adversary → ℕ → Game} + {Admissible : Adversary → Prop} (hfirst : Secure first middle Admissible) + (hlast : Secure middle last Admissible) : Secure first last Admissible := fun adversary ha => + negligible_of_le ((hfirst adversary ha).add (hlast adversary ha)) + (fun _ => advantage_nonneg _ _) (fun _ => advantage_triangle _ _ _) + +/-- A reduction preserves security when it preserves admissibility and bounds advantage. -/ +theorem Secure.of_reduction {Source Target : Type*} + {sourceReal sourceIdeal : Source → ℕ → Game} {targetReal targetIdeal : Target → ℕ → Game} + {SourceAdmissible : Source → Prop} {TargetAdmissible : Target → Prop} + (h : Secure sourceReal sourceIdeal SourceAdmissible) (reduce : Target → Source) + (hadmissible : ∀ adversary, TargetAdmissible adversary → SourceAdmissible (reduce adversary)) + (hbound : ∀ adversary, TargetAdmissible adversary → ∀ n, + advantage (targetReal adversary n) (targetIdeal adversary n) ≤ + advantage (sourceReal (reduce adversary) n) (sourceIdeal (reduce adversary) n)) : + Secure targetReal targetIdeal TargetAdmissible := fun adversary ha => + negligible_of_le (h _ (hadmissible adversary ha)) (fun _ => advantage_nonneg _ _) + (hbound adversary ha) + +/-- A negligible common error bound implies asymptotic security. -/ +theorem SecureWithError.secure {Adversary : Type*} {real ideal : Adversary → ℕ → Game} + {Admissible : Adversary → Prop} {ε : ℕ → ℝ≥0} + (h : SecureWithError real ideal Admissible ε) + (hε : Negligible (fun n => (ε n : ℝ))) : Secure real ideal Admissible := fun adversary ha => + negligible_of_le hε (fun _ => advantage_nonneg _ _) (h adversary ha) + +end Game +end Cslib.Crypto diff --git a/Cslib/Crypto/README.md b/Cslib/Crypto/README.md index 2d36e4e48..e64f331d1 100644 --- a/Cslib/Crypto/README.md +++ b/Cslib/Crypto/README.md @@ -23,6 +23,8 @@ To this end, we expect to leverage the combination of `Crypto` and [Languages](. [`Negligible`](Negligible.lean) specializes Mathlib's `SuperpolynomialDecay` to natural security parameters, with zero, comparison, and polynomial-loss bounds. +[`Game`](Game.lean) gives the acceptance probability, distinguishing advantage and negligible +security of Boolean experiments. ## Pseudorandom generators From 9b855ebe8683ca423ecfb113947452647f5fdfbc Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 4 Oct 2026 19:01:54 -0400 Subject: [PATCH 2/2] style(Crypto): trim simp arguments in security games --- Cslib/Crypto/Game.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cslib/Crypto/Game.lean b/Cslib/Crypto/Game.lean index 67dcadfe2..ab05be4ca 100644 --- a/Cslib/Crypto/Game.lean +++ b/Cslib/Crypto/Game.lean @@ -45,7 +45,7 @@ theorem advantage_nonneg (real ideal : Game) : 0 ≤ advantage real ideal := abs /-- Equal experiments have zero advantage. -/ @[simp] theorem advantage_self (game : Game) : advantage game game = 0 := by - simp [advantage] + simp /-- Swapping the experiments preserves advantage. -/ theorem advantage_comm (real ideal : Game) : advantage real ideal = advantage ideal real := @@ -55,7 +55,7 @@ theorem advantage_comm (real ideal : Game) : advantage real ideal = advantage id @[simp] theorem winProbability_not (game : Game) : winProbability (game.map Bool.not) = 1 - winProbability game := by rw [eq_sub_iff_add_eq', ← Probability.PMF.sum_toReal game, Fintype.sum_bool] - simp [winProbability, PMF.map_apply, tsum_fintype] + simp [winProbability] /-- Complementing both answers preserves advantage. -/ @[simp] theorem advantage_not (real ideal : Game) : @@ -82,7 +82,7 @@ theorem advantage_le_one (real ideal : Game) : advantage real ideal ≤ 1 := by /-- Comparing with a fair coin measures absolute prediction bias. -/ @[simp] theorem advantage_uniform_bool (game : Game) : advantage game (PMF.uniformOfFintype Bool) = |winProbability game - 1 / 2| := by - simp [advantage, winProbability, PMF.uniformOfFintype_apply] + simp [advantage, winProbability] /-- 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