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

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