针对NP关系的机器检验零知识证明：MPC-in-the-Head的形式化验证安全证明与实现
密码学与安全
2021-05-21 v3
摘要
MPC-in-the-Head（MitH）是一个通用框架，允许从安全多方计算（MPC）协议构造针对一般NP关系的高效零知识协议。在本文中，我们给出了这一变换的首个机器检验实现。我们首先对MitH进行EasyCrypt形式化，该形式化保持MitH的模块化结构，并可用任意满足标准安全性概念的MPC协议实例化，这使我们能够借助现有的机器检验的基于秘密共享的MPC协议开发成果。所得的具体ZK协议在EasyCrypt中被证明安全且正确。利用最近开发的EasyCrypt代码提取机制，我们综合出了该协议的形式化验证实现，并对其进行基准测试以了解我们的形式化选择与代码提取机制所带来的开销。
引用
@article{arxiv.2104.05516,
title = {Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head},
author = {José Carlos Bacelar Almeida and Manuel Barbosa and Karim Eldefrawy and Stéphane Graham-Lengrand and Hugo Pacheco and Vitor Pereira},
journal= {arXiv preprint arXiv:2104.05516},
year = {2021}
}