Automated Security Proofs with Sequences of Games

Bruno Blanchet and David Pointcheval. Automated Security Proofs with Sequences of Games. In Cynthia Dwork, editor, CRYPTO'06, Lecture Notes on Computer Science, Santa Barbara, CA, August 2006. Springer Verlag.

This page presents the CryptoVerif input and output for the FDH signature example.

The automatic verifier CryptoVerif is also available here.
Bruno Blanchet and David Pointcheval