ProofFrog: A Tool For Verifying Game-Hopping Proofs
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.
Collections
Cite this version of the work
Ross Evans
(2024).
ProofFrog: A Tool For Verifying Game-Hopping Proofs. UWSpace.
http://hdl.handle.net/10012/20441
Other formats
Related items
Showing items related by title, author, creator and subject.
-
Approximation, Proof Systems, and Correlations in a Quantum World
Gharibian, Sevag (University of Waterloo, 2012-08-29)This thesis studies three topics in quantum computation and information: The approximability of quantum problems, quantum proof systems, and non-classical correlations in quantum systems. Our first area of study concerns ... -
Quantum Information and Variants of Interactive Proof Systems
Upadhyay, Sarvagya (University of Waterloo, 2011-08-24)For nearly three decades, the model of interactive proof systems and its variants have been central to many important and exciting developments in computational complexity theory such as exact characterization of some well ... -
The Physical Underpinning of Security Proofs for Quantum Key Distribution
Boileau, Jean Christian (University of Waterloo, 2007-09-27)The dawn of quantum technology unveils a plethora of new possibilities and challenges in the world of information technology, one of which is the quest for secure information transmission. A breakthrough in classical ...