### Abstract

We formalizes two protocols from a privacy-preserving machine-learning framework based on ABY3, a particular three-party computation framework where inputs are systematically ‘reshared’ without being considered as privacy leakage. In particular, we consider the multiplication protocol and the array shuffling protocol, both based on ABY3's additive secret sharing scheme. We proved their security in the semi-honest setting under the ideal/real simulation paradigm. These two proof-of-concept opens the door to further verification of more protocols within the framework.

### License

BSD License

### Topics

- Computer science/Security

### Session ABY3_Protocols

- Finite_Number_Type
- Additive_Sharing
- Spmf_Common
- Sharing_Lemmas
- Shuffle
- Multiplication
- Multiplication_Synthesization

### Depends on

- CryptHOL

## Cite

×

ABY3_Protocols-AFP

    @article{ABY3_Protocols-AFP,
      author  = {Shuwei Hu},
      title   = {ABY3 Multiplication and Array Shuffling},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/ABY3_Protocols.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Feb 5, 2023 : Isabelle2022