Abstract
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.