{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:26:07Z","timestamp":1750220767133,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,1,20]],"date-time":"2020-01-20T00:00:00Z","timestamp":1579478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,1,20]]},"DOI":"10.1145\/3372885.3373815","type":"proceedings-article","created":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T13:09:33Z","timestamp":1579698573000},"page":"229-243","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Formalising oblivious transfer in the semi-honest and malicious model in CryptHOL"],"prefix":"10.1145","author":[{"given":"David","family":"Butler","sequence":"first","affiliation":[{"name":"Alan Turing Institute, UK \/ University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Aspinall","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adri\u00e0","family":"Gasc\u00f3n","sequence":"additional","affiliation":[{"name":"Google, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,1,22]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_1_1","DOI":"10.1145\/3133956.3134017"},{"key":"e_1_3_2_1_2_1","volume-title":"Multi-Party Computation. Archive of Formal Proofs 2019","author":"Aspinall David","year":"2019","unstructured":"David Aspinall and David Butler . 2019. Multi-Party Computation. Archive of Formal Proofs 2019 ( 2019 ). David Aspinall and David Butler. 2019. Multi-Party Computation. Archive of Formal Proofs 2019 (2019)."},{"doi-asserted-by":"crossref","unstructured":"G Barthe B Gr\u00e9goire and S Zanella B\u00e9guelin. 2009. Formal certification of code-based cryptographic proofs. In POPL. ACM 90\u2013101.  G Barthe B Gr\u00e9goire and S Zanella B\u00e9guelin. 2009. Formal certification of code-based cryptographic proofs. In POPL. ACM 90\u2013101.","key":"e_1_3_2_1_3_1","DOI":"10.1145\/1594834.1480894"},{"volume-title":"CRYPTO (Lecture Notes in Computer Science)","author":"Barthe G","unstructured":"G Barthe , B Gr\u00e9goire , S Heraud , and S Zanella B\u00e9guelin . 2011. Computer-Aided Security Proofs for the Working Cryptographer . In CRYPTO (Lecture Notes in Computer Science) , Vol. 6841 . Springer , 71\u2013 90. G Barthe, B Gr\u00e9goire, S Heraud, and S Zanella B\u00e9guelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO (Lecture Notes in Computer Science) , Vol. 6841. Springer, 71\u2013 90.","key":"e_1_3_2_1_4_1"},{"key":"e_1_3_2_1_5_1","first-page":"753","article-title":"CryptHOL: Game-based Proofs in Higher-order Logic","volume":"2017","author":"Basin David A.","year":"2017","unstructured":"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 . 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.","journal-title":"IACR Cryptology ePrint Archive"},{"volume-title":"EUROCRYPT (Lecture Notes in Computer Science)","author":"Bellare Mihir","unstructured":"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\u2013426. 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\u2013426.","key":"e_1_3_2_1_6_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1109\/TDSC.2007.1005"},{"key":"e_1_3_2_1_8_1","volume-title":"Sharemind: A Framework for Fast Privacy-Preserving Computations. In ESORICS (Lecture Notes in Computer Science)","author":"Bogdanov Dan","year":"2008","unstructured":"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\u2013206. 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\u2013206."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.1007\/978-3-642-03549-4_20"},{"key":"e_1_3_2_1_10_1","volume-title":"Multi Party Computation. Archive of Formal Proofs","author":"Butler David","year":"2019","unstructured":"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. 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."},{"volume-title":"ITP (Lecture Notes in Computer Science)","author":"Butler David","unstructured":"David Butler , David Aspinall , and Adri\u00e0 Gasc\u00f3n . 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\u2013130. David Butler, David Aspinall, and Adri\u00e0 Gasc\u00f3n. 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\u2013130.","key":"e_1_3_2_1_11_1"},{"volume-title":"POST (Lecture Notes in Computer Science)","author":"Butler David","unstructured":"David Butler , David Aspinall , and Adri\u00e0 Gasc\u00f3n . 2019. On the Formalisation of \u03a3 -Protocols and Commitment Schemes . In POST (Lecture Notes in Computer Science) , Vol. 11426 . Springer , 175\u2013196. David Butler, David Aspinall, and Adri\u00e0 Gasc\u00f3n. 2019. On the Formalisation of \u03a3 -Protocols and Commitment Schemes. In POST (Lecture Notes in Computer Science) , Vol. 11426. Springer, 175\u2013196.","key":"e_1_3_2_1_12_1"},{"key":"e_1_3_2_1_13_1","volume-title":"Sigma Protocols and Commitment Schemes. Archive of Formal Proofs","author":"Butler David","year":"2019","unstructured":"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. 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."},{"key":"e_1_3_2_1_14_1","first-page":"1185","article-title":"Formalising \u03a3-Protocols and Commitment Schemes using CryptHOL","volume":"2019","author":"Butler David","year":"2019","unstructured":"David Butler , Andreas Lochbihler , David Aspinall , and Adri\u00e0 Gasc\u00f3n . 2019 . Formalising \u03a3-Protocols and Commitment Schemes using CryptHOL . IACR Cryptology ePrint Archive 2019 (2019), 1185 . David Butler, Andreas Lochbihler, David Aspinall, and Adri\u00e0 Gasc\u00f3n. 2019. Formalising \u03a3-Protocols and Commitment Schemes using CryptHOL. IACR Cryptology ePrint Archive 2019 (2019), 1185.","journal-title":"IACR Cryptology ePrint Archive"},{"volume-title":"Universally Composable Security: A New Paradigm for Cryptographic Protocols","author":"Canetti Ran","unstructured":"Ran Canetti . 2001. Universally Composable Security: A New Paradigm for Cryptographic Protocols . In FOCS. IEEE Computer Society , 136\u2013 145. Ran Canetti. 2001. Universally Composable Security: A New Paradigm for Cryptographic Protocols. In FOCS. IEEE Computer Society, 136\u2013 145.","key":"e_1_3_2_1_15_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1109\/CSF.2019.00019"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_17_1","DOI":"10.1145\/3812.3818"},{"volume-title":"The Foundations of Cryptography -","author":"Goldreich Oded","unstructured":"Oded Goldreich . 2001. The Foundations of Cryptography - Volume 1 , Basic Techniques . Cambridge University Press . Oded Goldreich. 2001. The Foundations of Cryptography - Volume 1, Basic Techniques . Cambridge University Press.","key":"e_1_3_2_1_18_1"},{"volume-title":"The Foundations of Cryptography -","author":"Goldreich Oded","unstructured":"Oded Goldreich . 2004. The Foundations of Cryptography - Volume 2 , Basic Applications . Cambridge University Press . Oded Goldreich. 2004. The Foundations of Cryptography - Volume 2, Basic Applications . Cambridge University Press.","key":"e_1_3_2_1_19_1"},{"doi-asserted-by":"crossref","unstructured":"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\u2013229.  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\u2013229.","key":"e_1_3_2_1_20_1","DOI":"10.1145\/28395.28420"},{"volume-title":"Computer-Aided Proofs for Multiparty Computation with Active Security","author":"Haagh Helene","unstructured":"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\u2013131. 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\u2013131.","key":"e_1_3_2_1_21_1"},{"volume-title":"Efficient Secure Two-Party Protocols - Techniques and Constructions","author":"Hazay Carmit","unstructured":"Carmit Hazay and Yehuda Lindell . 2010. Efficient Secure Two-Party Protocols - Techniques and Constructions . Springer . Carmit Hazay and Yehuda Lindell. 2010. Efficient Secure Two-Party Protocols - Techniques and Constructions . Springer.","key":"e_1_3_2_1_22_1"},{"volume-title":"ESOP (Lecture Notes in Computer Science)","author":"Launchbury John","unstructured":"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\u201326. 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\u201326.","key":"e_1_3_2_1_23_1"},{"volume-title":"Tutorials on the Foundations of Cryptography","author":"Lindell Yehuda","unstructured":"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\u2013346. 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\u2013346.","key":"e_1_3_2_1_24_1"},{"unstructured":"Andreas Lochbihler. [n. d.]. CryptHOL. Archive of Formal Proofs 2017 ([n. d.]).  Andreas Lochbihler. [n. d.]. CryptHOL. Archive of Formal Proofs 2017 ([n. d.]).","key":"e_1_3_2_1_25_1"},{"volume-title":"ESOP (Lecture Notes in Computer Science)","author":"Lochbihler Andreas","unstructured":"Andreas Lochbihler . 2016. Probabilistic Functions and Cryptographic Oracles in Higher Order Logic . In ESOP (Lecture Notes in Computer Science) , Vol. 9632 . Springer , 503\u2013531. Andreas Lochbihler. 2016. Probabilistic Functions and Cryptographic Oracles in Higher Order Logic. In ESOP (Lecture Notes in Computer Science) , Vol. 9632. Springer, 503\u2013531.","key":"e_1_3_2_1_26_1"},{"doi-asserted-by":"crossref","unstructured":"Andreas Lochbihler and S. Reza Sefidgar. [n. d.]. Constructive Cryptography in HOL. Archive of Formal Proofs 2018 ([n. d.]).  Andreas Lochbihler and S. Reza Sefidgar. [n. d.]. Constructive Cryptography in HOL. Archive of Formal Proofs 2018 ([n. d.]).","key":"e_1_3_2_1_27_1","DOI":"10.1109\/CSF.2019.00018"},{"volume-title":"Computer Security Foundations (CSF 2019)","author":"Lochbihler Andreas","unstructured":"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\u2013166. 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\u2013166.","key":"e_1_3_2_1_28_1"},{"unstructured":"Andreas Lochbihler S. Reza Sefidgar and Bhargav Bhatt. [n. d.]. Gamebased cryptography in HOL. Archive of Formal Proofs 2017 ([n. d.]).  Andreas Lochbihler S. Reza Sefidgar and Bhargav Bhatt. [n. d.]. Gamebased cryptography in HOL. Archive of Formal Proofs 2017 ([n. d.]).","key":"e_1_3_2_1_29_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_30_1","DOI":"10.1016\/j.dam.2005.03.020"},{"volume-title":"Efficient oblivious transfer protocols","author":"Naor Moni","unstructured":"Moni Naor and Benny Pinkas . 2001. Efficient oblivious transfer protocols . In SODA. ACM\/SIAM , 448\u2013457. Moni Naor and Benny Pinkas. 2001. Efficient oblivious transfer protocols. In SODA. ACM\/SIAM, 448\u2013457.","key":"e_1_3_2_1_31_1"},{"volume-title":"POST (Lecture Notes in Computer Science)","author":"Petcher A","unstructured":"A Petcher and G Morrisett . 2015. The Foundational Cryptography Framework . In POST (Lecture Notes in Computer Science) , Vol. 9036 . Springer , 53\u201372. A Petcher and G Morrisett. 2015. The Foundational Cryptography Framework. In POST (Lecture Notes in Computer Science), Vol. 9036. Springer, 53\u201372.","key":"e_1_3_2_1_32_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_33_1","DOI":"10.1145\/359168.359176"},{"key":"e_1_3_2_1_34_1","first-page":"332","article-title":"Sequences of games: a tool for taming complexity in security proofs","volume":"2004","author":"Shoup Victor","year":"2004","unstructured":"Victor Shoup . 2004 . Sequences of games: a tool for taming complexity in security proofs . IACR Cryptology ePrint Archive 2004 (2004), 332 . Victor Shoup. 2004. Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive 2004 (2004), 332.","journal-title":"IACR Cryptology ePrint Archive"},{"volume-title":"Protocols for Secure Computations (Extended Abstract)","author":"Chi-Chih Yao Andrew","unstructured":"Andrew Chi-Chih Yao . 1982. Protocols for Secure Computations (Extended Abstract) . In FOCS. IEEE Computer Society , 160\u2013164. Andrew Chi-Chih Yao. 1982. Protocols for Secure Computations (Extended Abstract). In FOCS. IEEE Computer Society, 160\u2013164.","key":"e_1_3_2_1_35_1"},{"volume-title":"How to Generate and Exchange Secrets (Extended Abstract)","author":"Chi-Chih Yao Andrew","unstructured":"Andrew Chi-Chih Yao . 1986. How to Generate and Exchange Secrets (Extended Abstract) . In FOCS. IEEE Computer Society , 162\u2013167. Andrew Chi-Chih Yao. 1986. How to Generate and Exchange Secrets (Extended Abstract). In FOCS. IEEE Computer Society, 162\u2013167.","key":"e_1_3_2_1_36_1"}],"event":{"sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"acronym":"POPL '20","name":"POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"New Orleans LA USA"},"container-title":["Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373815","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372885.3373815","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:09Z","timestamp":1750200069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373815"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,20]]},"references-count":36,"alternative-id":["10.1145\/3372885.3373815","10.1145\/3372885"],"URL":"https:\/\/doi.org\/10.1145\/3372885.3373815","relation":{},"subject":[],"published":{"date-parts":[[2020,1,20]]},"assertion":[{"value":"2020-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}