{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T19:12:37Z","timestamp":1769973157585,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":55,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,30]],"date-time":"2017-10-30T00:00:00Z","timestamp":1509321600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["FCT-PD\/BD\/113967\/2015 and UID\/EEA\/50014\/2013"],"award-info":[{"award-number":["FCT-PD\/BD\/113967\/2015 and UID\/EEA\/50014\/2013"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","award":["POCI-01-01 45-FEDER-006961"],"award-info":[{"award-number":["POCI-01-01 45-FEDER-006961"]}],"id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N000141210914 and N000141512750"],"award-info":[{"award-number":["N000141210914 and N000141512750"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,30]]},"DOI":"10.1145\/3133956.3134017","type":"proceedings-article","created":{"date-parts":[[2017,10,27]],"date-time":"2017-10-27T12:48:18Z","timestamp":1509108498000},"page":"1989-2006","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["A Fast and Verified Software Stack for Secure Function Evaluation"],"prefix":"10.1145","author":[{"given":"Jos\u00e9 Bacelar","family":"Almeida","sequence":"first","affiliation":[{"name":"INESC TEC & Universidade do Minho, Braga, Portugal"}]},{"given":"Manuel","family":"Barbosa","sequence":"additional","affiliation":[{"name":"INESC TEC & FCUP Universidade do Porto, Porto, Portugal"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}]},{"given":"Fran\u00e7ois","family":"Dupressoir","sequence":"additional","affiliation":[{"name":"University of Surrey, Guildford, United Kingdom"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"Inria Sophia-Antipolis, Nice, France"}]},{"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}]},{"given":"Vitor","family":"Pereira","sequence":"additional","affiliation":[{"name":"INESC TEC & FCUP Universidade do Porto, Porto, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2017,10,30]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-013-0057-3"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","unstructured":"Jos\u00e9 Bacelar Almeida Manuel Barbosa Gilles Barthe and Francois Dupressoir. 2013. Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. In ACM CCS. 10.1145\/2508859.2516652","DOI":"10.1145\/2508859.2516652"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-52993-5_9"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_2_6_1","unstructured":"Michael Backes Matteo Maffei and Esfandiar Mohammadi. 2010. Computationally Sound Abstraction and Verification of Secure Multi-Party Computations. In FSTTCS."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe C\u00e9dric Fournet Benjamin Gr\u00e9goire Pierre-Yves Strub Nikhil Swamy and Santiago Zanella-B\u00e9guelin. 2014. Probabilistic Relational Verification for Cryptographic Implementations. In POPL. To appear. 10.1145\/2535838.2535847","DOI":"10.1145\/2535838.2535847"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Benjamin Gr\u00e9goire Sylvain Heraud and Santiago Zanella-B\u00e9guelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In CRYPTO. 10.1007\/978-3-642-22792-9_5","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/100216.100287"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.39"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382279"},{"key":"e_1_3_2_2_13_1","unstructured":"Mihir Bellare and Silvio Micali. 1989. Non-Interactive Oblivious Transfer and Applications. In CRYPTO."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11761679_25"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455804"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","unstructured":"Rikke Bendlin Ivan Damg\u00e5rd Claudio Orlandi and Sarah Zakarias. 2011. Semi-homomorphic Encryption and Multiparty Computation. In EUROCRYPT. 169--188. 10.1007\/978-3-642-20465-4_11","DOI":"10.1007\/978-3-642-20465-4_11"},{"key":"e_1_3_2_2_17_1","volume-title":"Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium, USENIX Security 15","author":"Beringer Lennart","year":"2015","unstructured":"Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium, USENIX Security 15, Washington, D.C., USA, August 12-14, 2015., Jaeyeon Jung and Thorsten Holz (Eds.). USENIX Association, 207--221. https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/beringer"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.1005"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"crossref","unstructured":"Bruno Blanchet. 2012. Security Protocol Verification: Symbolic and Computational Models. In POST.","DOI":"10.1007\/978-3-642-28641-4_2"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88313-5_13"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Sally Browning and Philip Weaver. 2010. Designing Tunable Verifiable Cryptographic Hardware Using Cryptol. (2010).","DOI":"10.1007\/978-1-4419-1539-9_4"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","unstructured":"David Cad\u00e9 and Bruno Blanchet. 2013. Proved Generation of Implementations from Computationally Secure Protocol Specifications. In POST. 10.1007\/978-3-642-36830-1_4","DOI":"10.1007\/978-3-642-36830-1_4"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53015-3_15"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","unstructured":"Morten Dahl and Ivan Damg\u00e5rd. 2014. Universally Composable Symbolic Analysis for Two-Party Protocols Based on Homomorphic Encryption. In EUROCRYPT. 10.1007\/978-3-642-55220-5_38","DOI":"10.1007\/978-3-642-55220-5_38"},{"key":"e_1_3_2_2_27_1","volume-title":"Peter Sebastian Nordholt, and Tomas Toft","author":"Damg\u00e5rd Ivan","year":"2016","unstructured":"Ivan Damg\u00e5rd, Kasper Damg\u00e5rd, Kurt Nielsen, Peter Sebastian Nordholt, and Tomas Toft. 2016. Confidential Benchmarking based on Multiparty Computation. In Financial Cryptography 2016. In print."},{"key":"e_1_3_2_2_28_1","volume-title":"Smart","author":"Damg\u00e5rd Ivan","year":"2013","unstructured":"Ivan Damg\u00e5rd, Marcel Keller, Enrique Larraia, Valerio Pastro, Peter Scholl, and Nigel P. Smart. 2013. Practical Covertly Secure MPC for Dishonest Majority - Or: Breaking the SPDZ Limits. In ESORICS. 1--18."},{"key":"e_1_3_2_2_29_1","first-page":"695","article-title":"Gate-scrambling Revisited - or: The TinyTable protocol for 2-Party Secure Computation","volume":"2016","author":"Damg\u00e5rd Ivan","year":"2016","unstructured":"Ivan Damg\u00e5rd, Jesper Buus Nielsen, Michael Nielsen, and Samuel Ranellucci. 2016. Gate-scrambling Revisited - or: The TinyTable protocol for 2-Party Secure Computation. IACR Cryptology ePrint Archive 2016 (2016), 695. http:\/\/eprint.iacr.org\/2016\/695","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32009-5_38"},{"key":"e_1_3_2_2_31_1","volume-title":"SCAPI: The Secure Computation Application Programming Interface. Cryptology ePrint Archive, Report 2012\/629.","author":"Ejgenberg Yael","year":"2012","unstructured":"Yael Ejgenberg, Moriya Farbstein, Meital Levy, and Yehuda Lindell. 2012. SCAPI: The Secure Computation Application Programming Interface. Cryptology ePrint Archive, Report 2012\/629. (2012)."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.26"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","unstructured":"C\u00e9dric Fournet Markulf Kohlweiss and Pierre-Yves Strub. 2011. Modular code-based cryptographic verification. In ACM CCS. 10.1145\/2046707.2046746","DOI":"10.1145\/2046707.2046746"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54807-9_15"},{"key":"e_1_3_2_2_36_1","first-page":"181","article-title":"A plausible approach to computer-aided cryptographic proofs","volume":"2005","author":"Halevi Shai","year":"2005","unstructured":"Shai Halevi. 2005. A plausible approach to computer-aided cryptographic proofs. IACR Cryptology ePrint Archive 2005 (2005), 181.","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866358"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866358"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","unstructured":"Andreas Holzer Martin Franz Stefan Katzenbeisser and Helmut Veith. 2012. Secure Two-party Computations in ANSI C. In ACM CCS. 10.1145\/2382196.2382278","DOI":"10.1145\/2382196.2382278"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Yan Huang David Evans Jonathan Katz and Lior Malka. 2011. Faster Secure Two-party Computation Using Garbled Circuits. In USENIX Security.","DOI":"10.1007\/978-3-642-25560-1_2"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-130464"},{"key":"e_1_3_2_2_42_1","unstructured":"Vladimir Kolesnikov and Thomas Schneider. 2008. Improved Garbled Circuit: Free XOR Gates and Applications. In ICALP."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-008-9036-8"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9"},{"key":"e_1_3_2_2_46_1","volume-title":"Fairplay - Secure Two-Party Computation System. In USENIX Security Symposium, Matt Blaze (Ed.). USENIX, 287--302","author":"Malkhi Dahlia","year":"2004","unstructured":"Dahlia Malkhi, Noam Nisan, Benny Pinkas, and Yaron Sella. 2004. Fairplay - Secure Two-Party Computation System. In USENIX Security Symposium, Matt Blaze (Ed.). USENIX, 287--302. https:\/\/www.usenix.org\/publications\/proceedings\/?f[0]=im_group_audience%3A173"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"crossref","unstructured":"Moni Naor and Benny Pinkas. 2001. Efficient Oblivious Transfer Protocols. In SODA.","DOI":"10.1007\/3-540-44448-3_16"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32009-5_40"},{"key":"e_1_3_2_2_49_1","volume-title":"Reversible circuit compilation with space constraints. CoRR abs\/1510.00377","author":"Parent Alex","year":"2015","unstructured":"Alex Parent, Martin Roetteler, and Krysta Marie Svore. 2015. Reversible circuit compilation with space constraints. CoRR abs\/1510.00377 (2015). http:\/\/arxiv.org\/abs\/1510.00377"},{"key":"e_1_3_2_2_50_1","volume-title":"Pinocchio: Nearly Practical Verifiable Computation","author":"Parno Bryan","year":"2013","unstructured":"Bryan Parno, Jon Howell, Craig Gentry, and Mariana Raykova. 2013. Pinocchio: Nearly Practical Verifiable Computation. In IEEE S&P."},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_3_2_2_53_1","volume-title":"Wysteria: A Programming Language for Generic, Mixed-Mode Multiparty Computations","author":"Rastogi Aseem","year":"2014","unstructured":"Aseem Rastogi, Matthew A. Hammer, and Michael Hicks. 2014. Wysteria: A Programming Language for Generic, Mixed-Mode Multiparty Computations. In IEEE S&P."},{"key":"e_1_3_2_2_54_1","unstructured":"Aseem Rastogi Nikhil Swamy and Michael Hicks. 2016. WYS*: A Verified Language Extension for Secure Multi-party Computations. (2016). Manuscript."},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-56617-7_14"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","unstructured":"Andrew C. Yao. 1982. Protocols for secure computations. In FOCS. 10.1109\/SFCS.1982.38","DOI":"10.1109\/SFCS.1982.38"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2016.2547898"}],"event":{"name":"CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security","location":"Dallas Texas USA","acronym":"CCS '17","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134017","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134017","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134017","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:27Z","timestamp":1750212807000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134017"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,30]]},"references-count":55,"alternative-id":["10.1145\/3133956.3134017","10.1145\/3133956"],"URL":"https:\/\/doi.org\/10.1145\/3133956.3134017","relation":{},"subject":[],"published":{"date-parts":[[2017,10,30]]},"assertion":[{"value":"2017-10-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}