Cryptographic Advantage

This file defines the advantage of an adversary in distinguishing games.

noncomputable def CatCrypt.Crypto.prTrue (G : Core.SPComp Bool) (h₀ : Core.Heap) : ENNReal

Probability that a computation returns true, starting from an initial heap. This sums over all final heaps.

Equations

• CatCrypt.Crypto.prTrue G h₀ = ∑' (h : CatCrypt.Core.Heap), (G h₀) (some (true, h))

noncomputable def CatCrypt.Crypto.Advantage (G₀ G₁ : Core.SPComp Bool) : ENNReal

Advantage: distinguishing probability between two games, measured as the absolute difference of the probabilities of returning true.

Scope: the initial heap is fixed to Heap.empty. This is the empty-heap distinguishing probability, not the supremum over all initial heaps; the stronger all-heap notion is SDist.sdist. The two are reconciled by the bridge lemmas sdist_isPure_le / sdist_oracleGame_le (SDist.lean), which bound this empty-heap advantage by the all-heap statistical distance. Use Advantage for empty-heap game hops; reach for sdist when the adversary may choose the starting state.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCrypt.Crypto.AdvantageA {α : Type u_1} (G₀ G₁ : Core.SPComp α) (A : α → Core.SPComp Bool) : ENNReal

Advantage with explicit adversary

Equations

• CatCrypt.Crypto.AdvantageA G₀ G₁ A = CatCrypt.Crypto.Advantage (G₀.bind A) (G₁.bind A)

Key Lemmas

theorem CatCrypt.Crypto.advantage_triangle (G₀ G₁ G₂ : Core.SPComp Bool) : Advantage G₀ G₂ ≤ Advantage G₀ G₁ + Advantage G₁ G₂

Triangle inequality for advantage |Pr[G₀] - Pr[G₂]| ≤ |Pr[G₀] - Pr[G₁]| + |Pr[G₁] - Pr[G₂]|

theorem CatCrypt.Crypto.advantage_zero_of_rHoare {α : Type u_1} (G₀ G₁ : Core.SPComp α) (h : Relational.rHoare Relational.eqPre G₀ G₁ Relational.eqPost) (A : α → Core.SPComp Bool) : AdvantageA G₀ G₁ A = 0

Perfect indistinguishability from pRHL equality. If G₀ and G₁ produce equal outputs when started from equal heaps, no adversary can distinguish them.

theorem CatCrypt.Crypto.advantage_zero_of_inv {α : Type u_1} (I : Relational.RPre) (G₀ G₁ : Core.SPComp α) (hI : I Core.Heap.empty Core.Heap.empty) (h : Relational.rHoare I G₀ G₁ fun (a₁ : α) (h₁ : Core.Heap) (a₂ : α) (h₂ : Core.Heap) => a₁ = a₂ ∧ I h₁ h₂) (A : α → Core.SPComp Bool) (hA_respects : ∀ (a : α) (h₁ h₂ : Core.Heap), I h₁ h₂ → A a h₁ = A a h₂) : AdvantageA G₀ G₁ A = 0

Zero advantage from invariant-preserving judgment with state separation.

If G₀ and G₁ preserve an invariant I and produce equal values, they are indistinguishable for any adversary that respects I.

Key Hypothesis: hA_respects states that when two heaps are I-related, the adversary produces the same distribution. This captures the essence of state separation: the adversary cannot observe differences in protocol-internal state that is encapsulated by I.

In CatCrypt/Rocq, this is enforced structurally via package validity:

• A's locations LA are disjoint from protocol locations L
• I only constrains locations in L
• Therefore A cannot observe I-related differences (A only sees LA)

For the basic case where I = eqPre (heap equality), use advantage_zero_of_rHoare.

Symmetry and Reflexivity

@[simp]

theorem CatCrypt.Crypto.Advantage_sym (G₀ G₁ : Core.SPComp Bool) : Advantage G₀ G₁ = Advantage G₁ G₀

Advantage is symmetric: swapping games doesn't change the advantage.

@[simp]

theorem CatCrypt.Crypto.Advantage_self (G : Core.SPComp Bool) : Advantage G G = 0

Self-advantage is zero: no adversary can distinguish a game from itself.

Utility Lemmas for Advantage Bounds

theorem CatCrypt.Crypto.prTrue_le_one (G : Core.SPComp Bool) (h₀ : Core.Heap) : prTrue G h₀ ≤ 1

prTrue is at most 1 (probability bound).

theorem CatCrypt.Crypto.prTrue_bind_sample_Bool (A : Bool → Core.SPComp Bool) (h₀ : Core.Heap) : prTrue ((Core.SPComp.sample Bool).bind A) h₀ = 2⁻¹ * prTrue (A true) h₀ + 2⁻¹ * prTrue (A false) h₀

prTrue of sampling Bool then applying A decomposes as weighted sum.

theorem CatCrypt.Crypto.advantage_sample_vs_pure_false (A : Bool → Core.SPComp Bool) : AdvantageA (Core.SPComp.sample Bool) (Core.SPComp.pure false) A ≤ 2⁻¹

Advantage of sampling uniform Bool vs pure constant is at most 1/2.

General Sampling Lemmas

theorem CatCrypt.Crypto.prTrue_bind_sample {α : Type u_1} [Fintype α] [Nonempty α] (F : α → Core.SPComp Bool) (h₀ : Core.Heap) : prTrue ((Core.SPComp.sample α).bind F) h₀ = ∑ x : α, (↑(Fintype.card α))⁻¹ * prTrue (F x) h₀

prTrue of sampling then applying F decomposes as weighted sum over the sampled type.

theorem CatCrypt.Crypto.advantageA_sample_bind {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] (f g : α → Core.SPComp β) (A : β → Core.SPComp Bool) (ε : ENNReal) (h : ∀ (x : α), AdvantageA (f x) (g x) A ≤ ε) : AdvantageA ((Core.SPComp.sample α).bind f) ((Core.SPComp.sample α).bind g) A ≤ ε

Advantage with uniform prefix sampling.

If two games differ only in their continuation after sampling, and the continuation advantage is bounded for all sampled values, then the overall advantage is bounded.

For finite types (like Word = Bool), this follows from the fact that sampling is a convex combination, and advantage respects convexity.

IsPure Prefix Factoring

theorem CatCrypt.Crypto.advantageA_isPure_bind {α : Type u_1} {β : Type u_2} (pfx : Core.SPComp α) (f g : α → Core.SPComp β) (A : β → Core.SPComp Bool) (ε : ENNReal) (hPure : pfx.IsPure) (h : ∀ (x : α), AdvantageA (f x) (g x) A ≤ ε) : AdvantageA (pfx.bind f) (pfx.bind g) A ≤ ε

Factoring out an IsPure prefix from advantage bounds.

If pfx is heap-independent and for every prefix value x, the advantage between f x and g x is bounded by ε, then the overall advantage is also bounded by ε.

This is the key lemma for mechanizing HKDF hybrid steps where the differing game depends on the prefix output (e.g., th_2 from keygens).