research-article

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

Authors:

David Aspinall,

Adrià GascónAuthors Info & Claims

CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 229 - 243

https://doi.org/10.1145/3372885.3373815

Published: 22 January 2020 Publication History

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₂¹) — a fundamental MPC protocol — in both the semi-honest and malicious models. We then extend our semi-honest formalisation to OT₄¹ 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₂¹ 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.

References

[1]

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, and Vitor Pereira. 2017. A Fast and Verified Software Stack for Secure Function Evaluation. In ACM Conference on Computer and Communications Security. ACM, 1989–2006.

Digital Library

[2]

David Aspinall and David Butler. 2019. Multi-Party Computation. Archive of Formal Proofs 2019 (2019).

[3]

G Barthe, B Grégoire, and S Zanella Béguelin. 2009. Formal certification of code-based cryptographic proofs. In POPL. ACM, 90–101.

[4]

G Barthe, B Grégoire, S Heraud, and S Zanella Béguelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO (Lecture Notes in Computer Science), Vol. 6841. Springer, 71– 90.

[5]

David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar. 2017. CryptHOL: Game-based Proofs in Higher-order Logic. IACR Cryptology ePrint Archive 2017 (2017), 753.

[6]

Mihir Bellare and Phillip Rogaway. 2006. The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. In EUROCRYPT (Lecture Notes in Computer Science), Vol. 4004. Springer, 409–426.

[7]

Bruno Blanchet. 2008. A Computationally Sound Mechanized Prover for Security Protocols. IEEE Trans. Dependable Sec. Comput. 5, 4 (2008), 193–207.

Digital Library

[8]

Dan Bogdanov, Sven Laur, and Jan Willemson. 2008. Sharemind: A Framework for Fast Privacy-Preserving Computations. In ESORICS (Lecture Notes in Computer Science), Vol. 5283. Springer, 192–206.

[9]

Peter Bogetoft, Dan Lund Christensen, Ivan Damgård, Martin Geisler, Thomas P. Jakobsen, Mikkel Krøigaard, Janus Dam Nielsen, Jesper Buus Nielsen, Kurt Nielsen, Jakob Pagter, Michael I. Schwartzbach, and Tomas Toft. 2009. Secure Multiparty Computation Goes Live. In Financial Cryptography (Lecture Notes in Computer Science), Vol. 5628. Springer, 325–343.

Digital Library

[10]

David Butler and David Aspinall. 2019. Multi Party Computation. Archive of Formal Proofs (2019). https://www.isa-afp.org/entries/ Multi_Party_Computation.html, Formal proof development.

[11]

David Butler, David Aspinall, and Adrià Gascón. 2017. How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation. In ITP (Lecture Notes in Computer Science), Vol. 10499. Springer, 114–130.

[12]

David Butler, David Aspinall, and Adrià Gascón. 2019. On the Formalisation of Σ -Protocols and Commitment Schemes. In POST (Lecture Notes in Computer Science), Vol. 11426. Springer, 175–196.

[13]

David Butler and Andreas Lochbihler. 2019. Sigma Protocols and Commitment Schemes. Archive of Formal Proofs (2019). https:// www.isa-afp.org/entries/Sigma_Commit_Crypto.html, Formal proof development.

[14]

David Butler, Andreas Lochbihler, David Aspinall, and Adrià Gascón. 2019. Formalising Σ-Protocols and Commitment Schemes using CryptHOL. IACR Cryptology ePrint Archive 2019 (2019), 1185.

[15]

Ran Canetti. 2001. Universally Composable Security: A New Paradigm for Cryptographic Protocols. In FOCS. IEEE Computer Society, 136– 145.

[16]

Ran Canetti, Alley Stoughton, and Mayank Varia. 2019. EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security. In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF 2019) . IEEE Computer Society, Hoboken, NJ, USA.

[17]

Shimon Even, Oded Goldreich, and Abraham Lempel. 1985. A Randomized Protocol for Signing Contracts. Commun. ACM 28, 6 (1985), 637–647.

Digital Library

[18]

Oded Goldreich. 2001. The Foundations of Cryptography - Volume 1, Basic Techniques . Cambridge University Press.

[19]

Oded Goldreich. 2004. The Foundations of Cryptography - Volume 2, Basic Applications . Cambridge University Press.

[20]

Oded Goldreich, Silvio Micali, and Avi Wigderson. 1987. How to Play any Mental Game or A Completeness Theorem for Protocols with Honest Majority. In STOC. ACM, 218–229.

[21]

Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, and Pierre-Yves Strub. 2018. Computer-Aided Proofs for Multiparty Computation with Active Security. In CSF. IEEE Computer Society, 119–131.

[22]

Carmit Hazay and Yehuda Lindell. 2010. Efficient Secure Two-Party Protocols - Techniques and Constructions . Springer.

[23]

John Launchbury, Dave Archer, Thomas DuBuisson, and Eric Mertens. 2014. Application-Scale Secure Multiparty Computation. In ESOP (Lecture Notes in Computer Science), Vol. 8410. Springer, 8–26.

[24]

Yehuda Lindell. 2017. How to Simulate It - A Tutorial on the Simulation Proof Technique. In Tutorials on the Foundations of Cryptography. Springer International Publishing, 277–346.

[25]

