Computer-Aided Proofs for Multiparty Computation with Active Security

TY - GEN

T1 - Computer-Aided Proofs for Multiparty Computation with Active Security

AU - Haagh, H.

AU - Karbyshev, A.

AU - Oechsner, S.

AU - Spitters, B.

AU - Strub, P.

N1 - Conference code: 31

PY - 2018/7/1

Y1 - 2018/7/1

N2 - 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.

AB - 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.

KW - Additives

KW - Cryptography

KW - EasyCrypt

KW - MPC

KW - Maurer's MPC protocol

KW - Probabilistic logic

KW - Protocols

KW - Secure-multi-party-computation,-security-definitions,-modelling-secure-protocols,-formal-verification,-easycrypt,-computer-aided-security-proofs

KW - Standards

KW - Tools

KW - active security

KW - ambient general purpose higher-order logic

KW - computer proof assistants

KW - computer-aided proofs

KW - data privacy

KW - digital signatures

KW - embedded language

KW - formal verification

KW - general cryptographic technique

KW - general polynomial functions

KW - multiparty computation

KW - polynomials

KW - probabilistic programming

KW - program equivalence

KW - programming language community

KW - programming languages

KW - proof assistant

KW - public key cryptography

KW - public-key encryption

KW - secret sharing schemes

KW - security definition

KW - theorem proving

UR - http://www.scopus.com/inward/record.url?scp=85052137985&partnerID=8YFLogxK

U2 - 10.1109/CSF.2018.00016

DO - 10.1109/CSF.2018.00016

M3 - Article in proceedings

SN - 978-1-5386-6681-4

VL - 2018

T3 - Proceedings of the IEEE Computer Security Foundations Symposium

SP - 119

EP - 131

BT - Proceedings - IEEE 31st Computer Security Foundations Symposium, CSF 2018

PB - IEEE

CY - Oxford

T2 - 2018 IEEE 31st Computer Security Foundations Symposium (CSF)

Y2 - 9 July 2018 through 12 July 2018

ER -