Computer-aided proofs for multiparty computation with active security

Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

Secure multi-party computation (MPC) is a general cryptographic technique that allows distrusting parties to compute a function of their individual inputs, while only revealing the output of the function. It has found applications in areas such as auctioning, email filtering, and secure teleconference. Given their importance, it is crucial that the protocols are specified and implemented correctly. In the programming language community, it has become good practice to use computer proof assistants to verify correctness proofs. In the field of cryptography, EasyCrypt is the state of the art proof assistant. It provides an embedded language for probabilistic programming, together with a specialized logic, embedded into an ambient general purpose higher-order logic. It allows us to conveniently express cryptographic properties. EasyCrypt has been used successfully on many applications, including public-key encryption, signatures, garbled circuits and differential privacy. Here we show for the first time that it can also be used to prove security of MPC against a malicious adversary. We formalize additive and replicated secret sharing schemes and apply them to Maurer's MPC protocol for secure addition and multiplication. Our method extends to general polynomial functions. We follow the insights from EasyCrypt that security proofs can often be reduced to proofs about program equivalence, a topic that is well understood in the verification of programming languages. In particular, we show that for a class of MPC protocols in the passive case the non-interference-based (NI) definition is equivalent to a standard simulation-based security definition. For the active case, we provide a new non-interference based alternative to the usual simulation-based cryptographic definition that is tailored specifically to our protocol.
Original languageEnglish
Title of host publicationProceedings - IEEE 31st Computer Security Foundations Symposium, CSF 2018
PublisherIEEE Computer Society
Pages119-131
ISBN (Print)9781538666807
DOIs
Publication statusPublished - 7 Aug 2018
Externally publishedYes
Event31st IEEE Computer Security Foundations Symposium, CSF 2018 - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Publication series

NameProceedings - IEEE Computer Security Foundations Symposium
ISSN (Print)1940-1434

Conference

Conference31st IEEE Computer Security Foundations Symposium, CSF 2018
Country/TerritoryUnited Kingdom
CityOxford
Period9/07/1812/07/18

Funding

Gilles Barthe showed us how non-interference can be used in the context of MPC for a passive adversary. Ivan Damgård helped us to understand MPC protocols and their security proofs. In the beginning of the project we profitted from discussions with Aslan Askarov, Michael Nielsen, and Mathias Pedersen. We are grateful to all of them. Helene Haagh and Sabine Oechsner were supported by the European Research Council (ERC) under the European Unions’s Horizon 2020 research and innovation programme under grant agreement No 669255 (MPCPRO), the Danish Independent Research Council under Grant-ID DFF-6108-00169 (FoCC), and the European Union’s Horizon 2020 research and innovation programme under grant agreement No 731583 (SODA). Bas Spitters was supported by the Guarded Homotopy Type Theory project, funded by the Villum Foundation, project number 12386.

FundersFunder number
FoCC
Natur og Univers, Det Frie ForskningsrådDFF-6108-00169
Villum Fonden12386
Horizon 2020 Framework Programme669255, 731583
European Research Council

    Fingerprint

    Dive into the research topics of 'Computer-aided proofs for multiparty computation with active security'. Together they form a unique fingerprint.

    Cite this