We're building a private computation platform similar to Zexe, where nested proofs are used to preserve the privacy of the programs being computed. We may use different proof systems for the inner and outer proofs. For the inner proofs, we're searching for a system with these properties:

  • Conjectured post-quantum security, which rules out Groth16 etc.
  • Constant or near-constant verification time. Logarithmic would be okay, but polylogarithmic (like STARKs) would be undesirable. If verification was polylogarithmic, we'd probably want multiple verification programs to handle different ranges of proof sizes, and the verification program being used for a computation would leak some information about the kind of computation being done.
  • Non-interactivity.

We don't need a zero knowledge property; that would be redundant since privacy is already protected by the outer proof system.

I believe the PCP theorem implies that it's at least possible to get logarithmic proof sizes (in the QROM), by transforming a PCP scheme into a sigma protocol, then applying Unruh's transform for non-interactivity. If we used a Merkle accumulator for commitments in the sigma protocol, the SNARG would consist of a constant number of log-sized Merkle paths.

Is this reasoning correct? Are there any practical proof systems with these properties?

  • 1
    $\begingroup$ "Cycles of elliptic curves" might serve as a model for inner/outer separation, 2014/595. It should be practical to verify "inner" proofs with "outer" system, so, is it 2018/475? Another design decision: are you formalizing computations with R1CS, what kind of witness and relations are expected for "inner"? An argument system (not a proof) using proper hard problem might be enough for post-quantum security. $\endgroup$ – Vadym Fedyukovych Nov 11 '18 at 22:58
  • 1
    $\begingroup$ Regarding your last question: yes, the reasoning is correct, if by "a PCP scheme" you mean "Kilian's succinct PCP-based ZK argument system". Also, you should note that although the standard Fiat-Shamir transform is not proven to be secure in the quantum ROM, we do not know of any attack against the quantum security of non-interactive proofs obtained by applying Fiat-Shamir, instead of Unruh, to an interactive quantum-safe proof. So, if you want something efficient, I would recommend using Fiat-Shamir instead of Unruh - that's what is done in most NIST proposals for post-quantum cryptography. $\endgroup$ – Geoffroy Couteau Nov 14 '18 at 23:31

There exists as of today two candidate SNARGs satisfying all your criteria. The first one is a recent proposal by Boneh, Ishai, Sahai, and Wu, which was presented last year at Eurocrypt. They achieve this construction by building upon the notion of linear-only encryption, which had been developed in previous works of some of the authors.

The second one, by Gennaro, Minelli, Nitulescu, and Orrù, is even more recent, it was presented at CCS this year. It generalizes square span programs, which were previously used to build SNARGs under pairing-based assumptions, to the lattice setting. It also comes with a proof-of-concept (unoptimized) implementation.

Both approach suffer from a common downside: they are designated-verifier, which means that a secret verification key is required to check the proof. If you crucially want public verifiability, even though it's theoretically feasible in a quantum-safe setting (as you mentioned, applying the random-oracle-based Fiat-Shamir transform to Kilian's succinct PCP-based proof system does the trick, and leads to logarithmic proof size and verification time), we do unfortunately not yet know of any concretely efficient construction that would meet all of your criteria.

| improve this answer | |

Out of all currently known state-of-the-art (publicly verifiable) SNARG constructions there exist three which satisfy conjectured PQ security:

  1. Ligero
  2. Stark
  3. Aurora

Each of these have polylogarithmic verification time and hence do not require your somewhat stringent requirement. Concretely, the best verification times are achieved by Aurora (one order of magnitude quicker than Ligero, two orders of magnitude quicker than Stark). In practice, verification times range from milliseconds to seconds.

| improve this answer | |
  • $\begingroup$ Ligero has polylogarithmic verification time? I don't think it's the case: the proof size is square root of the circuit, so even simply reading the proof, yet alone verifying it, requires square root computation. $\endgroup$ – Geoffroy Couteau Nov 14 '18 at 23:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.