“Towards Practical Zero‑Knowledge Proof for PSPACE”
Location: 177 Huntington Ave, conference room 503
Abstract: Zero-knowledge proofs (ZKPs) allow one party to prove a statement without revealing anything beyond its truth. While efficient ZKP systems exist for NP problems such as SAT, extending them to PSPACE has so far remained theoretical. In this talk, I will present our recent work on practical ZKPs for PSPACE-complete problems via proof systems for quantified Boolean formulas (QBFs). Our first protocol validates quantified-resolution (Q-RES) proofs in zero knowledge, and our second protocol proves knowledge of winning strategies (Skolem/Herbrand functions) by reducing them to unsatisfiability or validity proofs in ZKP. On the QBFEVAL benchmark suite, these protocols verify ~79% of instances within 100 seconds, whenever Q-RES proofs or winning strategies are available. I will also discuss applications of ZKPs for PSPACE to partial equivalence checking in hardware, conformant planning in AI, and black-box checking in software analysis, together with our evaluation results on these domains. This work has been accepted to IEEE S&P 2026.
Bio: Ning Luo is a tenure-track Assistant Professor in the Department of Electrical and Computer Engineering at the University of Illinois Urbana-Champaign. She received her Ph.D. in Computer Science from Yale University in December 2022 and subsequently spent a year as a postdoctoral researcher at Northwestern University. Ning’s research integrates formal methods, automated reasoning, programming languages, and cryptography to achieve security, verifiability, and confidentiality in practical and challenging scenarios. She is a recipient of EECS Rising Stars (2023), the CCS Distinguished Paper Award (2022), and the Roberts Innovation Award (2023).