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. (These files correspond to an older version of CryptoVerif; an up-to-date model is included in the CryptoVerif distribution: file examples/obasic/fdh.ocv.)

FDH input file
Text output of the prover (Begins with steps executed for proof search, followed by details on the found proof, including the sequence of games.)
TeX output of the prover (Describes the found proof.)
The above file compiled to PDF (after wrapping two very long lines)

The automatic verifier CryptoVerif is also available here.

Bruno Blanchet and David Pointcheval