This paper takes a first stab at developing high-assurance implementations of (P)MPC. We present high-assurance implementations of (P)MPC protocols. We formalize in EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, several abstract and reusable variations of secret sharing and of (P)MPC protocols building on top of them. Using those, we prove a series of abstract theorems for the proactive setting. We implement and perform computer-checked security proofs of concrete instantiations of all required (abstract) protocols in EasyCrypt.
We also develop a new tool-chain to extract high-assurance executable implementations of protocols implemented and verified in EasyCrypt that uses Why3 as an intermediate tool. Using this new tool, we were able to extract code from our (P)MPC formalizations and to conduct a practical evaluation of it by comparing the performance obtained using our approach to the performance of manually implemented versions using Python-based Charm framework for prototyping cryptographic schemes. We argue that the small overhead of our high-assurance executables is a reasonable price to pay for the increased confidence about their correctness and security.
Category / Keywords: Secure Multi-Party Computation, Verified Implementation, High-Assurance Cryptography Original Publication (with minor differences): ACM CCS 2019 Date: received 13 Aug 2019, last revised 18 Aug 2019 Contact author: vitorm2p at gmail com Available format(s): PDF | BibTeX Citation Version: 20190818:224758 (All versions of this report) Short URL: ia.cr/2019/922