Multi-Party Computation

Title:	Multi-Party Computation
Authors:	David Aspinall and David Butler
Submission date:	2019-05-09
Abstract:	We use CryptHOL to consider Multi-Party Computation (MPC) protocols. MPC was first considered by Yao in 1983 and recent advances in efficiency and an increased demand mean it is now deployed in the real world. Security is considered using the real/ideal world paradigm. We first define security in the semi-honest security setting where parties are assumed not to deviate from the protocol transcript. In this setting we prove multiple Oblivious Transfer (OT) protocols secure and then show security for the gates of the GMW protocol. We then define malicious security, this is a stronger notion of security where parties are assumed to be fully corrupted by an adversary. In this setting we again consider OT, as it is a fundamental building block of almost all MPC protocols.
BibTeX:	@article{Multi_Party_Computation-AFP, author = {David Aspinall and David Butler}, title = {Multi-Party Computation}, journal = {Archive of Formal Proofs}, month = may, year = 2019, note = {\url{http://isa-afp.org/entries/Multi_Party_Computation.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Game_Based_Crypto
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.