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协议在“易用加密”中被证明是安全和正确的。我们利用最近开发的“易用加密”代码提取机制综合了经正式核实的协议实施过程,我们根据这一机制来衡量与我们正式化选择和代码提取机制相关的间接费用。