Formal Proof of Provable Security by Game-Playing in a Proof Assistant

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 s...

• Type: Conference
• Year: 2007
• Where: PROVSEC
• Authors: Reynald Affeldt, Miki Tanaka, Nicolas Marti
• Keywords: Proof Assistant, PROVSEC 2007, Reductionist Security Proofs, Security Proofs