Sciweavers

Share
PROVSEC
2007
Springer

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

12 years 24 days ago
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...
Reynald Affeldt, Miki Tanaka, Nicolas Marti
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where PROVSEC
Authors Reynald Affeldt, Miki Tanaka, Nicolas Marti
Comments (0)
books