Manual

ProofFrog is a tool for verifying transitions in cryptographic game-hopping proofs. This manual is the place to start if you want to use it: install it, write your first proof, and look up language constructs as you go.

Getting Started

If you are new to ProofFrog, work through the pages below in order:

1. Installation: Set up Python, install via pip, and verify.
2. Tutorial: A two-part hands-on introduction — Part 1: Hello Frog runs an existing proof, breaks it on purpose, and fixes it; Part 2: OTP has one-time secrecy walks through writing your first complete four-file proof from scratch, about the security of the one-time pad.
3. Worked Examples: Read fully-explained walkthroughs of real proofs, starting with chained symmetric encryption (the first reduction proof) and then chosen-plaintext attack security of hybrid public key encryption (the KEM-DEM construction) (a multi-primitive proof).

After that, treat the manual as a reference and use the navigation to look up what you need.

Reference

• Language Reference: Types, operators, sampling, statements, the four file types (primitive, scheme, game, proof), and the execution model.
• Canonicalization: How ProofFrog tries to check that two games are equivalent: what transformations it applies automatically, how to use helper games, and how to diagnose a failing hop.
• Limitations: Capability limits of ProofFrog’s language and canonicalization engine. ProofFrog’s soundness is discussed in the “For Researchers” section.
• Command-Line Interface Reference: proof_frog on the command-line: version, parse, check, prove, describe, web.
• Web Editor: Using ProofFrog’s web-based editor environment via proof_frog web.
• Editor Plugins: How to add ProofFrog extensions to VSCode and other editors using the LSP server.
• Troubleshooting: How to diagnose common errors.