Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL

David Butler, David Aspinall, Adria Gascon

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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 (OT12 )-a fundamental MPC protocol-in both the semi-honest and malicious models. We then extend our semi-honest formalisation to OT14 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 OT12 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.

Original languageEnglish
Title of host publicationCPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020
EditorsJasmin Blanchette, Catalin Hritcu
PublisherAssociation for Computing Machinery, Inc
Pages229-243
Number of pages15
ISBN (Electronic)9781450370974
DOIs
Publication statusPublished - 20 Jan 2020
Event9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 - New Orleans, United States
Duration: 20 Jan 202021 Jan 2020

Publication series

NameCPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020

Conference

Conference9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020
Country/TerritoryUnited States
CityNew Orleans
Period20/01/2021/01/20

Keywords / Materials (for Non-textual outputs)

  • formal verification
  • Isabelle/HOL
  • Multi-Party Computation
  • Oblivious transfer

Fingerprint

Dive into the research topics of 'Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL'. Together they form a unique fingerprint.

Cite this