Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL
David Butler, David Aspinall, Adrià Gascón · 2020
Multi-Party Computation (MPC) allows multiple parties to compute a function together while keeping their inputs private. Large scale implementations of MPC protocols are becoming practical thus it is important to have strong guarantees for the whole development process, from the underlying cryptography to the implementation. Computer aided proofs are a way to provide such guarantees.