June 2007: secprf (Provsec 2007)

The whole archive: provsec2007.tar.gz

Contents overview:

• Base formalization:
  • build: Makefile.
  • util.v: Addendum to the standard library.
  • distrib.v: Formalization of probabilities.
  • oracle.v: Specification of the random oracle.
  • game.v: Syntax and semantics of games.
• Reusable lemmas:
  • transform.v: Simple syntactic transformations.
  • random.v: Properties of random sampling.
  • preserv.v: Preservation of probabilities.
  • prob_pred.v: Probabilistic predicates.
  • bound.v: Probability bounds.
  • fun_lem.v: Specialization of the fundamental lemma of game-playing.
• Use-case:
  • switching.v: Formal proof of the PRP/PRF Switching Lemma.