Email Gateway (Aug 22 2022 at 19:49): Email Gateway (Aug 22 2022 at 19:49):From: Lawrence Paulson <lp15@cam.ac.uk>
I am happy to announce a new entry, thanks to David Aspinall and David Butler:
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.
Incidentally, a look at the theory browser shows the tangled hierarchy that this development depends on. The logical structures we can create now really are impressive!
You will find it online here: https://www.isa-afp.org/entries/Multi_Party_Computation.html
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC