Director of Research (if dissertation) or Advisor (if thesis)
Miller, Andrew
Doctoral Committee Chair(s)
Miller, Andrew
Committee Member(s)
Gunter, Carl
Parno, Bryan
Ringer, Talia
Rosu, Grigore
Department of Study
Siebel Computing &DataScience
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Formal Methods
Snarks
Language
eng
Abstract
There is a high demand for rigorous security proofs for Succinct Non-interactive Arguments of Knowledge (SNARKs). We look to apply modern formal tools to this domain: This thesis describes techniques we have developed to formally state and prove security properties for the most succinct SNARKs in the literature, including linear PCP and polynomial IOP based SNARKs. In particular, we focus on the soundness of these compact proof systems, an area that previous works on the formalization of cryptography have avoided. A challenge in this endeavor is the wide variety of protocols that differ in small details. To tame these complications, our work is guided by systematic specifications of SNARK constructions in the classes we study. We take advantage of shared heritage between systems to offer the potential for automated formal analysis. This automation allows us to quickly produce formal verified proofs of soundness for a large class of SNARKs simultaneously, bringing down the overhead of producing more proofs for further variants on these SNARK construction approaches.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
