Research output: Other contribution › Net publication - Internet publication › Research › peer-review

**Computer-aided proofs for multiparty computation with active security.** / Haagh, Helene; Karbyshev, Aleksandr; Oechsner, Sabine; Spitters, Bas; Strub, Pierre-Yves.

Research output: Other contribution › Net publication - Internet publication › Research › peer-review

Haagh, H, Karbyshev, A, Oechsner, S, Spitters, B & Strub, P-Y 2018, *Computer-aided proofs for multiparty computation with active security*. arXiv.org.

Haagh, H., Karbyshev, A., Oechsner, S., Spitters, B., & Strub, P-Y. (2018, Jun 19). Computer-aided proofs for multiparty computation with active security. *arXiv.org*. Computer Security Foundations

Haagh H, Karbyshev A, Oechsner S, Spitters B, Strub P-Y. 2018. Computer-aided proofs for multiparty computation with active security. arXiv.org. 13 p.

Haagh, Helene et al., *Computer-aided proofs for multiparty computation with active security*, (Computer Security Foundations)., arXiv.org, 2018.

Haagh H, Karbyshev A, Oechsner S, Spitters B, Strub P-Y. Computer-aided proofs for multiparty computation with active security. 2018. 13 p.

Haagh, Helene ; Karbyshev, Aleksandr ; Oechsner, Sabine ; Spitters, Bas ; Strub, Pierre-Yves. / **Computer-aided proofs for multiparty computation with active security**. 2018. arXiv.org. 13 p. (Computer Security Foundations).

@misc{b4747684f521409aadab78797911722b,

title = "Computer-aided proofs for multiparty computation with active security",

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 its 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 be 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 in the passive case the non-interference-based definition is equivalent to a standard game-based security definition. For the active case we provide a new NI definition, which we call input independence.",

keywords = "cs.LO, cs.CR",

author = "Helene Haagh and Aleksandr Karbyshev and Sabine Oechsner and Bas Spitters and Pierre-Yves Strub",

year = "2018",

month = "6",

day = "19",

language = "English",

publisher = "arXiv.org",

type = "Other",

}

TY - ICOMM

T1 - Computer-aided proofs for multiparty computation with active security

AU - Haagh, Helene

AU - Karbyshev, Aleksandr

AU - Oechsner, Sabine

AU - Spitters, Bas

AU - Strub, Pierre-Yves

PY - 2018/6/19

Y1 - 2018/6/19

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 its 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 be 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 in the passive case the non-interference-based definition is equivalent to a standard game-based security definition. For the active case we provide a new NI definition, which we call input independence.

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 its 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 be 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 in the passive case the non-interference-based definition is equivalent to a standard game-based security definition. For the active case we provide a new NI definition, which we call input independence.

KW - cs.LO

KW - cs.CR

M3 - Net publication - Internet publication

PB - arXiv.org

ER -