Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Practical Zero-Knowledge Proof for PSPACE

Ashwin Karthikeyan, Hengyu Liu, Kuldeep S. Meel, Ning Luo

TL;DR

This work provides the first practical zero-knowledge proofs for PSPACE by enabling ZK proofs of $QBF$ evaluation through $Q$-Resolution proofs and by also proving knowledge of winning strategies (Herbrand/Skolem functions). It introduces polynomial encodings of $Q$-Res, a commit-and-prove ZK framework, and two protocols (ZKQRES and ZKWS) that verify $QBF$ evaluation and winning strategies, respectively, on real benchmarks such as QBFEVAL. Experimental results show verifiable coverage of up to $72 ext{\%}$ of false $QBF$ evaluations via $Q$-Res proofs and $82 ext{\%}$ of instances’ winning strategies within $100$ seconds, with optimization techniques like batching reducing overhead. The work bridges theory and practice, enabling privacy-preserving certificates for PSPACE-complete problems and impacting domains like PEC, C-PLAN, and BBC, while outlining efficiency-leakage trade-offs and avenues for future improvements.

Abstract

Efficient zero-knowledge proofs (ZKPs) have been restricted to NP statements so far, whereas they exist for all statements in PSPACE. This work presents the first practical zero-knowledge (ZK) protocols for PSPACE-complete statements by enabling ZK proofs of QBF (Quantified Boolean Formula) evaluation. The core idea is to validate quantified resolution proofs (Q-Res) in ZK. We develop an efficient polynomial encoding of Q-Res proofs, enabling proof validation through low-overhead arithmetic checks. We also design a ZK protocol to prove knowledge of a winning strategy related to the QBF, which is often equally important in practice. We implement our protocols and evaluate them on QBFEVAL. The results show that our protocols can verify 72% of QBF evaluations via Q-Res proof and 82% of instances' winning strategies within 100 seconds, for instances where such proofs or strategies can be obtained.

Towards Practical Zero-Knowledge Proof for PSPACE

TL;DR

This work provides the first practical zero-knowledge proofs for PSPACE by enabling ZK proofs of evaluation through -Resolution proofs and by also proving knowledge of winning strategies (Herbrand/Skolem functions). It introduces polynomial encodings of -Res, a commit-and-prove ZK framework, and two protocols (ZKQRES and ZKWS) that verify evaluation and winning strategies, respectively, on real benchmarks such as QBFEVAL. Experimental results show verifiable coverage of up to of false evaluations via -Res proofs and of instances’ winning strategies within seconds, with optimization techniques like batching reducing overhead. The work bridges theory and practice, enabling privacy-preserving certificates for PSPACE-complete problems and impacting domains like PEC, C-PLAN, and BBC, while outlining efficiency-leakage trade-offs and avenues for future improvements.

Abstract

Efficient zero-knowledge proofs (ZKPs) have been restricted to NP statements so far, whereas they exist for all statements in PSPACE. This work presents the first practical zero-knowledge (ZK) protocols for PSPACE-complete statements by enabling ZK proofs of QBF (Quantified Boolean Formula) evaluation. The core idea is to validate quantified resolution proofs (Q-Res) in ZK. We develop an efficient polynomial encoding of Q-Res proofs, enabling proof validation through low-overhead arithmetic checks. We also design a ZK protocol to prove knowledge of a winning strategy related to the QBF, which is often equally important in practice. We implement our protocols and evaluate them on QBFEVAL. The results show that our protocols can verify 72% of QBF evaluations via Q-Res proof and 82% of instances' winning strategies within 100 seconds, for instances where such proofs or strategies can be obtained.

Paper Structure

This paper contains 57 sections, 5 theorems, 15 equations, 21 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Key challenges.
  3. This work.
  4. Our Contribution.
  5. Related Work
  6. A motivating example.
  7. Preliminaries
  8. Quantified Boolean Formulae
  9. Winning strategies.
  10. Efficient Zero-Knowledge Proof
  11. Set argument.
  12. Append-only array.
  13. ZKUNSAT zkunsat.
  14. ZKP for Q-Res Proof Validation
  15. Encoding QBF
  16. ...and 42 more sections

Key Result

Theorem 1

A closed QBF in PCNF is unsatisfiable if and only if there exists a sequence of Q-resolution steps leading to the empty clause.

Figures (21)

  • Figure 1: Paper roadmap. We propose two practical approaches for proving QBF evaluation in ZK: one based on Q-Res proofs and the other based on winning strategies. We implement and evaluate both approaches, with results presented in \ref{['sec:eval']}.
  • Figure 2: Our protocols' evaluation against QBFEVAL. We present the cumulative fraction of QBF instances successfully verified by our protocols via Q-RES proofs and winning strategies within a given time threshold (left $Y$-axis), as well as the fraction verified around each time point (right $Y$-axis). Our protocols can verify 72% of QBFs' evaluations via Q-Res proof and 82% of instances' winning strategies within 100 seconds, for instances where such proofs or strategies can be obtained. See \ref{['sec:eval']} for details.
  • Figure 3: The Q-Res proof for falsifying Formula \ref{['eq:qbf']}. Clauses are deducted via $\forall$-Red and $\exists$-Res. $\forall$-reduction removes universal literals from a clause when permitted by the quantifier prefix. $\exists$-Res combines two clauses by eliminating the complementary literals. The deducted empty clause indicates that the evaluation of Formula \ref{['eq:qbf']} is false.
  • Figure 4: Functionality for zero-knowledge proofs of circuit satisfiability and integer comparison.
  • Figure 5: Functionality for set operations in ZK.
  • ...and 16 more figures

Theorems & Definitions (6)

  • Theorem 1: BUNING199512
  • Theorem 2: balabanov2011resolutionniemetz2012resolution
  • Theorem 3
  • Theorem 4
  • Theorem 5: Herbrand Function Well-Formedness
  • proof