Proving UNSAT in Zero Knowledge
Proving UNSAT in Zero Knowledge
复制标题
零知识证明 UNSAT
DOI：
10.1145/3548606.3559373
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Wang, Xiao
中科院分区：
文献类型：
--
作者：
Luo, Ning;Antonopoulos, Timos;Harris, William R.;Piskac, Ruzica;Tromer, Eran;Wang, Xiao
零知识（ZK）协议使一方能够向其他方证明它知道一个事实，而不透露任何关于这种知识的证据的信息。NP中的所有问题都存在ZK协议，最近的工作开发了高效的协议，用于证明布尔公式，电路和其他NP形式主义的满足分配的知识。这项工作显示了一个有效的协议，用于匡威的：证明公式在ZK中不可满足（当证明者证明非ZK证明时）。一个直接的实际应用是有效地证明秘密程序的安全性，其关键思想是在ZK中证明不可满足归结证明的有效性。这是有效地实现使用代数表示，利用分辨率证明的结构表示公式子句作为低次多项式，结合ZK随机访问参数。我们实现了我们的协议，并使用它来证明在标准验证基准，包括Linux内核驱动程序和英特尔密码模块的组合问题和程序正确性条件编码公式的不可满足性。结果表明，我们的协议具有实用性，并且其基于非平凡编码的积极优化显着提高了实际性能。
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 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.
登录
查看更多内容
正确程序执行的近线性时间零知识证明
DOI：
10.1007/978-3-030-03326-2_20
发表时间：
2018
期刊：
Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security
影响因子：
--
作者：
Jonathan Bootle;Andrea Cerulli;Jens Groth;S. K. Jakobsen;Mary Maller
通讯作者：
Mary Maller
DOI：
--
发表时间：
2020
期刊：
IACR Cryptol. ePrint Arch.
影响因子：
--
作者：
Joseph Bonneau;Izaak Meckler;V. Rao;Evan Shapiro
通讯作者：
Joseph Bonneau;Izaak Meckler;V. Rao;Evan Shapiro
具有次线性摊余成本的非代数语句的高效零知识证明
影响因子：
19
作者：
Zhangxiang Hu;Payman Mohassel;Mike Rosulek
通讯作者：
Mike Rosulek
RAM 程序的次线性零知识论证
DOI：
--
发表时间：
2017
期刊：
International Conference on the Theory and Application of Cryptographic Techniques
影响因子：
--
作者：
Payman Mohassel;Mike Rosulek;Alessandra Scafuro
通讯作者：
Alessandra Scafuro
DOI：
10.1109/sp40001.2021.00089
发表时间：
2021-05
期刊：
2021 IEEE Symposium on Security and Privacy (SP)
影响因子：
--
作者：
David Heath;Yibin Yang;David Devecsery;V. Kolesnikov
通讯作者：
David Heath;Yibin Yang;David Devecsery;V. Kolesnikov