MPC-in-the-Head (MitH) is a general framework that allows constructing efficient Zero Knowledge protocols for general NP-relations from secure multiparty computation (MPC) protocols. In this paper we give the first machine-checked implementation of this transformation. We begin with an EasyCrypt formalization of MitH that preserves the modular structure of MitH and can be instantiated with arbitrary MPC protocols that satisfy standard notions of security, which allows us to leverage an existing machine-checked secret-sharing-based MPC protocol development. The resulting concrete ZK protocol is proved secure and correct in EasyCrypt. Using a recently developed code extraction mechanism for EasyCrypt we synthesize a formally verified implementation of the protocol, which we benchmark to get an indication of the overhead associated with our formalization choices and code extraction mechanism.


翻译:MPC - 头部(MitH)是一个总框架,它允许为来自安全的多功能计算(MPC)协议的一般NP关系构建高效的零知识协议。 在本文中,我们首次对这项转变进行了机检。我们首先对MitH正式化进行了简单加密,以维护MitH的模块结构,并可以与满足标准安全概念的任意MPC协议同时进行,从而使我们能够利用现有的机器检查的基于秘密共享的MPC协议开发。由此产生的混凝土 ZK协议在“易用加密”中被证明是安全和正确的。我们利用最近开发的“易用加密”代码提取机制综合了经正式核实的协议实施过程,我们根据这一机制来衡量与我们正式化选择和代码提取机制相关的间接费用。

0
下载
关闭预览

相关内容

Google-EfficientNet v2来了!更快,更小,更强!
专知会员服务
18+阅读 · 2021年4月4日
专知会员服务
44+阅读 · 2020年10月31日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
【快讯】CVPR2020结果出炉,1470篇上榜, 你的paper中了吗?
FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
28+阅读 · 2019年10月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
已删除
将门创投
9+阅读 · 2017年7月28日
Arxiv
0+阅读 · 2021年7月8日
VIP会员
相关主题
相关资讯
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
已删除
将门创投
9+阅读 · 2017年7月28日
Top
微信扫码咨询专知VIP会员