Evolution of Proofs in Computer Science
Explore the development of proofs in computer science, from classical mathematical proofs to interactive and zero-knowledge proofs pioneered by researchers like Goldwasser, Micali, Rackoff, and others. Discover how proof theory has evolved over time, making computation verification more efficient and secure.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
The Evolution of Proofs in Computer Science Yael Tauman Kalai Microsoft Research
What is a Proof? Mathematical proofs: Developed by ancient Greek mathematicians [Thales,Eudoxus,Theaetetus,Atistotle 600BCE] [Euclid 300 BCE] Introduced axiomatic method, theorems are proved using deductive logic. Proof theory: well studied branch of mathematics [Hilbert 19th century]
Classical Proofs http://t1.gstatic.com/images?q=tbn:ANd9GcRgVZaiUJw6jETLHjTP2kLvHubHBHBEgPR_7e5AejdA009zk8XWQw ? ?
Zero-Knowledge Proofs [Goldwasser-Micali-Rackoff85] https://encrypted-tbn2.gstatic.com/images?q=tbn:ANd9GcQUTuUOrhz56SCCWsCh_zSwnfBPAV02PZVA8YqrN4TRxALPs_l_
Zero-Knowledge Proofs [Goldwasser-Micali-Rackoff85] https://encrypted-tbn2.gstatic.com/images?q=tbn:ANd9GcQUTuUOrhz56SCCWsCh_zSwnfBPAV02PZVA8YqrN4TRxALPs_l_ ? ?
Interactive Proofs [Goldwasser-Micali-Rackoff85] ? ? [Goldreich-Micali-Wigderson87]: Every statement that has a classical proofhas zero- knowledge interactive proof, assuming one-way functions
Interactive Proofs are More Efficient! [Lund-Fortnow-Karloff-Nissan90, Shamir90] Example: Chess
Interactive Proofs are More Efficient! [Lund-Fortnow-Karloff-Nissan90, Shamir90] correctness of any computation can be proved: Time to verify Space required to do the computation
Multi-Prover Interactive Proofs [BenOr-Goldwasser-Kilian-Wigderson88] ?1 ?2 ?1 ?2 ?
The Power of Multi-Prover Interactive Proofs (MIPs) [Babai-Fortnow-Lund90] Any proof can be made exponentially shorter with a 2-prover interactive proof!
[Fortnow-Rompel-Sipser88]: ?1 ?2?3?4 ?1 ?2?3?4 ?1 ?2 ?
Probabilistically Checkable Proofs V [Feige-Goldwasser-Lovasz-Safra-Szegedy91, Babai-Fortnow-Levin- Szegedy91, Arora-Safra92, Arora-Lund-Mutwani-Sudan-Szegedy92] PCP Theorem: Every proof can be converted to a probabilistically checkable one (of almost same size) that can be verified by reading only constant number of its bits.
Classical proofs (zero-knowledge) Interactive proofs multi-prover interactive proofs Probabilistically checkable proofs
Delegating Computation in the Real World Help me compute ? on ? ?(?) proof http://t3.gstatic.com/images?q=tbn:ANd9GcScK77uBTorrrLXSv5W0LY_P5gegzcxoCQB81Tr7sMajiUC_DNB Verifying should be easier than computing! Proving should not be much harder than computing!
Interactive Proofs not useful for real world delegation Verifying is easier that computing (time to verify proportional to space of computation) Proving is harder than computing
Interactive Proofs useful for real world delegation [Goldwasser-Kalai-Rothblum08] ? ? Proving is not harder than computing Only for functions computable by low depth circuits
Computationally-Sound Proofs [Micali94] A delegation scheme for all functions. Computational soundness: Cheating is possible, but requires too much work, assuming hardness assumption ? ? hash proof certificate! Secure under standard assumption [Kilian92] no satisfying proof of security
2-Message Delegation Scheme [Aiello-Bhatt-Ostrovsky-Rajagopalan2000, Dwork- Langberg-Naor-Nissim-Reingold2004, Kalai-Raz2009, Groth10, Gennaro-Gentry-Parno2010 , Chung-Kalai- Vadhan2010, Applebaum-Ishai-Kushilevitz2010, Gentry- Wichs2011, Parno-Raykova-Vaikuntanathan2011, Benabbas-Gennaro-Vahlis2011, Goldwasser-Lin- Rubinstein2011, Damgard-Faust-Hazay2011, Lipma12, Fiore-Gennaro2012, Bitansky-Canetti-Chiesa- Tromer2012a, Bitansky-Canetti-Chiesa-Tromer2012b, Gennaro-Gentry-Parno-Raykova2012, Kalai-Raz- Rothblum2013, Kalai-Raz-Rothblum2014]
[Kalai-Raz-Rothblum2014]: 2-message delegation scheme for all functions under standard hardness assumptions No-signalling strategies [Khaln-Tsirelson85, Rastall85] special relativity theory: information does not travel faster than the speed of light
No-Signalling Strategies ?1 ?2 ?1 ?2 ? Original soundness: ?1 and ?2don t interact Quantum soundness: ?1 and ?2may have entangled quantum states No-signalling soundness: answer of ?1 (conditioned on ?1)does not give information about ?2
Multi-Prover Interactive Proofs (MIPs) Classical soundness: [Babai-Fortnow-Lund90]: MIP for all functions Quantum soundness: [Ito-Vidick2012]: MIP for all functions No-Signalling soundness: [Kalai-Raz-Rothblum2014]: MIP for all functions
[Kalai-Raz-Rothblum2014]: No-signalling multi-prover interactive proofs for all functions 2-message delegation for all functions under standard hardness assumptions
[Kalai-Raz-Rothblum2014]: MIP ?1 ?2 ? sound against no-signalling provers ? ?1?2 ?1 ?2 ? ? [Aiello-Bhatt-Ostrovsky-Sivarama00] 2-msg delegation secure for every FHE with sub-exponential security ? ? ?1, ?2, , ? ?1, ?2, , ?
Classical proofs zero-knowledge Interactive proofs No-signalling multi-prover interactive proofs Muti-prover interactive proofs Probabilistically checkable proofs 2-message delegation
Delegation in Practice [Cormode-Mitzenmacher-Thaler2012] [Thaler-Roberts-Mitzenmacher-Pfister2012] [Thaler2013] [Vu-Setty-Blumberg-Walfish2013] [BenSasson-Chiesa-Genkin-Tromer-Virza2013] [Parno-Gentry-Howell-Raykova2013]
