A tool for checking transitions in cryptographic game-hopping proofs.
ProofFrog checks the validity of game hops for cryptographic game-hopping proofs in the reduction-based security paradigm: it checks that the starting and ending games match the security definition, and that each adjacent pair of games is either interchangeable (by code equivalence) or justified by a stated assumption. Proofs are written in FrogLang, a small C/Java-style domain-specific language designed to look like a pen-and-paper proof. ProofFrog can be used from the command line, a browser-based editor, or an MCP server for integration with AI coding assistants. ProofFrog is suitable for introductory level proofs, but is not as expressive for advanced concepts as other verification tools like EasyCrypt.
pip install proof_frog
proof_frog download-examples
proof_frog prove examples/joy/Proofs/Ch2/OTPSecure.proofFull documentation, including installation instructions, tutorials, and a language reference, are available at prooffrog.github.io.
| Repository | Description |
|---|---|
| ProofFrog | Core tool: parser, proof engine, CLI, web editor, LSP server, and MCP server |
| examples | Growing collection of cryptographic definitions and verified proofs |
The examples catalogue includes proofs covering:
- Introductory proofs adapted from The Joy of Cryptography by Mike Rosulek
- Symmetric encryption: PRF-based encryption, composition of encryption schemes, encrypt-then-MAC authenticated encryption
- Pseudorandom generators: length-tripling PRG construction, counter-mode PRG from a PRF
- Pseudorandom functions: multi-key PRF security from single-key security
- Group-based assumptions: implications between DDH, CDH, and Hashed DDH
- Public-key encryption: ElGamal, Hashed ElGamal, hybrid KEM-DEM encryption
- KEM constructions: PRF-based KEM with correctness, IND-CPA, and IND-CCA proofs
- Research applications: KEM combiner from Giacon, Heuer, and Poettering (PKC 2018)
- Ask questions on GitHub Discussions
- Report bugs or request features via Issues
- Contribute pull requests
ProofFrog is released under the MIT License.
ProofFrog was created by Ross Evans and Douglas Stebila, building on the pygamehop tool created by Douglas Stebila and Matthew McKague. ProofFrog's syntax and approach to modelling is heavily inspired by Mike Rosulek's The Joy of Cryptography. We acknowledge the support of the Natural Sciences and Engineering Research Council of Canada (NSERC).
