Paper 2019/922

A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation

Karim Eldefrawy and Vitor Pereira

Abstract

Secure Multiparty Computation (MPC) enables a group of $n$ distrusting parties to jointly compute a function using private inputs. MPC guarantees correctness of computation and confidentiality of inputs if no more than a threshold $t$ of the parties are corrupted. Proactive MPC (PMPC) addresses the stronger threat model of a mobile adversary that controls a changing set of parties (but only up to $t$ at any instant), and may eventually corrupt all $n$ parties over a long time. This paper takes a first stab at developing high-assurance implementations of (P)MPC. 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 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 the required (abstract) protocols in EasyCrypt. We also develop a new tool-chain to extract high-assurance executable implementations of protocols formalized and verified in EasyCrypt. Our tool-chain uses Why as an intermediate tool, and enables us to extract executable code from our (P)MPC formalizations. We conduct an evaluation of the extracted executables by comparing their performance to 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.

Metadata
Available format(s)
PDF
Publication info
Published elsewhere. Minor revision.ACM CCS 2019
DOI
10.1145/3319535.3354205
Keywords
Secure Multi-Party ComputationVerified ImplementationHigh-Assurance Cryptography
Contact author(s)
vitorm2p @ gmail com
History
2019-09-24: last of 3 revisions
2019-08-13: received
See all versions
Short URL
https://ia.cr/2019/922
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2019/922,
      author = {Karim Eldefrawy and Vitor Pereira},
      title = {A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation},
      howpublished = {Cryptology ePrint Archive, Paper 2019/922},
      year = {2019},
      doi = {10.1145/3319535.3354205},
      note = {\url{https://eprint.iacr.org/2019/922}},
      url = {https://eprint.iacr.org/2019/922}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.