Traditionally, proof systems are stated in terms of two parties. The prover and the verifier. The prover \mathcal P knows some secret information w (the witness), and wants to convince the verifier \mathcal V about some statement using w.
In many applications, the witness w is derived from sensitive information owned by mutually distrusting parties. Say Alice and Bob. In these cases, the single prover setting does not align well. Alice won’t reveal her secret to Bob; neither Bob will reveal his secret to Alice. But they still want to produce a proof of validity \pi to their joint statement. Who acts as the prover in this case?
The answer given in [BO21] is to run \mathcal P as a secure multi-party computation (MPC). For simplicity, suppose the witness is just the composition of Alice and Bob secrets w:=(a,b) They both start secret-sharing their data to a set of N provers \mathcal P_1,\ldots,\mathcal P_N:
The i-th prover has a share w_i:=(w_{a,i},w_{b,i}) of the witness w. The syntax of the SNARK changes slightly. The MPC prover takes N witness shares as input.
-
\mathsf{Setup}(1^\lambda)\rightarrow pp
-
\Pi_\mathsf{Prove}(x,\mathcal w_1,\ldots \mathcal w_N)\rightarrow \pi
-
\mathsf{Verify}(x,\pi)\rightarrow \{0,1\}
Witness extension
SNARKs can prove membership to any NP language \mathcal L. Given an instance x, the statement “x\in\mathcal L” is proved using a witness w for x. Languages are defined via an underlying efficient relation \mathcal{R}. An instance x is in \mathcal L if and only if exists w such that (x,w)\in\mathcal R.
Before running the proving or verifying algorithms, the instance/witness pair (x,w) must be reduced to an instance/witness of the NP-complete relation that the SNARK operates on. Examples of such backend relations are R1CS, Plonkish, AIR, or CCS.
The reduction is actually a composition of two maps. The instance and witness reduction
As a preliminary step, the prover of the SNARK runs both reductions. The verifier only runs the instance reduction.
Witness extension refers to running the witness reduction in MPC. For example, take the \mathsf{CircuitSAT} problem as the source relation, and \mathsf{R1CS} as the backend relation. Reducing a private satisfying input w (the \mathsf{CircuitSAT} witness) to an \mathsf{R1CS} witness \mathbf w, comprises collecting all the values of the intermediate circuit wires into \mathbf w.
The final compiled protocol \Pi_{\mathsf{Prove}}
The prover is distributed with two separate MPC protocols \Pi_{\mathsf{Prove}}:=(\Pi_{\mathsf{reduceWitness}},\Pi_{\mathsf{R1CS}}), which are executed sequentially:
-
Frontend step. The N provers input a sharing [w] of the original witness to \Pi_{\mathsf{reduceWitness}}, and end up with a sharing [\mathbf{w}] of the \mathsf{R1CS} witness.
-
Backend step. The N provers input \mathbf{x}:=\mathsf{reduceInstance}(x) and the sharing [\mathbf{w}] to \Pi_\mathsf{R1CS}, and end up with a proof \pi.
Theorem 1 of [BO21]: If (\mathsf{Setup},\mathsf{Prove}, \mathsf{Verify}) is a zk-SNARK, and \Pi_\mathsf{Prove} is an MPC protocol for \mathsf{Prove} secure for up to t corruptions, then (\mathsf{Setup},\Pi_\mathsf{Prove}, \mathsf{Verify}) is knowledge sound and t-zero-knowledge.
Zero-knowledge and soundness
The notions of zero-knowledge and knowledge soundness are slightly revisited in the collaborative setting. We will state them at high level, stressing their differences with the single prover setting. Refer to [BO21, Defn.2] for formal definitions.
t-Zero-knowledge. Up to t\leq N colluding provers learn nothing about the witness shares they do not control, other than the validity of the joint witness [w] = (w_1,\ldots,w_N). This is formalized with a simulator algorithm that, using the instance x and t colluding witness shares, can generate transcripts that are indistinguishable from transcripts of the MPC protocol \Pi_\mathsf{Prove}:
The simulator is given an extra piece of information: a bit b signalling whether the joint witness [w] is valid or not for the instance x. This leakage is unavoidable: t dishonest provers can always engage in \Pi_\mathsf{Prove} with arbitrary witness portions and check whether their choice yields a valid proof \pi.
In the single prover setting, zero-knowledge requires that the simulator, using the instance x alone, generates indistinguishable transcripts from proof transcripts involving arbitrary verifiers. In the collaborative setting, zero-knowledge is closer to what is meant by privacy in the MPC literature. But, one can argue that, seeing the verifier as the entity corrupting the t provers, we can recover the standard notion.
Knowledge soundness. It is possible to extract the witness [w] from N arbitrary provers \vec{\mathcal P}^* = (\mathcal P^*_1, \ldots, \mathcal P^*_N) that generate a valid proof \pi. Extraction is possible even if the provers deviate from the prescribed protocol \Pi_\mathsf{Prove}. As in the single prover setting, the extractor algorithm \mathsf{Ext} is given rewinding oracle access to all provers \vec{\mathcal P^*}. It can emulate a run between them and, if they produce a valid proof, it can extract a valid joint witness:
In the collaborative setting, knowledge soundness refers to the joint witness. It does not say that each \mathcal P_i^* knows a valid share w_i, which is what the single prover notion demands. Requiring individual knowledge is hard to formalize anyway. Convincing a verifier that a single prover knows a valid witness share requires awareness of the number of participating provers. But the proof system is non-interactive, so N is hidden to the verifier.
Coming up
In the next post, we will dive into the details of which SNARKs are amenable to distribute the backend prover efficiently. Don’t miss out!