Cryptology ePrint Archive: Report 2021/437

Formal security analysis of MPC-in-the-head zero-knowledge protocols

Nikolaj Sidorenco and Sabine Oechsner and Bas Spitters

Abstract: Zero-knowledge proofs allow a prover to convince a verifier of the veracity of a statement without revealing any other information. An interesting class of zero-knowledge protocols are those following the MPC-in-the-head paradigm (Ishai et al., STOC 07) which use secure multiparty computation (MPC) protocols as the basis. Efficient instances of this paradigm have emerged as an active research topic in the last years, starting with ZKBoo (Giacomelli et al., USENIX 16). Zero-knowledge protocols are a vital building block in the design of privacy-preserving technologies as well as cryptographic primitives like digital signature schemes that provide post-quantum security. This work investigates the security of zero-knowledge protocols following the MPC-in-the-head paradigm. We provide the first machine-checked security proof of such a protocol on the example of ZKBoo. Our proofs are checked in the EasyCrypt proof assistant. To enable a modular security proof, we develop a new security notion for the MPC protocols used in MPC-in-the-head zero-knowledge protocols. This allows us to recast existing security proofs in a black-box fashion which we believe to be of independent interest.

Category / Keywords: foundations / zero knowledge, secure multi-party computation, formal security analysis, easycrypt

Date: received 3 Apr 2021

Contact author: sidorenco at cs au dk,oechsner@cs au dk,spitters@cs au dk

Available format(s): PDF | BibTeX Citation

Version: 20210406:072713 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]