Security Experiments

This file gives a basic way to represent security experiments, as an extension of OracleAlg. The definition is meant to be simple enough to give useful lemmas while still being able to represent most common use cases.

We also give a definition SecAdv α β of a security adversary with input α and output β, as just a computation bundled with a bound on the number of queries it makes.

The main definition is SecExp spec α β, which extends OracleAlg with three functions:

• inp_gen that chooses an input for the experiment of type α
• main that takes an input and computes a result of type β
• isValid that decides whether the experiment succeeded

noncomputable def ProbComp.advantage' (p : ProbComp Bool) : ℝ

noncomputable def ProbComp.advantage₂' (p q : ProbComp Bool) : ℝ

noncomputable def ProbComp.advantage (p : ProbComp Unit) : ℝ

The advantage of a game p, assumed to be a probabilistic computation ending with a guard statement, is the absolute difference between the probability of success and 1/2.

theorem ProbComp.advantage_eq_half_sub_probFailure (p : ProbComp Unit) : p.advantage = |1 / 2 - [⊥|p].toReal|

The advantage doesn't change if we replace ⊥ with = () (i.e. swap the probability of success and failure).

theorem ProbComp.advantage_eq_half_of_sub (p : ProbComp Unit) : p.advantage = 2⁻¹ * |[⊥|p].toReal - [=()|p].toReal|

The advantage of a probabilistic computation is half the absolute difference between the probabilities of success and failure.

noncomputable def ProbComp.advantage₂ (p q : ProbComp Unit) : ℝ

The advantage between two games p and q, modeled as probabilistic computations returning Unit, is the absolute difference between their probabilities of success.

@[simp]

theorem ProbComp.advantage₂_self (p : ProbComp Unit) : p.advantage₂ p = 0

The advantage between a game and itself is zero (i.e. it is reflexive).

theorem ProbComp.advantage₂_comm (p q : ProbComp Unit) : p.advantage₂ q = q.advantage₂ p

The advantage between two games is symmetric.

theorem ProbComp.advantage₂_eq_abs_sub_probFailure (p q : ProbComp Unit) : p.advantage₂ q = |[⊥|p].toReal - [⊥|q].toReal|

The advantage between two games is the same as the absolute difference between their probabilities of failure.

structure SecAdv {ι : Type u} [DecidableEq ι] (spec : OracleSpec ι) (α β : Type u) : Type (u + 1)

A security adversary bundling a computation with a bound on the number of queries it makes, where the bound must be shown to satisfy IsQueryBound. We also require an explicit list of all oracles used in the computation, which is necessary in order to make certain reductions computable.

• run : α → OracleComp spec β
• qb : ι → ℕ
• qb_isQueryBound (x : α) : (self.run x).IsQueryBound self.qb
• activeOracles : List ι
• mem_activeOracles_iff (i : ι) : i ∈ self.activeOracles ↔ self.qb i ≠ 0