ProofFrog is a tool for checking transitions in cryptographic game-hopping proofs. It verifies that each adjacent pair of games in a proof 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 is suitable for introductory level proofs, but is not as expressive for advanced concepts as other verification tools like EasyCrypt.
This repository contains a growing collection of cryptographic definitions and proofs that can be used with ProofFrog.
Follow the installation instructions to install ProofFrog (requires Python 3.11+):
pip install proof_frog
Then download the examples:
proof_frog download-examples
# or clone this repository directly:
# git clone https://github.com/ProofFrog/examples
To check a proof:
proof_frog prove joy/Proofs/Ch2/OTPSecure.proof
This repository contains primitives, schemes, games, and proofs covering:
- Joy of Cryptography — proofs from Chapters 1 and 2 of The Joy of Cryptography by Mike Rosulek, designed to be read alongside the textbook and the best place to start learning ProofFrog
- 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)
A detailed catalogue of examples is available at prooffrog.github.io/examples.
Full ProofFrog documentation is available at prooffrog.github.io, including a tutorial, language reference, and worked examples.
These examples are released under the MIT License.