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

### License

BSD License

### Topics

- Computer science/Security

### Session Multi_Party_Computation

- Cyclic_Group_Ext
- Number_Theory_Aux
- Uniform_Sampling
- Semi_Honest_Def
- OT_Functionalities
- ETP
- ETP_OT
- ETP_RSA_OT
- Noar_Pinkas_OT
- OT14
- GMW
- Secure_Multiplication
- DH_Ext
- Malicious_Defs
- Malicious_OT

### Depends on

- Game-based cryptography in HOL

## Cite

×

Multi_Party_Computation-AFP

    @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{https://isa-afp.org/entries/Multi_Party_Computation.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- May 10, 2019 : Isabelle2018