Leakage Judgments for Side-Channel Reasoning

This file defines three leakage judgments of increasing strength, enabling formal side-channel reasoning within the VCVio framework. All three operate on observed computations (outputs of runObs) that produce a result paired with an accumulated trace.

Main Definitions

• TraceNoninterference: exact trace equality in every coupling (pRHL indicator). Two observed computations satisfy this when their trace components always match, regardless of the result. This is the VCVio analogue of constant-time execution.
• ProbLeakFree: distributional trace independence. The trace distribution does not depend on secrets.
• LeakageBound: approximate trace independence via total variation distance. The trace distributions differ by at most ε.

Main Results

• traceNoninterference_implies_probLeakFree: exact trace equality implies distributional independence.
• probLeakFree_iff_leakageBound_zero: ProbLeakFree is the ε = 0 case of LeakageBound.
• leakageBound_triangle: transitivity for game-hopping arguments.

TraceNoninterference

def OracleComp.Leakage.TraceNoninterference {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] (oa₁ : OracleComp spec₁ (α × ω)) (oa₂ : OracleComp spec₂ (β × ω)) : Prop

Exact trace noninterference: two observed computations produce equal trace components in every coupled output. This is the strongest leakage judgment, corresponding to constant-time execution for deterministic channels.

Defined via RelTriple' (the pRHL indicator pattern from QuantitativeDefs.lean).

ProbLeakFree

def OracleComp.Leakage.ProbLeakFree {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] (oa₁ : OracleComp spec₁ (α × ω)) (oa₂ : OracleComp spec₂ (β × ω)) : Prop

Distributional trace independence: the trace distributions are identical regardless of which computation produced them. This captures the property that an adversary observing only the trace cannot distinguish between the two computations.

The comparison is made at the SPMF level via evalDist, allowing computations over different oracle specs to be compared.

LeakageBound

def OracleComp.Leakage.LeakageBound {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] (ε : ℝ) (oa₁ : OracleComp spec₁ (α × ω)) (oa₂ : OracleComp spec₂ (β × ω)) : Prop

Approximate trace independence: the trace distributions differ by at most ε in total variation distance. This enables game-hopping arguments where each hop introduces a small leakage discrepancy.

Bridge Lemmas

theorem OracleComp.Leakage.traceNoninterference_implies_probLeakFree {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : TraceNoninterference oa₁ oa₂) : ProbLeakFree oa₁ oa₂

Exact trace noninterference implies distributional trace independence: if traces always match in every coupling, their distributions must be equal.

theorem OracleComp.Leakage.probLeakFree_iff_leakageBound_zero {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} : ProbLeakFree oa₁ oa₂ ↔ LeakageBound 0 oa₁ oa₂

ProbLeakFree is equivalent to LeakageBound 0.

