Computationally Sound Proofs

By Silvio Micali. 2000

468 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Program Analysis & Verification, Automated Theorem Proving & Formal Methods

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Dan Boneh
2. Srinath T. V. Setty
3. Eli Ben-Sasson
4. Michael Walfish
5. Andrew Justin Blumberg
6. Eran Tromer
7. Brent Waters
8. Alessandro Chiesa

In Computational Theory and Mathematics

1. Srinath T. V. Setty
2. Eli Ben-Sasson
3. Dan Boneh
4. Michael Walfish
5. Andrew Justin Blumberg
6. Brent Waters
7. Eran Tromer
8. Alessandro Chiesa

In Program Analysis & Verification

1. Srinath T. V. Setty
2. Michael Walfish
3. Andrew Justin Blumberg
4. Eli Ben-Sasson
5. Justin Thaler
6. Eran Tromer
7. Alessandro Chiesa
8. Charalampos Papamanthou

In Automated Theorem Proving & Formal Methods

1. Srinath T. V. Setty
2. Michael Walfish
3. Eran Tromer
4. Eli Ben-Sasson
5. Andrew Justin Blumberg
6. Alessandro Chiesa
7. Madars Virza
8. Dan Boneh

Citations in the corpus

• Advances and Open Problems in Federated Learning (2019, background): “[40] and has been studied under various terms in the literature: checking computations [40], certified computation [295], delegating computations [185], as well as verifiable computing [173].”
• Geppetto: Versatile Verifiable Computation (2015, background): “Prior work on verifying computation focused on narrow classes of computation [32, 51], relied on physical-security assumptions [41, 47], assumed uncorrelated failures [19, 20], or achieved good asymptotics [2, 28, 30, 31, 33, 38, 44] but impractical concrete performance [46, 50].”
• Pinocchio: Nearly Practical Verifiable Computation (2013, methodology): “In practice however, because they rely on complex Probabilis-tically Checkable Proofs (PCPs) [17] or fully-homomorphic encryption (FHE) [24], the performance is unacceptable – verifying small instances would take hundreds to trillions of years ( § 5.2).”
• Verifying computations with state (2013, neutral): “To briefly compare the performance of Zaatar and Pinocchio, Pinocchio has superior amortization behavior (see above) but higher proving and setup costs (and hence higher cross-over points), by constant factors.”
• Introduction to Property Testing (2017, background): “, CS-proofs [190, 207] and their applications [31, 67]), and the length of the PCP affects the complexity of those applications.”
• Efficient Arguments without Short PCPs (2007, background): “Moreover, classical proofs cannot be generally used to speed up the verification of a deterministic polynomial-time computation, a goal which is strongly motivated by real life applications.”
• Scalable, transparent, and post-quantum secure computational integrity (2018, methodology): “A ZK system based on the PCP Theorem (ZK-PCP) [74, 85, 49, 75, 71] has three additional advantages that are essential for ongoing public trust in computational integrity.”
• Fast reductions from RAMs to delegatable succinct constraint satisfaction problems: extended abstract (2013, background): “All known PCP-based succinct argument constructions [61, 71, 5, 30, 22, 14, 29, 47] inherit these problem representations.”
• Taking Proof-Based Verified Computation a Few Steps Closer to Practicality (2012, methodology): “Applying proof systems to verifiable computation is standard in the theory community [5–7, 10, 16, 32, 37, 38, 43], and the asymptotics continue to improve [13, 14, 23, 46].”
• Interactive Oracle Proofs (2016, methodology): “A Merkle tree with privacy is similarly used by [IMS12, IMSX15], along with honest-verifier PCPs, to achieve zero knowledge in modifications of Kilian’s [Kil92, BG08] and Micali’s [Mic00] constructions.”
• The random oracle methodology, revisited (2000, methodology): “2 uses in an essential way non-interactive CS-proofs (in the Random Oracle Model), as defined and constructed by Micali [27].”
• An Uninstantiable Random-Oracle-Model Scheme for a Hybrid-Encryption Problem (2004, background): “(Their schemes are designed to return the secret key depending on the result of some test applied to an output of the oracle, and they use diagonalization and CS proofs [18].”
• The Efficient Server Audit Problem, Deduplicated Re-execution, and the Web (2017, background): “Execution integrity has long been studied by theorists [15, 37, 38, 42, 60], and these ideas have been refined and implemented [19, 32, 65, 75] (see [89] for a survey and [12, 18, 88, 96] for recent developments).”
• Quadratic Span Programs and Succinct NIZKs without PCPs (2013, background): “Micali [36] showed how to make these arguments non-interactive in the random oracle model.”
• Scalable Zero Knowledge with No Trusted Setup (2019, methodology): “– Non-interactive STARK (nSTARK) As shown by Micali [61] and Valiant [77] for the PCP model, and by Ben-Sasson et al.”