Computer-Aided Proofs for Multiparty Computation with Active Security

H. Haagh, A. Karbyshev, S. Oechsner, B. Spitters, P. Strub

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review

22 Citationer (Scopus)

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.

OriginalsprogEngelsk
TitelProceedings - IEEE 31st Computer Security Foundations Symposium, CSF 2018
Antal sider13
Vol/bind2018
UdgivelsesstedOxford
ForlagIEEE
Publikationsdato7 aug. 2018
Sider119-131
Artikelnummer8429300
ISBN (Trykt) 978-1-5386-6681-4
ISBN (Elektronisk)978-1-5386-6680-7
DOI
StatusUdgivet - 7 aug. 2018
Begivenhed2018 IEEE 31st Computer Security Foundations Symposium (CSF) - Oxford, Storbritannien
Varighed: 9 jul. 201812 jul. 2018
Konferencens nummer: 31
https://www.cs.ox.ac.uk/conferences/csf2018/

Konference

Konference2018 IEEE 31st Computer Security Foundations Symposium (CSF)
Nummer31
Land/OmrådeStorbritannien
ByOxford
Periode09/07/201812/07/2018
Internetadresse
NavnProceedings of the IEEE Computer Security Foundations Symposium
Nummer31
ISSN1940-1434

Emneord

  • Additives
  • Cryptography
  • EasyCrypt
  • MPC
  • Maurer's MPC protocol
  • Probabilistic logic
  • Protocols
  • Secure-multi-party-computation,-security-definitions,-modelling-secure-protocols,-formal-verification,-easycrypt,-computer-aided-security-proofs
  • Standards
  • Tools
  • active security
  • ambient general purpose higher-order logic
  • computer proof assistants
  • computer-aided proofs
  • data privacy
  • digital signatures
  • embedded language
  • formal verification
  • general cryptographic technique
  • general polynomial functions
  • multiparty computation
  • polynomials
  • probabilistic programming
  • program equivalence
  • programming language community
  • programming languages
  • proof assistant
  • public key cryptography
  • public-key encryption
  • secret sharing schemes
  • security definition
  • theorem proving

Fingeraftryk

Dyk ned i forskningsemnerne om 'Computer-Aided Proofs for Multiparty Computation with Active Security'. Sammen danner de et unikt fingeraftryk.

Citationsformater