theorem OracleComp.Leakage.leakageBound_triangle {ι₁ ι₂ ι₃ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {spec₃ : OracleSpec ι₃} {α β γ ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] [spec₃.Fintype] [spec₃.Inhabited] {ε₁ ε₂ : ℝ} {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} {oa₃ : OracleComp spec₃ (γ × ω)} (h₁₂ : LeakageBound ε₁ oa₁ oa₂) (h₂₃ : LeakageBound ε₂ oa₂ oa₃) : LeakageBound (ε₁ + ε₂) oa₁ oa₃

Transitivity of LeakageBound for game-hopping: if the first pair of computations has leakage at most ε₁ and the second pair at most ε₂, then the outer pair has leakage at most ε₁ + ε₂.

@[simp]

theorem OracleComp.Leakage.probLeakFree_refl {ι₁ : Type u} {spec₁ : OracleSpec ι₁} {α ω : Type} [spec₁.Fintype] [spec₁.Inhabited] (oa : OracleComp spec₁ (α × ω)) : ProbLeakFree oa oa

ProbLeakFree is reflexive.

theorem OracleComp.Leakage.probLeakFree_symm {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : ProbLeakFree oa₁ oa₂) : ProbLeakFree oa₂ oa₁

ProbLeakFree is symmetric.

theorem OracleComp.Leakage.probLeakFree_of_leakageBound_zero {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : LeakageBound 0 oa₁ oa₂) : ProbLeakFree oa₁ oa₂

LeakageBound with ε = 0 implies ProbLeakFree.

@[simp]

theorem OracleComp.Leakage.leakageBound_refl {ι₁ : Type u} {spec₁ : OracleSpec ι₁} {α ω : Type} [spec₁.Fintype] [spec₁.Inhabited] (oa : OracleComp spec₁ (α × ω)) : LeakageBound 0 oa oa

LeakageBound is reflexive with bound 0.

theorem OracleComp.Leakage.leakageBound_symm {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {ε : ℝ} {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : LeakageBound ε oa₁ oa₂) : LeakageBound ε oa₂ oa₁

LeakageBound is symmetric.

theorem OracleComp.Leakage.leakageBound_mono {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {ε₁ ε₂ : ℝ} (hε : ε₁ ≤ ε₂) {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : LeakageBound ε₁ oa₁ oa₂) : LeakageBound ε₂ oa₁ oa₂

Monotonicity: a smaller leakage bound implies a larger one.

Compositional Lemmas: Map

theorem OracleComp.Leakage.probLeakFree_map_fst {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β γ ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : ProbLeakFree oa₁ oa₂) {δ : Type} (f₁ : α → γ) (f₂ : β → δ) : ProbLeakFree (Prod.map f₁ id <$> oa₁) (Prod.map f₂ id <$> oa₂)

Mapping the result component preserves distributional trace independence.

theorem OracleComp.Leakage.leakageBound_map_fst {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β γ ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {ε : ℝ} {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : LeakageBound ε oa₁ oa₂) {δ : Type} (f₁ : α → γ) (f₂ : β → δ) : LeakageBound ε (Prod.map f₁ id <$> oa₁) (Prod.map f₂ id <$> oa₂)

Mapping the result component preserves approximate trace independence.

theorem OracleComp.Leakage.traceNoninterference_map_fst {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β γ ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : TraceNoninterference oa₁ oa₂) {δ : Type} (f₁ : α → γ) (f₂ : β → δ) : TraceNoninterference (Prod.map f₁ id <$> oa₁) (Prod.map f₂ id <$> oa₂)

Mapping the result component preserves trace noninterference.

theorem OracleComp.Leakage.probLeakFree_map_snd {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : ProbLeakFree oa₁ oa₂) {ω' : Type} (g : ω → ω') : ProbLeakFree (Prod.map id g <$> oa₁) (Prod.map id g <$> oa₂)

Mapping the trace component with the same function preserves distributional trace independence.

theorem OracleComp.Leakage.leakageBound_map_snd {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {ε : ℝ} {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : LeakageBound ε oa₁ oa₂) {ω' : Type} (g : ω → ω') : LeakageBound ε (Prod.map id g <$> oa₁) (Prod.map id g <$> oa₂)

Mapping the trace component with the same function preserves approximate trace independence.

theorem OracleComp.Leakage.traceNoninterference_map_snd {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : TraceNoninterference oa₁ oa₂) {ω' : Type} (g : ω → ω') : TraceNoninterference (Prod.map id g <$> oa₁) (Prod.map id g <$> oa₂)

Mapping the trace component with the same function preserves trace noninterference.

Compositional Lemmas: Bind

theorem OracleComp.Leakage.traceNoninterference_bind {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β γ ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {δ ω' : Type} {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} {f₁ : α × ω → OracleComp spec₁ (γ × ω')} {f₂ : β × ω → OracleComp spec₂ (δ × ω')} (h : TraceNoninterference oa₁ oa₂) (hf : ∀ (a : α) (b : β) (w : ω), TraceNoninterference (f₁ (a, w)) (f₂ (b, w))) : TraceNoninterference (oa₁ >>= f₁) (oa₂ >>= f₂)

Trace noninterference is preserved by sequential composition (bind). The continuations may depend on both the result and the trace, but whenever the traces match, the continuations must themselves be trace noninterfering.

theorem OracleComp.Leakage.probLeakFree_bind_of_trace_only {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β γ ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {δ ω' : Type} {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : ProbLeakFree oa₁ oa₂) {f : ω → OracleComp spec₁ (γ × ω')} {g : ω → OracleComp spec₂ (δ × ω')} (hfg : ∀ (w : ω), ProbLeakFree (f w) (g w)) : ProbLeakFree (do let z ← oa₁ f z.2) do let z ← oa₂ g z.2

Distributional trace independence is preserved by bind when the continuation depends only on the trace (second component).

theorem OracleComp.Leakage.leakageBound_bind_of_trace_only {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β γ ω : Type} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {ε : ℝ} {δ ω' : Type} {oa₁ : OracleComp spec₁ (α × ω)} {oa₂ : OracleComp spec₂ (β × ω)} (h : LeakageBound ε oa₁ oa₂) {f : ω → OracleComp spec₁ (γ × ω')} {g : ω → OracleComp spec₂ (δ × ω')} (hfg : ∀ (w : ω), ProbLeakFree (f w) (g w)) : LeakageBound ε (do let z ← oa₁ f z.2) do let z ← oa₂ g z.2

Approximate trace independence is preserved by bind when the continuation depends only on the trace and produces identical trace distributions.