Towards Practical Zero-Knowledge Proof for PSPACE

TL;DR

This paper introduces the first practical zero-knowledge proof protocols for PSPACE-complete problems, specifically for QBF evaluation, enabling efficient validation of complex logical statements in zero-knowledge.

Contribution

It develops a polynomial encoding of Q-Res proofs and a ZK protocol for QBF strategies, advancing practical ZK proofs beyond NP.

Findings

Verified 72% of QBF evaluations via Q-Res proofs

Proved 82% of winning strategies within 100 seconds

Achieved practical performance on QBFEVAL instances

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.