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