2026-09-22T08:24:42Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/125632 2025-02-06 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

application/pdf en text Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-02-04 without embargo terms The student, Bolton Bailey, accepted the attached license on 2024-07-12 at 14:24. The student, Bolton Bailey, submitted this Dissertation for approval on 2024-07-12 at 14:33. This Dissertation was approved for publication on 2024-07-12 at 14:58. DSpace SAF Submission Ingestion Package generated from Vireo submission #21102 on 2025-02-04 at 21:05:21 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. 2024-08 Thesis https://hdl.handle.net/2142/125632 Copyright 2024 Bolton Bailey Formalizing soundness proofs of SNARKs Bailey, Bolton 2024-07-12 Miller, Andrew Miller, Andrew Gunter, Carl Parno, Bryan Ringer, Talia Rosu, Grigore Formal Methods Snarks eng Siebel Computing &DataScience Computer Science University of Illinois at Urbana-Champaign Ph.D. Dissertation