State-separating handlers: ε-indistinguishability #
QueryImpl.Stateful.IndistAt h₀ s₀ h₁ s₁ ε bounds the Boolean
distinguishing advantage between two stateful handlers from explicit initial
states.
ε-bounded indistinguishability of two stateful handlers from explicit initial states.
Instances For
theorem
QueryImpl.Stateful.IndistAt.refl
{ιₑ : Type uₑ}
{E : OracleSpec ιₑ}
{σ : Type}
(h : Stateful unifSpec E σ)
(s : σ)
:
h.IndistAt s h s 0
ε-monotonicity #
theorem
QueryImpl.Stateful.IndistAt.refl_le
{ιₑ : Type uₑ}
{E : OracleSpec ιₑ}
{σ : Type}
{ε : ℝ}
(h : Stateful unifSpec E σ)
(s : σ)
(hε : 0 ≤ ε)
:
h.IndistAt s h s ε
Bridge from DistEquiv #
theorem
QueryImpl.Stateful.IndistAt.distEquiv_left
{ιₑ : Type uₑ}
{E : OracleSpec ιₑ}
{σ σ₀ σ₁ : Type}
{h₀ : Stateful unifSpec E σ₀}
{s₀ : σ₀}
{h₀' : Stateful unifSpec E σ}
{s₀' : σ}
{h₁ : Stateful unifSpec E σ₁}
{s₁ : σ₁}
{ε : ℝ}
(h : h₀.DistEquiv s₀ h₀' s₀')
(hi : h₀'.IndistAt s₀' h₁ s₁ ε)
:
h₀.IndistAt s₀ h₁ s₁ ε
theorem
QueryImpl.Stateful.IndistAt.distEquiv_right
{ιₑ : Type uₑ}
{E : OracleSpec ιₑ}
{σ σ₀ σ₁ : Type}
{h₀ : Stateful unifSpec E σ₀}
{s₀ : σ₀}
{h₁ : Stateful unifSpec E σ₁}
{s₁ : σ₁}
{h₁' : Stateful unifSpec E σ}
{s₁' : σ}
{ε : ℝ}
(h : h₁.DistEquiv s₁ h₁' s₁')
(hi : h₀.IndistAt s₀ h₁ s₁ ε)
:
h₀.IndistAt s₀ h₁' s₁' ε
Bridge to advantage #
theorem
QueryImpl.Stateful.IndistAt.advantage_le
{ιₑ : Type uₑ}
{E : OracleSpec ιₑ}
{σ₀ σ₁ : Type}
{h₀ : Stateful unifSpec E σ₀}
{s₀ : σ₀}
{h₁ : Stateful unifSpec E σ₁}
{s₁ : σ₁}
{ε : ℝ}
(h : h₀.IndistAt s₀ h₁ s₁ ε)
(A : OracleComp E Bool)
:
theorem
QueryImpl.Stateful.IndistAt.of_advantage_le
{ιₑ : Type uₑ}
{E : OracleSpec ιₑ}
{σ₀ σ₁ : Type}
{h₀ : Stateful unifSpec E σ₀}
{s₀ : σ₀}
{h₁ : Stateful unifSpec E σ₁}
{s₁ : σ₁}
{ε : ℝ}
(h : ∀ (A : OracleComp E Bool), h₀.advantage s₀ h₁ s₁ A ≤ ε)
:
h₀.IndistAt s₀ h₁ s₁ ε
Hybrid and compositional bounds #
theorem
QueryImpl.Stateful.IndistAt.hybrid
{ιₑ : Type uₑ}
{E : OracleSpec ιₑ}
{n : ℕ}
{σ : ℕ → Type}
{ε : ℕ → ℝ}
(h : (i : ℕ) → Stateful unifSpec E (σ i))
(s : (i : ℕ) → σ i)
(hh : ∀ i ∈ Finset.range n, (h i).IndistAt (s i) (h (i + 1)) (s (i + 1)) (ε i))
:
(h 0).IndistAt (s 0) (h n) (s n) (∑ i ∈ Finset.range n, ε i)
theorem
QueryImpl.Stateful.IndistAt.link_inner_congr
{ιₑ : Type uₑ}
{E : OracleSpec ιₑ}
{σ₀ σ₁ : Type}
{ιₘ : Type uₘ}
{M : OracleSpec ιₘ}
{σ_P : Type}
(outer : Stateful M E σ_P)
(sP : σ_P)
{inner₀ : Stateful unifSpec M σ₀}
{s₀ : σ₀}
{inner₁ : Stateful unifSpec M σ₁}
{s₁ : σ₁}
{ε : ℝ}
(h : inner₀.IndistAt s₀ inner₁ s₁ ε)
: