ProofFrog

A tool for checking transitions in cryptographic game-hopping proofs.

ProofFrog checks the validity of transitions in game-hopping proofs — the standard technique in provable security for showing that a cryptographic scheme satisfies a security property. Proofs are written in FrogLang, a domain-specific language for defining primitives, schemes, security games, and proofs. ProofFrog is designed to handle introductory-level proofs, trading expressivity and power for ease of use. The ProofFrog engine checks each hop by manipulating abstract syntax trees into a canonical form, with some help from Z3 and SymPy. ProofFrog’s engine does not have any formal guarantees: the soundness of its transformations has not been verified.

ProofFrog can be used via a command-line interface, a browser-based editor, or an MCP server for integration with AI coding assistants.

Getting Started

ProofFrog is implemented in Python (3.11+) and can be installed using pip:

pip install proof_frog
git clone https://github.com/ProofFrog/examples        # optionally download examples

See the getting started page for detailed installation options, the web interface, and CLI usage, or the guide to writing proofs in ProofFrog.

A list of examples is given on the Examples page.

Development

See the GitHub repo for source code and development information. ProofFrog is released under the MIT License.

Publications

ProofFrog was created by Ross Evans and Douglas Stebila, building on the pygamehop tool created by Douglas Stebila and Matthew McKague. For more information about ProofFrog’s design, see Ross Evans’ master’s thesis and eprint 2025/418.

We acknowledge the support of the Natural Sciences and Engineering Research Council of Canada (NSERC).