From 75e9e26486009bd00a1952dbf1e6a635ff7b3f9b Mon Sep 17 00:00:00 2001 From: Marc Ilunga Date: Mon, 12 Oct 2026 17:01:33 +0100 Subject: [PATCH] =?UTF-8?q?Bounds=20in=20=E2=84=9D=E2=89=A50?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Security bounds are stated in ℝ≥0 and read in ℝ≥0∞ through the coercion, which is additive and order-preserving, instead of through `ENNReal.ofReal`, which clamps negatives and is additive only on non-negative arguments. `ofReal` stays only where the distances are defined from real probabilities and in two bridging lemmas: `RandomSystem.transcriptDistance_le` (a bound on the transcript laws under every environment) and `transcriptDistance_le_of_advantage_le` (a bound on every advantage). Restated with ε : ℝ≥0: `transcriptDistance_visible_le_of_unsetProbability`, `dist_visible_le`, `game_dist_le`, `game_dist_ofSingleFunction_le`, and the authenticated-encryption bounds, now `≤ (q_e² / |M| : ℝ≥0)`. AGENTS.md records the convention. Closes #16. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9 --- AGENTS.md | 5 ++ THEORY.md | 82 +++++++++---------- .../InterfaceGame.lean | 5 +- .../PresentedGame.lean | 10 +-- .../AuthenticatedEncryption/Collision.lean | 6 +- .../AuthenticatedEncryption/Security.lean | 10 +-- src/RandomSystems/Distance/Decision.lean | 19 ++++- src/RandomSystems/Distance/Distinguisher.lean | 14 ++++ src/RandomSystems/Game/MBO.lean | 16 ++-- src/Tests/AuthenticatedEncryption.lean | 3 +- 10 files changed, 103 insertions(+), 67 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index c914708..2780843 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -243,6 +243,11 @@ globally; use `letI` or a wrapper carrier. - New and changed code passes Mathlib's standard linter set: `lake env lean -Dweak.linter.mathlibStandardSet=true ` reports nothing. The set is not yet enabled in the lakefile, because older code does not pass it. +- Security bounds are stated in `ℝ≥0`, as `Δ R S ≤ (b : ℝ≥0)`; the coercion to `ℝ≥0∞` is + additive and order-preserving, so `push_cast` moves it. `ENNReal.ofReal` appears only where + the distances are defined from real probabilities (`transcriptDistance`, the advantages, + `advantageDistance`) and in the lemmas that bridge to them (`transcriptDistance_le`, + `transcriptDistance_le_of_advantage_le`). ## Naming and ownership diff --git a/THEORY.md b/THEORY.md index c7963a6..9c8e26f 100644 --- a/THEORY.md +++ b/THEORY.md @@ -871,30 +871,30 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [Program.inline]: src/RandomSystems/Converter/ProgramAttachment.lean#L258 [Program.combine]: src/RandomSystems/Converter/ProgramAttachment.lean#L429 [Program.trim_apply_ofProgramOn_automaton]: src/RandomSystems/Converter/ProgramAttachment.lean#L609 -[RandomSystem.transcriptDistance]: src/RandomSystems/Distance/Decision.lean#L225 -[Domain.Compatible]: src/RandomSystems/Distance/Decision.lean#L162 -[Domain.DecisionCompatible]: src/RandomSystems/Distance/Decision.lean#L168 +[RandomSystem.transcriptDistance]: src/RandomSystems/Distance/Decision.lean#L228 +[Domain.Compatible]: src/RandomSystems/Distance/Decision.lean#L165 +[Domain.DecisionCompatible]: src/RandomSystems/Distance/Decision.lean#L171 [IsDDD]: src/RandomSystems/System/InterfaceSystem.lean#L968 -[RandomSystem.decisionProbability]: src/RandomSystems/Distance/Decision.lean#L247 -[Domain.Distinguisher]: src/RandomSystems/Distance/Distinguisher.lean#L121 -[Domain.Distinguisher.probability]: src/RandomSystems/Distance/Distinguisher.lean#L125 -[Domain.Distinguisher.advantage]: src/RandomSystems/Distance/Distinguisher.lean#L131 -[advantage_self]: src/RandomSystems/Distance/Distinguisher.lean#L140 -[advantage_symm]: src/RandomSystems/Distance/Distinguisher.lean#L142 -[advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L145 -[RandomSystem.transcriptDistance_eq_iSup]: src/RandomSystems/Distance/Distinguisher.lean#L153 -[advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L182 -[Domain.DistinguisherBehavior]: src/RandomSystems/Distance/Distinguisher.lean#L193 -[DistinguisherBehavior.advantage]: src/RandomSystems/Distance/Distinguisher.lean#L204 -[DistinguisherBehavior.advantage_self]: src/RandomSystems/Distance/Distinguisher.lean#L214 -[DistinguisherBehavior.advantage_symm]: src/RandomSystems/Distance/Distinguisher.lean#L216 -[DistinguisherBehavior.advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L219 -[DistinguisherBehavior.advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L224 -[RandomSystem.transcriptDistance_eq_iSup_behavior]: src/RandomSystems/Distance/Distinguisher.lean#L232 -[DistinguisherBehavior.absorb]: src/RandomSystems/Distance/Distinguisher.lean#L277 -[DistinguisherBehavior.absorb_comp]: src/RandomSystems/Distance/Distinguisher.lean#L290 -[Domain.Distinguisher.exists_absorbAll]: src/RandomSystems/Distance/Distinguisher.lean#L251 -[Domain.Distinguisher.exists_absorbRight]: src/RandomSystems/Distance/Distinguisher.lean#L316 +[RandomSystem.decisionProbability]: src/RandomSystems/Distance/Decision.lean#L262 +[Domain.Distinguisher]: src/RandomSystems/Distance/Distinguisher.lean#L122 +[Domain.Distinguisher.probability]: src/RandomSystems/Distance/Distinguisher.lean#L126 +[Domain.Distinguisher.advantage]: src/RandomSystems/Distance/Distinguisher.lean#L132 +[advantage_self]: src/RandomSystems/Distance/Distinguisher.lean#L141 +[advantage_symm]: src/RandomSystems/Distance/Distinguisher.lean#L143 +[advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L146 +[RandomSystem.transcriptDistance_eq_iSup]: src/RandomSystems/Distance/Distinguisher.lean#L154 +[advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L196 +[Domain.DistinguisherBehavior]: src/RandomSystems/Distance/Distinguisher.lean#L207 +[DistinguisherBehavior.advantage]: src/RandomSystems/Distance/Distinguisher.lean#L218 +[DistinguisherBehavior.advantage_self]: src/RandomSystems/Distance/Distinguisher.lean#L228 +[DistinguisherBehavior.advantage_symm]: src/RandomSystems/Distance/Distinguisher.lean#L230 +[DistinguisherBehavior.advantage_triangle]: src/RandomSystems/Distance/Distinguisher.lean#L233 +[DistinguisherBehavior.advantage_le_transcriptDistance]: src/RandomSystems/Distance/Distinguisher.lean#L238 +[RandomSystem.transcriptDistance_eq_iSup_behavior]: src/RandomSystems/Distance/Distinguisher.lean#L246 +[DistinguisherBehavior.absorb]: src/RandomSystems/Distance/Distinguisher.lean#L291 +[DistinguisherBehavior.absorb_comp]: src/RandomSystems/Distance/Distinguisher.lean#L304 +[Domain.Distinguisher.exists_absorbAll]: src/RandomSystems/Distance/Distinguisher.lean#L265 +[Domain.Distinguisher.exists_absorbRight]: src/RandomSystems/Distance/Distinguisher.lean#L330 [absorbAll]: src/RandomSystems/Distance/Absorption.lean#L42 [RandomSystem.restrict]: src/RandomSystems/Distance/Restriction.lean#L59 [RandomSystem.restrict_restrict]: src/RandomSystems/Distance/Restriction.lean#L67 @@ -904,14 +904,14 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [DDG]: src/RandomSystems/Game/DiscreteMBO.lean#L50 [PDG]: src/RandomSystems/Game/DiscreteMBO.lean#L54 [PDG.ofFunction]: src/RandomSystems/Game/FunctionGame.lean#L37 -[RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L289 -[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L298 -[DDE.blindMBO]: src/RandomSystems/Game/MBO.lean#L391 -[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L461 -[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L504 -[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L758 -[Domain.Distinguisher.winProbability_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L837 -[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L862 +[RandomSystem.MonotoneMBO]: src/RandomSystems/Game/MBO.lean#L290 +[RandomSystem.visible]: src/RandomSystems/Game/MBO.lean#L299 +[DDE.blindMBO]: src/RandomSystems/Game/MBO.lean#L392 +[RandomSystem.winProbability]: src/RandomSystems/Game/MBO.lean#L462 +[RandomSystem.ConditionallyEquivalent]: src/RandomSystems/Game/MBO.lean#L505 +[Domain.Distinguisher.advantage_le_winProbability]: src/RandomSystems/Game/MBO.lean#L759 +[Domain.Distinguisher.winProbability_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L838 +[RandomSystem.transcriptDistance_visible_le_of_unsetProbability]: src/RandomSystems/Game/MBO.lean#L863 [PDCBehavior.liftMBO]: src/RandomSystems/Game/MBOAttachment.lean#L455 [PDCBehavior.liftMBO_id]: src/RandomSystems/Game/MBOAttachment.lean#L495 [PDCBehavior.liftMBO_comp]: src/RandomSystems/Game/MBOAttachment.lean#L1515 @@ -958,10 +958,10 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [Interface.Resource.ofFunction]: src/ConstructiveCryptography/Functional.lean#L56 [Interface.Resource.ofConditional]: src/ConstructiveCryptography/Functional.lean#L38 [Interface.Resource.sample]: src/ConstructiveCryptography/Functional.lean#L176 -[Interface.withMBO]: src/ConstructiveCryptography/InterfaceGame.lean#L51 -[Interface.Game]: src/ConstructiveCryptography/InterfaceGame.lean#L62 -[Interface.liftMBO]: src/ConstructiveCryptography/InterfaceGame.lean#L65 -[Interface.Game.visible]: src/ConstructiveCryptography/InterfaceGame.lean#L83 +[Interface.withMBO]: src/ConstructiveCryptography/InterfaceGame.lean#L52 +[Interface.Game]: src/ConstructiveCryptography/InterfaceGame.lean#L63 +[Interface.liftMBO]: src/ConstructiveCryptography/InterfaceGame.lean#L66 +[Interface.Game.visible]: src/ConstructiveCryptography/InterfaceGame.lean#L84 [Interface.Game.ofPDG]: src/ConstructiveCryptography/PresentedGame.lean#L54 [Interface.Game.visible_ofPDG]: src/ConstructiveCryptography/PresentedGame.lean#L64 [Interface.Game.conditionallyEquivalent_ofPDG_iff]: src/ConstructiveCryptography/PresentedGame.lean#L74 @@ -1033,12 +1033,12 @@ agreeing with a map on a finite set $`S`$: there are $`\lvert Y \rvert^{\lvert X [Games.absorb]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L93 [DistinctionGames.absorb]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L148 [Games.absorb_comp]: src/ConstructiveCryptography/CryptographicAlgebra/Game.lean#L101 -[Interface.games]: src/ConstructiveCryptography/InterfaceGame.lean#L99 -[Interface.distinctionGames]: src/ConstructiveCryptography/InterfaceGame.lean#L149 -[Interface.dist_visible_le]: src/ConstructiveCryptography/InterfaceGame.lean#L210 -[Interface.winners]: src/ConstructiveCryptography/InterfaceGame.lean#L88 -[Interface.solvers]: src/ConstructiveCryptography/InterfaceGame.lean#L93 -[Interface.win_le]: src/ConstructiveCryptography/InterfaceGame.lean#L194 +[Interface.games]: src/ConstructiveCryptography/InterfaceGame.lean#L100 +[Interface.distinctionGames]: src/ConstructiveCryptography/InterfaceGame.lean#L150 +[Interface.dist_visible_le]: src/ConstructiveCryptography/InterfaceGame.lean#L211 +[Interface.winners]: src/ConstructiveCryptography/InterfaceGame.lean#L89 +[Interface.solvers]: src/ConstructiveCryptography/InterfaceGame.lean#L94 +[Interface.win_le]: src/ConstructiveCryptography/InterfaceGame.lean#L195 diff --git a/src/ConstructiveCryptography/InterfaceGame.lean b/src/ConstructiveCryptography/InterfaceGame.lean index c86732c..a949d72 100644 --- a/src/ConstructiveCryptography/InterfaceGame.lean +++ b/src/ConstructiveCryptography/InterfaceGame.lean @@ -46,6 +46,7 @@ probability that its MBO is set on fixed queries (CR18, Theorem 4.17), through namespace SystemAlgebra.Interface open CategoryTheory ConstructiveCryptography +open scoped NNReal /-- The interface of `A` with the MBO: its replies carry the MBO. -/ abbrev withMBO (A : Interface) : Interface where @@ -208,9 +209,9 @@ Theorem 4.17): a game on an interface conditionally equivalent to a resource `T` unset with probability at least `1 - ε` on the queries of each transcript of `T`, has its visible resource within `ε` of `T`. -/ theorem dist_visible_le {A : Interface} {G : Game A} {T : Resource A} - (hc : DistinctionGames.ConditionallyEquivalent G T) {ε : ℝ} + (hc : DistinctionGames.ConditionallyEquivalent G T) {ε : ℝ≥0} (hε : ∀ h, T.1 h ≠ 0 → 1 - ε ≤ G.1.1.unsetProbability (h.map Prod.fst)) : - CryptographicAlgebra.distance (DistinctionGames.visible G) T ≤ ENNReal.ofReal ε := by + CryptographicAlgebra.distance (DistinctionGames.visible G) T ≤ ε := by -- The distance of `CompatiblePseudoMetric` (its field `fibreMetric`) on interfaces is the -- systems-level transcript distance of the random systems. rw [cc_distance_eq] diff --git a/src/ConstructiveCryptography/PresentedGame.lean b/src/ConstructiveCryptography/PresentedGame.lean index 83987c5..2624c8e 100644 --- a/src/ConstructiveCryptography/PresentedGame.lean +++ b/src/ConstructiveCryptography/PresentedGame.lean @@ -40,7 +40,7 @@ the ideal answers. namespace SystemAlgebra open Probability ConstructiveCryptography -open scoped SystemAlgebra +open scoped SystemAlgebra NNReal namespace Interface @@ -88,9 +88,9 @@ every admitted query sequence, then `R` and `S` are at most `ε` apart. -/ theorem game_dist_le {A : Interface} {G : PDG (Σ i, A.X i) (Σ i, A.Y i) A.inputDomain} {hG : G.isProbDist} {R S : Resource A} (visible : R.1 = PDS.behavior G.underlying (PDG.underlying_probability hG)) - (equiv : Game.ofPDG G hG visible |≡ S) {ε : ℝ} + (equiv : Game.ofPDG G hG visible |≡ S) {ε : ℝ≥0} (hbad : ∀ xs, xs = [] ∨ A.domain xs → G.badProbability xs ≤ ε) : - Δ R S ≤ ENNReal.ofReal ε := by + Δ R S ≤ ε := by -- Δ(R, S) = Δ((ofPDG G)⁻, S) (`R` is the visible resource of the presented game) -- ≤ ε (`ofPDG G |≡ S`, MBO unset with probability ≥ 1 - ε) -- @@ -220,9 +220,9 @@ theorem game_dist_ofSingleFunction_le {I K X Y : Type} {P : Distribution K} [Distribution.IsProbability P] {f : K → X → Y} {bad : K → MC X} {R S : Resource ⟨I, fun _ => X, fun _ => Y, D, hD, bound, hb⟩} (equiv : Game.ofSingleFunction D hD bound hb P f bad |≡ S) - (visible : R = Resource.sample P (fun k => Resource.ofFunction (fun _ => f k))) {ε : ℝ} + (visible : R = Resource.sample P (fun k => Resource.ofFunction (fun _ => f k))) {ε : ℝ≥0} (hbad : ∀ xs, xs = [] ∨ D xs → P.mass (fun k => (bad k).1 (xs.map Sigma.snd)) ≤ ε) : - Δ R S ≤ ENNReal.ofReal ε := by + Δ R S ≤ ε := by -- `R` is the resource sampling the function. subst visible -- The distance bound for a presented game: `R` is presented by the visible systems of the diff --git a/src/Examples/AuthenticatedEncryption/Collision.lean b/src/Examples/AuthenticatedEncryption/Collision.lean index d22492e..487b4a1 100644 --- a/src/Examples/AuthenticatedEncryption/Collision.lean +++ b/src/Examples/AuthenticatedEncryption/Collision.lean @@ -30,7 +30,7 @@ replacement message, in either order. open SystemAlgebra SystemAlgebra.DSL SystemAlgebra.Interface Probability open Commons -open scoped SystemAlgebra +open scoped SystemAlgebra NNReal namespace AuthenticatedEncryption @@ -538,7 +538,7 @@ theorem collisionGame_badProbability_le (xs : List (Σ i, (AE.perPort M C q).X i theorem hybrid_ideal_distance_le : Δ (Hybrid scheme q) (AE.Ideal.perPort M C (budget := q) • Encryption.Real.perPort scheme : Interface.Resource (AE.perPort M C q)) ≤ - ENNReal.ofReal ((q .enc : ℝ) ^ 2 / Fintype.card M) := + ((q .enc) ^ 2 / Fintype.card M : ℝ≥0) := -- The distinguisher D on the left queries either system at the ports `enc` (sends `m`, -- receives `c`) and `dec` (sends `c`, receives `m` or ⊥), at most `q p` times at port `p`; -- replies return along the same wires. @@ -561,7 +561,7 @@ theorem hybrid_ideal_distance_le : -- Δ(Hybrid, ρ^ae(E_k)) ≤ sup_xs Pr[collision on xs] (game_dist_le; xs empty or admitted) -- ≤ q_e² / |M| (collisionGame_badProbability_le) game_dist_le (hybrid_visible scheme q) (collisionGame_conditionallyEquivalent scheme q) - (collisionGame_badProbability_le scheme q) + fun xs hxs => by push_cast; exact collisionGame_badProbability_le scheme q xs hxs end Game diff --git a/src/Examples/AuthenticatedEncryption/Security.lean b/src/Examples/AuthenticatedEncryption/Security.lean index 28542f8..72e03dd 100644 --- a/src/Examples/AuthenticatedEncryption/Security.lean +++ b/src/Examples/AuthenticatedEncryption/Security.lean @@ -36,7 +36,7 @@ open CategoryTheory open Commons open ConstructiveCryptography ConstructiveCryptography.CryptographicAlgebra open SystemAlgebra SystemAlgebra.Interface -open scoped SystemAlgebra +open scoped SystemAlgebra NNReal namespace AuthenticatedEncryption @@ -60,7 +60,7 @@ theorem ae_of_ind_cca_int_ptxt [AdmissibleDistinguishers] AE.Secure scheme fun D => εptxt D + εcca (absorb ρ^ptxt D) + εptxt (absorb (ρ^ptxt ≫ ρ^cca) D) + εcca (absorb (ρ^ptxt ≫ ρ^cca ≫ ρ^ptxt) D) + - ENNReal.ofReal ((q .enc : ℝ) ^ 2 / Fintype.card M) := by + ((q .enc) ^ 2 / Fintype.card M : ℝ≥0) := by cc_calc mixed (distinguisherAdvantage AdmissibleDistinguishers.admissible) using (fun D _ R S => distinguisherAdvantage_le_distance _ D R S) ⟦E_k, D_k⟧ ≃[εptxt] ρ^ptxt • ⟦E_k, D_k⟧ := ptxt @@ -71,7 +71,7 @@ theorem ae_of_ind_cca_int_ptxt [AdmissibleDistinguishers] _ ≃[εcca ∘ absorb (ρ^ptxt ≫ ρ^cca ≫ ρ^ptxt)] ρ^ptxt • ρ^cca • ρ^ptxt • ρ^cca • ⟦E_k, D_k⟧ := AdmissibleDistinguishers.substitutesWithin_context (ρ^ptxt ≫ ρ^cca ≫ ρ^ptxt) cca - _ ≈[ENNReal.ofReal ((q .enc : ℝ) ^ 2 / Fintype.card M)] ⟦E$_k, D^⊥⟧ := + _ ≈[((q .enc) ^ 2 / Fintype.card M : ℝ≥0)] ⟦E$_k, D^⊥⟧ := hybrid_ideal_distance_le scheme q /-- The two assumptions of the implication. -/ @@ -124,7 +124,7 @@ theorem real_ideal_distance_le : Δ ⟦E_k, D_k⟧ ⟦E$_k, D^⊥⟧ ≤ Δ ⟦E_k, D_k⟧ (ρ^ptxt • ⟦E_k, D_k⟧) + Δ ⟦E_k, D_k⟧ (ρ^cca • ⟦E_k, D_k⟧) + Δ ⟦E_k, D_k⟧ (ρ^ptxt • ⟦E_k, D_k⟧) + Δ ⟦E_k, D_k⟧ (ρ^cca • ⟦E_k, D_k⟧) + - ENNReal.ofReal ((q .enc : ℝ) ^ 2 / Fintype.card M) := by + ((q .enc) ^ 2 / Fintype.card M : ℝ≥0) := by cc_calc statistical ⟦E_k, D_k⟧ ≈[Δ ⟦E_k, D_k⟧ (ρ^ptxt • ⟦E_k, D_k⟧)] ρ^ptxt • ⟦E_k, D_k⟧ := le_rfl _ ≈[Δ ⟦E_k, D_k⟧ (ρ^cca • ⟦E_k, D_k⟧)] ρ^ptxt • ρ^cca • ⟦E_k, D_k⟧ := @@ -134,7 +134,7 @@ theorem real_ideal_distance_le : _ ≈[Δ ⟦E_k, D_k⟧ (ρ^cca • ⟦E_k, D_k⟧)] ρ^ptxt • ρ^cca • ρ^ptxt • ρ^cca • ⟦E_k, D_k⟧ := ((distance_attach_le _ _ _).trans (distance_attach_le _ _ _)).trans (distance_attach_le _ _ _) - _ ≈[ENNReal.ofReal ((q .enc : ℝ) ^ 2 / Fintype.card M)] ⟦E$_k, D^⊥⟧ := + _ ≈[((q .enc) ^ 2 / Fintype.card M : ℝ≥0)] ⟦E$_k, D^⊥⟧ := hybrid_ideal_distance_le scheme q end AuthenticatedEncryption diff --git a/src/RandomSystems/Distance/Decision.lean b/src/RandomSystems/Distance/Decision.lean index 0935817..7953d54 100644 --- a/src/RandomSystems/Distance/Decision.lean +++ b/src/RandomSystems/Distance/Decision.lean @@ -23,6 +23,8 @@ a sample. ## Main results +* `RandomSystem.transcriptDistance_le`: a bound in `ℝ≥0` on the transcript laws under every + environment bounds the transcript distance * `RandomSystem.decisionProbability_envProbe`: an environment followed by an event test decides `1` with the probability of the event * `RandomSystem.decisionProbability_gap_le`: decision gaps are at most the transcript @@ -36,6 +38,7 @@ a sample. namespace SystemAlgebra open Classical Probability +open scoped NNReal theorem Cons.queries_eq {A B : Type} {e : List B →. A} {h : List (A × B)} (hc : Cons e h) : h.map Prod.fst = qsOf e (h.map Prod.snd) := by @@ -232,11 +235,23 @@ theorem statDist_le_transcriptDistance {E : DDE (Σ i, X i) (Σ i, Y i)} {n : ENNReal.ofReal (statDist (R.sLaw E.1 n) (S.sLaw E.1 n)) ≤ R.transcriptDistance S := le_iSup_of_le E (le_iSup_of_le n (le_iSup_of_le hn (le_iSup_of_le hc le_rfl))) +/-- **A bound on the transcript laws bounds the transcript distance**: if under every compatible +query-bounded environment the statistical distance of the transcript laws is at most `b`, the +transcript distance is at most `b`. -/ +theorem transcriptDistance_le {R S : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟} {b : ℝ≥0} + (h : ∀ (E : DDE (Σ i, X i) (Σ i, Y i)) (n : ℕ), QueryBounded n E → 𝒟.Compatible E → + statDist (R.sLaw E.1 n) (S.sLaw E.1 n) ≤ b) : + R.transcriptDistance S ≤ b := + iSup_le fun E => iSup_le fun n => iSup_le fun hn => iSup_le fun hc => by + -- The real bound `b` read in `ℝ≥0∞` is `b` itself. + rw [← ENNReal.ofReal_coe_nnreal] + exact ENNReal.ofReal_le_ofReal (h E n hn hc) + theorem transcriptDistance_le_one {R S : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟} (hR : R.RepliesAtQueriedInterface) (hS : S.RepliesAtQueriedInterface) : R.transcriptDistance S ≤ 1 := by - refine iSup_le fun E => iSup_le fun n => iSup_le fun _ => iSup_le fun hc => ?_ - apply ENNReal.ofReal_le_one.mpr + rw [← ENNReal.coe_one] + refine transcriptDistance_le fun E n _ hc => ?_ have hr := R.sLaw_isProbDist (hc R hR) n have hs := S.sLaw_isProbDist (hc S hS) n exact (statDist_le_weight hr.1 hs.1).trans_eq hr.2 diff --git a/src/RandomSystems/Distance/Distinguisher.lean b/src/RandomSystems/Distance/Distinguisher.lean index d8ca084..07e819b 100644 --- a/src/RandomSystems/Distance/Distinguisher.lean +++ b/src/RandomSystems/Distance/Distinguisher.lean @@ -46,6 +46,7 @@ serial composition is absorbing its PDCs in turn. namespace SystemAlgebra open Classical Probability +open scoped NNReal section Attachment @@ -178,6 +179,19 @@ theorem RandomSystem.transcriptDistance_eq_iSup {𝒟 : Domain (Σ i, X i) (Σ i _ = R.transcriptDistance S := ENNReal.ofReal_toReal (ne_top_of_le_ne_top ENNReal.one_ne_top (transcriptDistance_le_one hR hS)) +/-- **A bound on every advantage bounds the transcript distance**: if every probabilistic +distinguisher's advantage is at most `b`, the transcript distance is at most `b`. -/ +theorem RandomSystem.transcriptDistance_le_of_advantage_le {𝒟 : Domain (Σ i, X i) (Σ i, Y i)} + {R S : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟} + (hR : R.RepliesAtQueriedInterface) (hS : S.RepliesAtQueriedInterface) {b : ℝ≥0} + (h : ∀ P : 𝒟.Distinguisher, |P.probability R - P.probability S| ≤ b) : + R.transcriptDistance S ≤ b := by + -- The transcript distance is the largest advantage; each is at most `b`. + rw [RandomSystem.transcriptDistance_eq_iSup hR hS] + refine iSup_le fun P => ?_ + rw [Domain.Distinguisher.advantage, ← ENNReal.ofReal_coe_nnreal] + exact ENNReal.ofReal_le_ofReal (h P) + /-- The advantage of a probabilistic distinguisher is at most the transcript distance. -/ theorem Domain.Distinguisher.advantage_le_transcriptDistance {𝒟 : Domain (Σ i, X i) (Σ i, Y i)} (P : 𝒟.Distinguisher) {R S : RandomSystem (Σ i, X i) (Σ i, Y i) 𝒟} diff --git a/src/RandomSystems/Game/MBO.lean b/src/RandomSystems/Game/MBO.lean index e573754..ce27923 100644 --- a/src/RandomSystems/Game/MBO.lean +++ b/src/RandomSystems/Game/MBO.lean @@ -46,6 +46,7 @@ visible system `S⁻`), Definition 4.19 (conditional equivalence), Lemma 4.16 an namespace SystemAlgebra open Probability +open scoped NNReal /-! ## Replies with the MBO -/ @@ -863,20 +864,19 @@ theorem RandomSystem.transcriptDistance_visible_le_of_unsetProbability {G : RandomSystem (Σ i, X i) (Σ i, withMBO Y i) (Domain.ofInputs E m hE)} {T : RandomSystem (Σ i, X i) (Σ i, Y i) (Domain.ofInputs E m hE)} (hG : G.RepliesAtQueriedInterface) (hT : T.RepliesAtQueriedInterface) - (hm : G.MonotoneMBO) (hc : G.ConditionallyEquivalent T) {ε : ℝ} + (hm : G.MonotoneMBO) (hc : G.ConditionallyEquivalent T) {ε : ℝ≥0} (hε : ∀ h, T h ≠ 0 → 1 - ε ≤ G.unsetProbability (h.map Prod.fst)) : - G.visible.transcriptDistance T ≤ ENNReal.ofReal ε := by + G.visible.transcriptDistance T ≤ ε := by -- Δ(G⁻, T) = sup_P |p_P(G⁻) − p_P(T)| (transcriptDistance_eq_iSup) -- ≤ sup_P Γ_P(G) (advantage_le_winProbability) -- ≤ ε (winProbability_le_of_unsetProbability) -- The hypothesis bounds the MBO only on fixed query sequences, yet the bound holds for -- every adaptive distinguisher. - -- The transcript distance is the largest advantage of a probabilistic distinguisher. - rw [RandomSystem.transcriptDistance_eq_iSup hG.visible hT] - -- Lemma 4.16 bounds each advantage by winning, which the unset MBO bounds. - exact iSup_le fun P => ENNReal.ofReal_le_ofReal - ((P.advantage_le_winProbability hG hT hm hc).trans - (P.winProbability_le_of_unsetProbability hG hT hm hc hε)) + -- The transcript distance is the largest advantage of a probabilistic distinguisher; Lemma + -- 4.16 bounds each advantage by winning, which the unset MBO bounds. + exact RandomSystem.transcriptDistance_le_of_advantage_le hG.visible hT fun P => + (P.advantage_le_winProbability hG hT hm hc).trans + (P.winProbability_le_of_unsetProbability hG hT hm hc hε) end Winning diff --git a/src/Tests/AuthenticatedEncryption.lean b/src/Tests/AuthenticatedEncryption.lean index a518389..2189038 100644 --- a/src/Tests/AuthenticatedEncryption.lean +++ b/src/Tests/AuthenticatedEncryption.lean @@ -17,6 +17,7 @@ open ConstructiveCryptography ConstructiveCryptography.CryptographicAlgebra namespace AuthenticatedEncryptionTests open AuthenticatedEncryption +open scoped NNReal /-- The one-time pad on bits: a uniform key, `Enc_k(m) = k ⊕ m` and `Dec_k(c) = k ⊕ c`. -/ noncomputable def oneTimePad : SymmetricEncryption Bool Bool Bool where @@ -28,7 +29,7 @@ noncomputable def oneTimePad : SymmetricEncryption Bool Bool Bool where theorem oneTimePad_hybrid_ideal (q : AE.Port → ℕ) : Δ (Hybrid oneTimePad q) (AE.Ideal.perPort Bool Bool (budget := q) • Encryption.Real.perPort oneTimePad : Interface.Resource (AE.perPort Bool Bool q)) ≤ - ENNReal.ofReal ((q .enc : ℝ) ^ 2 / 2) := by + ((q .enc) ^ 2 / 2 : ℝ≥0) := by simpa using hybrid_ideal_distance_le oneTimePad q /-- The collision step on the one-time pad, through the games layer: every solver's advantage is