Cryptology ePrint Archive: Report 2021/1149

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head

José Bacelar Almeida and Manuel Barbosa and Manuel L Correia and Karim Eldefrawy and Stéphane Graham-Lengrand and Hugo Pacheco and Vitor Pereira

Abstract: MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero- knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of this transformation. We begin with an EasyCrypt formalization that preserves modular structure of the original MitH construction and can be instantiated with arbitrary MPC protocols, secret sharing and commitment schemes satisfying standard notions of security. We then formalize various suitable components, which we use to obtain full-fledged ZK protocols for general relations. We compare two approaches for obtaining verified executable implementations. The first approach realizes a fully automated extraction from EasyCrypt to OCaml. The second one reduces the trusted computing base (TCB) and provides better performance for the extracted executable by combining code extraction with manual formal verification of low-level components implemented in the Jasmin language. We conclude the paper with a discussion of the trade-off between formal verification effort and performance, and also discuss how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH.

Category / Keywords: implementation / Zero-Knowledge; Secure Multiparty Computation; Formal Verification

Original Publication (with minor differences): ACM CCS 2021
DOI:
10.1145/3460120.3484771

Date: received 9 Sep 2021, last revised 15 Sep 2021

Contact author: hpacheco at fc up pt, mbb at fc up pt, jba at di uminho pt, vitor pereira at sri com

Available format(s): PDF | BibTeX Citation

Version: 20210915:150632 (All versions of this report)

Short URL: ia.cr/2021/1149


[ Cryptology ePrint archive ]