Andreas Lochbihler. [n. d.]. CryptHOL. Archive of Formal Proofs 2017 ([n. d.]).

[26]

Andreas Lochbihler. 2016. Probabilistic Functions and Cryptographic Oracles in Higher Order Logic. In ESOP (Lecture Notes in Computer Science), Vol. 9632. Springer, 503–531.

[27]

Andreas Lochbihler and S. Reza Sefidgar. [n. d.]. Constructive Cryptography in HOL. Archive of Formal Proofs 2018 ([n. d.]).

[28]

Andreas Lochbihler, S. Reza Sefidgar, David A. Basin, and Ueli Maurer. 2019. Formalizing Constructive Cryptography using CryptHOL. In Computer Security Foundations (CSF 2019) . IEEE, 152–166.

[29]

Andreas Lochbihler, S. Reza Sefidgar, and Bhargav Bhatt. [n. d.]. Gamebased cryptography in HOL. Archive of Formal Proofs 2017 ([n. d.]).

[30]

Ueli M. Maurer. 2006. Secure multi-party computation made simple. Discrete Applied Mathematics 154, 2 (2006), 370–381.

[31]

Moni Naor and Benny Pinkas. 2001. Efficient oblivious transfer protocols. In SODA. ACM/SIAM, 448–457.

[32]

A Petcher and G Morrisett. 2015. The Foundational Cryptography Framework. In POST (Lecture Notes in Computer Science), Vol. 9036. Springer, 53–72.

[33]

Adi Shamir. 1979. How to Share a Secret. Commun. ACM 22, 11 (1979), 612–613.

Digital Library

[34]

Victor Shoup. 2004. Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive 2004 (2004), 332.

[35]

Andrew Chi-Chih Yao. 1982. Protocols for Secure Computations (Extended Abstract). In FOCS. IEEE Computer Society, 160–164.

[36]

Andrew Chi-Chih Yao. 1986. How to Generate and Exchange Secrets (Extended Abstract). In FOCS. IEEE Computer Society, 162–167.

Cited By

Xie XLi YZhang WWang TXu SZhu JSong Y(2024)GAuV: A Graph-Based Automated Verification Framework for Perfect Semi-Honest Security of Multiparty Computation Protocols2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00131(484-502)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00131
Blanchet B(2024)Dealing with Dynamic Key Compromise in Crypto Verif2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00015(495-510)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00015
Kosaian KTan YRozier K(2024)Formalizing Coppersmith’s Method in Isabelle/HOLIntelligent Computer Mathematics10.1007/978-3-031-66997-2_8(127-145)Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-66997-2_8
Show More Cited By

Index Terms

Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL
1. Security and privacy
  1. Formal methods and theory of security
    1. Formal security models
    2. Logic and verification

Recommendations

Computationally Secure Oblivious Transfer

We describe new computationally secure protocols of 1-out-of-N oblivious transfer, k-out-of-N oblivious transfer, and oblivious transfer with adaptive queries. The protocols are very efficient compared with solutions based on generic two-party ...
Semi-honest to malicious oblivious transfer: the black-box way
TCC'08: Proceedings of the 5th conference on Theory of cryptography

Until recently, all known constructions of oblivious transfer protocols based on general hardness assumptions had the following form. First, the hardness assumption is used in a black-box manner (i.e., the construction uses only the input/output ...
Oblivious Transfer Based on Key Exchange

Key-exchange protocols have been overlooked as a possible means for implementing oblivious transfer (OT). In this article, we present protocols for mutual exchange of secrets, 1-out-of-2 OT and coin-flipping similar to the Diffie-Hellman protocol using ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2020

381 pages

ISBN:9781450370974

DOI:10.1145/3372885

Program Chairs:
Jasmin Blanchette
Universiteit Amsterdam, Netherlands
,
Cătălin Hriţcu
Inria, France

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 January 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '20

Sponsor:

SIGPLAN

POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 20 - 21, 2020

LA, New Orleans, USA

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
135
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)6

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Xie XLi YZhang WWang TXu SZhu JSong Y(2024)GAuV: A Graph-Based Automated Verification Framework for Perfect Semi-Honest Security of Multiparty Computation Protocols2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00131(484-502)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00131
Blanchet B(2024)Dealing with Dynamic Key Compromise in Crypto Verif2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00015(495-510)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00015
Kosaian KTan YRozier K(2024)Formalizing Coppersmith’s Method in Isabelle/HOLIntelligent Computer Mathematics10.1007/978-3-031-66997-2_8(127-145)Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-66997-2_8
Gancher JSojakova KFan XShi EMorrisett G(2023)A Core Calculus for Equational Proofs of Cryptographic ProtocolsProceedings of the ACM on Programming Languages10.1145/35712237:POPL(866-892)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571223
He DDu RZhu SZhang MLiang KChan S(2022)Secure Logistic Regression for Vertical Federated LearningIEEE Internet Computing10.1109/MIC.2021.313885326:2(61-68)Online publication date: 1-Mar-2022
https://dl.acm.org/doi/10.1109/MIC.2021.3138853
Butler DLochbihler AAspinall DGascón A(2020)Formalising $$\varSigma $$-Protocols and Commitment Schemes Using CryptHOLJournal of Automated Reasoning10.1007/s10817-020-09581-wOnline publication date: 9-Sep-2020
https://doi.org/10.1007/s10817-020-09581-w

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents