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.)
The automatic verifier CryptoVerif is also available
and David Pointcheval