ProofFrog: A Tool For Verifying Game-Hopping Proofs
Loading...
Date
2024-04-15
Authors
Evans, Ross
Journal Title
Journal ISSN
Volume Title
Publisher
University of Waterloo
Abstract
Cryptographic proofs allow researchers to provide theoretical guarantees on the security
that their constructions provide. A proof of security can completely eliminate a class of
attacks by potential adversaries. Human fallibility, however, means that even a proof
reviewed by experts may still hide flaws or outright errors. Proof assistants are software
tools built for the purpose of formally verifying each step in a proof, and as such have the
potential to prevent erroneous proofs from being published and insecure constructions from
being implemented. Unfortunately, existing tooling for verifying cryptographic proofs has
found limited adoption in the cryptographic community, in part due to concerns with ease
of use.
This thesis presents ProofFrog: a new tool for verifying cryptographic game-hopping
proofs. ProofFrog is designed with the average cryptographer in mind, using an imperative
syntax for specifying games and a syntax for proofs that closely models pen-and-paper
arguments. As opposed to other proof assistant tools which largely operate by manipulating
logical formulae, ProofFrog manipulates abstract syntax trees (ASTs) into a canonical form
to establish indistinguishable or equivalent behaviour for pairs of games in a user-provided
sequence. We detail the domain-specific language developed for use with the ProofFrog
proof engine as well as present a sequence of worked examples that demonstrate ProofFrog’s
capacity for verifying proofs and the exact transformations it applies to canonicalize ASTs.
A tool like ProofFrog that prioritizes ease of use can lower the barrier of entry to using
computer-verified proofs and aid in catching insecure constructions before they are made
public.
Description
Keywords
cryptography, proof verification, game hopping, formal verification, proof assistants, state separating proofs, ProofFrog