Cost-Aware Security Reductions

This file packages the cost-transform part of a reduction theorem.

ReductionWithCost records:

• a reduction reduce : Adv → Adv',
• a monotone transform on asymptotic cost bounds,
• a proof that the reduced adversary's cost profile is bounded by that transform.

This is intentionally abstract in both the choice of efficiency class and the shape of the cost objects being transformed. Users can instantiate the resulting meta-theorems with scalar costs, structured resource profiles, interface-profile bounds, or any other preordered asymptotic notion that is closed under the transform carried by the reduction.

def SecurityGame.EfficientFor {Adv : Type u_1} {σ : Type u_4} [Preorder σ] (cost : Adv → ℕ → σ) (isEff : (ℕ → σ) → Prop) : Adv → Prop

An adversary is efficient for a profile class isEff if its concrete cost profile is bounded by some admissible asymptotic profile in that class.

structure SecurityGame.CostClassMap {σ : Type u_4} {σ' : Type u_5} (isEff : (ℕ → σ) → Prop) (isEff' : (ℕ → σ') → Prop) (transform : ℕ → σ → σ') : Prop

A transform on asymptotic cost bounds maps a source efficiency class into a target one.

• map_mem (bound : ℕ → σ) : isEff bound → isEff' fun (n : ℕ) => transform n (bound n)

structure SecurityGame.ReductionWithCost {Adv : Type u_1} {Adv' : Type u_2} {σ : Type u_4} {σ' : Type u_5} [Preorder σ] [Preorder σ'] (cost : Adv → ℕ → σ) (cost' : Adv' → ℕ → σ') : Type (max (max (max u_1 u_2) u_4) u_5)

A reduction together with an explicit transform on asymptotic cost bounds.

• reduce : Adv → Adv'
• transform : ℕ → σ → σ'
• monotone_transform (n : ℕ) : Monotone (self.transform n)
• cost_bound (A : Adv) (n : ℕ) : cost' (self.reduce A) n ≤ self.transform n (cost A n)

theorem SecurityGame.ReductionWithCost.efficientFor_image {Adv : Type u_1} {Adv' : Type u_2} {σ : Type u_4} {σ' : Type u_5} [Preorder σ] [Preorder σ'] {cost : Adv → ℕ → σ} {cost' : Adv' → ℕ → σ'} (R : ReductionWithCost cost cost') {isEff : (ℕ → σ) → Prop} {isEff' : (ℕ → σ') → Prop} {A : Adv} (hA : EfficientFor cost isEff A) (hmap : CostClassMap isEff isEff' R.transform) : EfficientFor cost' isEff' (R.reduce A)

The cost transform of a reduction sends admissible profile bounds on the source adversary to admissible profile bounds on the reduced adversary.

def SecurityGame.ReductionWithCost.comp {Adv : Type u_1} {Adv' : Type u_2} {Adv'' : Type u_3} {σ : Type u_4} {σ' : Type u_5} {σ'' : Type u_6} [Preorder σ] [Preorder σ'] [Preorder σ''] {cost : Adv → ℕ → σ} {cost' : Adv' → ℕ → σ'} {cost'' : Adv'' → ℕ → σ''} (R₁ : ReductionWithCost cost cost') (R₂ : ReductionWithCost cost' cost'') : ReductionWithCost cost cost''

Cost-aware reductions compose by composing both the adversary map and the profile transform.

theorem SecurityGame.secureAgainst_of_reduction_withCost {Adv : Type u_1} {Adv' : Type u_2} {σ : Type u_4} {σ' : Type u_5} [Preorder σ] [Preorder σ'] {g : SecurityGame Adv} {g' : SecurityGame Adv'} {cost : Adv → ℕ → σ} {cost' : Adv' → ℕ → σ'} {isEff : (ℕ → σ) → Prop} {isEff' : (ℕ → σ') → Prop} (R : ReductionWithCost cost cost') (hadv : ∀ (A : Adv) (n : ℕ), g.advantage A n ≤ g'.advantage (R.reduce A) n) (hmap : CostClassMap isEff isEff' R.transform) (hsecure : g'.secureAgainst (EfficientFor cost' isEff')) : g.secureAgainst (EfficientFor cost isEff)

Cost-aware security reduction.

If a reduction preserves advantage, and if the target efficiency class is closed under the reduction's cost transform, then security of the target game implies security of the source game for adversaries whose cost profiles lie in the source class.