wiki:SNARKs

Version 5 (modified by warner, at 2014-03-11T18:51:57Z) (diff)

--

zero-knowledge proofs/arguments of knowledge: reading list

This page collects useful papers, articles, and links about multi-party computation and zero-knowledge proofs.

SNARKs

SNARKs for C

SNARKs for C: Verifying Program Executions Succinctly and in Zero Knowledge: (Ben-Sasson, Chiesa, Genkin, Tromer, Virza). This defines the zk-SNARK (zero-knowledge Succinct Non-interactive ARgument of Knowledge) scheme used by Zerocash.

This paper collects a number of previous clever ideas, adds some new ones, and finds ways to optimize the combination enough to make everything useful. The resulting system does the following:

  • compiles an arbitrary C program into a simple virtual machine named "TinyRAM"
  • performs a one-time key-generation phase that takes the program and limits on runtime and input size, and produces two keys: the "proving key" and the "verification key". The proving key is very big, while the verification key is pretty small.
  • for each run of the program (given some primary input):
    • the Prover runs the TinyRAM program in a special way that gathers information about its execution (order of execution, changes to memory values). It also gets "auxilliary input", which is not revealed to the verifier, and represents nondeterminism (somehow).
    • the Prover combines this information with the proving key to create the proof. These proofs are very small.
    • later, the Verifier can combine the proof, the primary input, and the verification key, and compute a single "accept/reject" value. Verifying a proof is much much faster than creating one.

One example they use is a proof of a good solution for the "rectilinear Traveling Salesman Problem", whose input is the node locations (x,y), the starting point (x,y), and a distance bound. You can solve this problem by measuring the Manhattan distance for all possible routes (permutations of the non-starting-point nodes) and finding at least one whose total distance is lower than the bound. Their example uses such a solution as the "auxilliary input", and a TinyRAM program which sums the distances and compares it against the bound. The verifier learns that the program really does run and emits "yes", without learning what the route is.

For a 200-node graph, their TinyRAM program had 1105 instructions and needed 11001 steps to complete. It took 247 minutes to create the proving and verification keys. The proving key was about 12GB (using an 80-bit security level), and the verification key was 620 bytes. It then took 155 minutes to create one instance of the proof, and the proof itself was 322 bytes. Verifying the proof took 0.11 seconds.

Pinocchio

Pinocchio: Nearly Practical Verifiable Computation: (Parno, Gentry)

This precursor is the application paper for the main generic snark implementation.

Recursive Composition of SNARKs

Recursive Composition and Bootstrapping for SNARKs and Proof-Carrying Data: (Nitansky, Canetti, Chiesa, Tromer)

Andrew Miller tells me that the introductory text in this paper is really good, but the rest is "more advanced technical stuff".

GGPR

Quadratic Span Programs and Succinct NIZKs without PCPs: (Gennaro, Gentry, Parno, Raykova)

This is "the" big result in this field, known as "GGPR". Andrew says this is analogous to the big Craig Gentry paper on fully-homomorphic encryption, but for SNARKs. He says it's good to use to gauge your understanding by flipping back to this one.

Justin Thaler's survey post

http://mybiasedcoin.blogspot.com/2013/09/guest-post-by-justin-thaler-mini-survey.html

MPC Lounge blog series

http://mpclounge.org/blog/

History of provable complexity-classes

http://courses.cs.washington.edu/courses/cse533/05au/pcp-history.pdf

Over the last 30 years, folks have been trying to identify what kinds of problems can be proved in this zero-knowledge style (where the "prover" knows a solution but doesn't want to reveal it, and a "verifier" wants to be convinced that they really do know a valid solution). Originally the categories of problems (defined as a class of languages in which the solution is an valid statement in the language) were quite narrow. Variations on what it means to prove something were thrown about (interactive vs non-interactive, publically-verifiable versus not, public coin-tosses vs private). Eventually it was shown that a very large class of problems can be efficiently proved this way.