Write a Blog >>
Tue 21 Jan 2020 11:45 - 12:07 at Maurepas - Verified cryptography Chair(s): Adam Chlipala

Large scale implementations of Multi-Party Computation (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 general framework for reasoning about proofs of security of MPC. In particular we first 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 GMW protocol.

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

Conference Day
Tue 21 Jan

Displayed time zone: Saskatchewan, Central America change

11:45 - 12:30
Verified cryptographyCPP at Maurepas
Chair(s): Adam ChlipalaMassachusetts Institute of Technology
Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL
David ButlerAlan Turing Institute, David AspinallUniversity of Edinburgh, Adria GasconAlan Turing Institute
DOI Pre-print Media Attached
Verified Security of BLT Signature Scheme
Denis FirsovGuardtime AS, Ahto BuldasTallinn University of Technology, Ahto TruuGuardtime AS, Risto LaanojaGuardtime AS
DOI Pre-print Media Attached File Attached