September 27, 2024
Zero-Knowledge (ZK) protocols have been extensively researched in recent years, with a focus on finding efficient protocols for problems in NP, such as proving the satisfiability of a Boolean formula. However, less attention has been given to proving the unsatisfiability of a given formula without revealing any related proofs or even the formula itself. In this talk, I will talk about our work on a highly efficient zero-knowledge protocol for proving the unsatisfiability of Boolean formulas in propositional logic. Our protocol is based on polynomial equivalence checking, which allows for the verification of a resolution proof of unsatisfiability in a zero-knowledge setting. We have implemented this protocol and have demonstrated its effectiveness by checking the unsatisfiability of real-world formulae used for verifying system drivers within just 300 seconds. This work was published in the CCS 2022 and was awarded a distinguished paper award.
About Ning Luo
Ning Luo is an Assistant Professor in the Department of Electrical & Computer Engineering, University of Illinois Urbana-Champaign. She received her Ph.D. in Computer Science from Yale University in Dec 2022. After that, she was a postdoctoral fellow in the computer science department at Northwestern University. Ning’s research combines formal methods, automated reasoning, programming language, and cryptography to achieve security, verifiability, and confidentiality in practical and challenging scenarios. She is a recipient of EECS Rising Stars (2023), a CCS Distinguished Paper Award (2022), Yale Computer Science Distinguished Dissertation Award (2023), and Roberts Innovation Award (2023).