Towards Practical Zero-Knowledge Proof for PSPACE
Ashwin Karthikeyan, Hengyu Liu, Kuldeep S. Meel, Ning Luo
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 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.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 93fc7d4c-775b-4842-8b1b-1773382ec6bfCited by top-tier papers1
Ask how each one uses itBuilds on13
- Ligero: Lightweight Sublinear Arguments Without a Trusted SetupScott Ames, Carmit Hazay, Yuval Ishai, Muthuramakrishnan VenkitasubramaniamCCS 2017 · 338 citations
- Wolverine: Fast, Scalable, and Communication-Efficient Zero-Knowledge Proofs for Boolean and Arithmetic CircuitsChenkai Weng, Kang Yang, Jonathan Katz, Xiao WangS&P 2021 · 205 citations
- Mystique: Efficient Conversions for Zero-Knowledge Proofs with Applications to Machine LearningChenkai Weng, Kang Yang, Xiang Xie, Jonathan Katz et al.USENIX Security 2021 · 161 citations
- Time- and Space-Efficient Arguments from Groups of Unknown OrderAlexander R. Block, Justin Holmgren, Alon Rosen, Ron D. Rothblum et al.CRYPTO 2021 · 67 citations
- Appenzeller to Brie: Efficient Zero-Knowledge Proofs for Mixed-Mode Arithmetic and Z2kCarsten Baum, Lennart Braun, Alexander Munch-Hansen, Benoît Razet et al.CCS 2021 · 29 citations
Related papers
- Proving UNSAT in Zero KnowledgeNing Luo, Timos Antonopoulos, William R. Harris, Ruzica Piskac et al.CCS 2022 · 14 citations
- ZKSMT: A VM for Proving SMT Theorems in Zero KnowledgeDaniel Luick, John C. Kolesar, Timos Antonopoulos, William R. Harris et al.USENIX Security 2024
- Coinductive Proofs of Regular Expression Equivalence in Zero KnowledgeJohn C. Kolesar, Shan Ali, Timos Antonopoulos, Ruzica PiskacOOPSLA 2025 · 4 citations
- Proof Simulation via Round-based Strategy Extraction for QBFLeroy ChewAAAI 2025 · 3 citations
- Automating Bitvector and Finite Field Equivalence Proofs in LeanElizaveta Pertseva, Valentin Robert, Clark W. Barrett, James ParkerCAV 2026
