Cryptology ePrint Archive: Report 2019/1449

Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL

David Butler and David Aspinall and Adria Gascon

Abstract: 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. We use CryptHOL to formalise a framework for reasoning about two party protocols using the security definitions for MPC. In particular we consider protocols for 1-out-of-2 Oblivious Transfer ($OT^1_2$) --- a fundamental MPC protocol --- in both the semi-honest and malicious models. We then extend our semi-honest formalisation to $OT^1_4$ which is a building block for our proof of security for the two party GMW protocol --- a protocol that can securely compute any Boolean circuit. The semi-honest $OT^1_2$ protocol we formalise is constructed from Extended Trapdoor Permutations (ETP), we first prove the general construction secure and then instantiate for the RSA collection of functions --- a known ETP. Our general proof assumes only the existence of ETPs, meaning any instantiated results come without needing to prove any security properties, only that the requirements of an ETP are met.

Category / Keywords: foundations / formal methods, MPC, oblivious transfer

Original Publication (in the same form): CPP 2020

Date: received 13 Dec 2019, last revised 13 Dec 2019

Contact author: dbutler at turing ac uk

Available format(s): PDF | BibTeX Citation

Version: 20191216:112629 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]