{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/125632"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/125632","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Formalizing soundness proofs of SNARKs","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-02-04 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-02-04 without embargo terms","abstract_has_math":false,"creators":["Bailey, Bolton"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Miller, Andrew","Gunter, Carl","Parno, Bryan","Ringer, Talia","Rosu, Grigore"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2024,"date_issued":"2024-08","date_published":"2024-08","updated_at":"2026-07-22T22:25:02Z","subjects":["Formal Methods","Snarks"],"languages":["en","eng"],"rights":["Copyright 2024 Bolton Bailey"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/125632","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Miller, Andrew","Gunter, Carl","Parno, Bryan","Ringer, Talia","Rosu, Grigore"]},{"key":"dc:creator","label":"Author","values":["Bailey, Bolton"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2024-08","2024-07-12"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Formal Methods","Snarks"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2024 Bolton Bailey"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/125632"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Formalizing soundness proofs of SNARKs"]}]}],"canonical_facts":{"dc:contributor":["Miller, Andrew","Gunter, Carl","Parno, Bryan","Ringer, Talia","Rosu, Grigore"],"dc:creator":["Bailey, Bolton"],"dc:date":["2024-08","2024-07-12"],"dc:description":["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."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/125632"],"dc:language":["en","eng"],"dc:rights":["Copyright 2024 Bolton Bailey"],"dc:subject":["Formal Methods","Snarks"],"dc:title":["Formalizing soundness proofs of SNARKs"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:02Z"}