[isabelle] New in the AFP: Multi-Party Computation

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.