Formalizing soundness proofs of SNARKs

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2024

Author dc:creator

• Bailey, Bolton

Contributors dc:contributor

• Miller, Andrew
• Gunter, Carl
• Parno, Bryan
• Ringer, Talia
• Rosu, Grigore

• Formal Methods
• Snarks

Statement dc:rights

• Copyright 2024 Bolton Bailey

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/125632

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F125632