### Proving UNSAT in Zero Knowledge

Ning Luo, Timos Antonopoulos, William Harris, Ruzica Piskac, Eran Tromer, and Xiao Wang

##### Abstract

Zero-knowledge (ZK) protocols enable one party to prove to others that it knows a fact without revealing any information about the evidence for such knowledge. There exist ZK protocols for all problems in NP, and recent works developed highly efficient protocols for proving knowledge of satisfying assignments to Boolean formulas, circuits and other NP formalisms. This work shows an efficient protocol for the the converse: proving formula *unsatisfiability* in ZK (when the prover posses a non-ZK proof). An immediate practical application is efficiently proving safety of secret programs. The key insight is to prove, in ZK, the validity of *resolution proofs* of unsatisfiability. This is efficiently realized using an algebraic representation that exploits resolution proofs' structure to represent formula clauses as low-degree polynomials, combined with ZK random-access arguments. Only the proof's dimensions are revealed. We implemented our protocol and used it to prove unsatisfiability of formulas that encode combinatoric problems and program correctness conditions in standard verification benchmarks, including Linux kernel drivers and Intel cryptography modules. The results demonstrate both that our protocol has practical utility, and that its aggressive optimizations, based on non-trivial encodings, significantly improve practical performance.

Available format(s)
Category
Cryptographic protocols
Publication info
Preprint. MINOR revision.
Keywords
zero-knowledge proofs
Contact author(s)
ning luo @ yale edu
timos antonopoulos @ yale edu
wrharris @ galois com
ruzica piskac @ yale edu
et2555 @ columbia edu
wangxiao @ cs northwestern edu
History
Short URL
https://ia.cr/2022/206

CC BY

BibTeX

@misc{cryptoeprint:2022/206,
author = {Ning Luo and Timos Antonopoulos and William Harris and Ruzica Piskac and Eran Tromer and Xiao Wang},
title = {Proving UNSAT in Zero Knowledge},
howpublished = {Cryptology ePrint Archive, Paper 2022/206},
year = {2022},
note = {\url{https://eprint.iacr.org/2022/206}},
url = {https://eprint.iacr.org/2022/206}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.