Bounded verification for finite-field-blasting. In a compiler for zero knowledge proofs

DOI10.1007/978-3-031-37709-9_8zbMATH Open1547.68447MaRDI QIDQ6535685FDOQ6535685

Authors: Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark Barrett 

Publication date: 1 February 2024

Recommendations

• Stacked garbling for disjunctive zero-knowledge proofs
• Automatic generation of \(\Sigma\)-protocols
• Scalable zero knowledge via cycles of elliptic curves
• Scalable zero knowledge via cycles of elliptic curves
• An efficient ZK compiler from SIMD circuits to general circuits

Mathematics Subject Classification ID

Cryptography (94A60) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• A mathematical introduction to logic.
• The knowledge complexity of interactive proof-systems
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• CakeML
• A formally verified compiler back-end
• Automated soundness proofs for dataflow analyses and transformations via local rules
• Scalable zero knowledge with no trusted setup
• Marlin: preprocessing zkSNARKs with universal and updatable SRS
• The verified CakeML compiler backend
• Towards satisfiability modulo parametric bit-vectors
• Towards bit-width-independent proofs in SMT solvers

This page was built for publication: Bounded verification for finite-field-blasting. In a compiler for zero knowledge proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535685)