Game-playing is an approach to write security proofs that are easy
  to verify. In this approach, security definitions and intractable
  problems are written as programs called games and reductionist
  security proofs are sequences of game transformations. This bias
  towards programming languages suggests the implementation of a tool
  based on compiler techniques (syntactic program transformations) to
  build security proofs, but it also raises the question of the
  soundness of such a tool. In this paper, we advocate the
  formalization of game-playing in a proof assistant as a tool to
  build security proofs. In a proof assistant, starting from just the
  formal definition of a probabilistic programming language, all the
  properties required in game-based security proofs can be proved
  internally as lemmas whose soundness is ensured by proof theory.
  Concretely, we show how to formalize the game-playing framework of
  Bellare and Rogaway in the Coq proof assistant, how to prove
  formally reusable lemmas such as the fundamental lemma of
  game-playing, and how to use them to formally prove the PRP/PRF
  Switching Lemma.

@INPROCEEDINGS{atm07provsec,
  author = {Reynald Affeldt and Miki Tanaka and Nicolas Marti},
  title = {Formal Proof of Provable Security by Game-playing in a Proof Assistant},
  booktitle = {1st International Conference on Provable Security (Provsec 2007)},
  pages = {151--168},
  year = {2007},
  editor = {Willy Susilo and Joseph K.\ Liu and Yi Mu},
  volume = {4784},
  series = {Lecture Notes in Computer Science},
  month = {Oct.},
  publisher = {Springer-Verlag},
  note = {To appear.}
}