{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T15:10:46Z","timestamp":1777129846289,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":33,"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:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"funder":[{"name":"ERC","award":["CIRCUS"],"award-info":[{"award-number":["CIRCUS"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,30]]},"DOI":"10.1145\/3133956.3134043","type":"proceedings-article","created":{"date-parts":[[2017,10,27]],"date-time":"2017-10-27T12:48:18Z","timestamp":1509108498000},"page":"1789-1806","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":160,"title":["HACL*: A Verified Modern Cryptographic Library"],"prefix":"10.1145","author":[{"given":"Jean-Karim","family":"Zinzindohou\u00e9","sequence":"first","affiliation":[{"name":"INRIA, Paris, France"}]},{"given":"Karthikeyan","family":"Bhargavan","sequence":"additional","affiliation":[{"name":"INRIA, Paris, France"}]},{"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]},{"given":"Benjamin","family":"Beurdouche","sequence":"additional","affiliation":[{"name":"INRIA, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2017,10,30]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_3_2_2_2_1","first-page":"1241","article-title":"Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC","volume":"2015","author":"Almeida Jos\u00e9 Bacelar","year":"2015","unstructured":"Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and Franccois Dupressoir. 2015. Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. IACR Cryptology ePrint Archive Vol. 2015 (2015), 1241. http:\/\/eprint.iacr.org\/2015\/1241","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_3_2_2_3_1","volume-title":"Verifying Constant-Time Implementations. In USENIX Security Symposium. 53--70","author":"Almeida Jos\u00e9 Bacelar","year":"2016","unstructured":"Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franccois Dupressoir, and Michael Emmi 2016. Verifying Constant-Time Implementations. In USENIX Security Symposium. 53--70."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Gustavo Betarte Juan Campo Carlos Luna and David Pichardie 2014. System-level non-interference for constant-time cryptography Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security. ACM 1267--1279.","DOI":"10.1145\/2660267.2660283"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Benjamin Gr\u00e9goire Sylvain Heraud and Santiago Zanella B\u00e9guelin. 2011. Computer-aided security proofs for the working cryptographer Annual Cryptology Conference. 71--90.","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_3_2_2_7_1","unstructured":"David Benjamin. 2016. poly1305-x86.pl produces incorrect output. https:\/\/mta.openssl.org\/pipermail\/openssl-dev\/2016-March\/006161. (2016)."},{"key":"e_1_3_2_2_8_1","volume-title":"Verified Correctness and Security of OpenSSL HMAC USENIX Security Symposium. 207--221","author":"Beringer Lennart","unstructured":"Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel 2015. Verified Correctness and Security of OpenSSL HMAC USENIX Security Symposium. 207--221."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Daniel J. Bernstein. 2005. The Poly1305-AES Message-Authentication Code. In Fast Software Encryption (FSE). 32--49.","DOI":"10.1007\/11502760_3"},{"key":"e_1_3_2_2_10_1","volume-title":"Curve25519: new Diffie-Hellman speed records. Public Key Cryptography-PKC","author":"Bernstein Daniel J","year":"2006","unstructured":"Daniel J Bernstein. 2006. Curve25519: new Diffie-Hellman speed records. Public Key Cryptography-PKC 2006. Springer, 207--228."},{"key":"e_1_3_2_2_11_1","volume-title":"a variant of Salsa20","author":"Bernstein Daniel J","unstructured":"Daniel J Bernstein. 2008. ChaCha, a variant of Salsa20."},{"key":"e_1_3_2_2_12_1","unstructured":"Daniel J Bernstein Niels Duif Tanja Lange Peter Schwabe and Bo-Yin Yang. High-speed high-security signatures. Journal of Cryptographic Engineering (????) 1--13."},{"key":"e_1_3_2_2_13_1","volume-title":"The security impact of a new cryptographic library International Conference on Cryptology and Information Security in Latin America (LATINCRYPT)","author":"Bernstein Daniel J","unstructured":"Daniel J Bernstein, Tanja Lange, and Peter Schwabe. 2012. The security impact of a new cryptographic library International Conference on Cryptology and Information Security in Latin America (LATINCRYPT). Springer, 159--176."},{"key":"e_1_3_2_2_14_1","volume-title":"NEON crypto International Workshop on Cryptographic Hardware and Embedded Systems","author":"Bernstein Daniel J","unstructured":"Daniel J Bernstein and Peter Schwabe 2012. NEON crypto International Workshop on Cryptographic Hardware and Embedded Systems. Springer, 320--339."},{"key":"e_1_3_2_2_15_1","volume-title":"International Conference on Cryptology and Information Security in Latin America (LATINCRYPT). Springer, 64--83","author":"Bernstein Daniel J","year":"2014","unstructured":"Daniel J Bernstein, Bernard Van Gastel, Wesley Janssen, Tanja Lange, Peter Schwabe, and Sjaak Smetsers 2014. TweetNaCl: A crypto library in 100 tweets. In International Conference on Cryptology and Information Security in Latin America (LATINCRYPT). Springer, 64--83."},{"key":"e_1_3_2_2_16_1","volume-title":"ACM SIGPLAN International Conference on Functional Programming (ICFP).","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Catalin Hritcu, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Peng Wang, Santiago Zanella-B\u00e9guelin, and Jean-Karim Zinzindohou\u00e9. 2017. Verified Low-Level Programming Embedded in F*. ACM SIGPLAN International Conference on Functional Programming (ICFP)."},{"key":"e_1_3_2_2_17_1","volume-title":"Implementing TLS with Verified Cryptographic Security IEEE Symposium on Security & Privacy (Oakland). 445--462","author":"Bhargavan Karthikeyan","year":"2013","unstructured":"Karthikeyan Bhargavan, C\u00e9dric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub 2013. Implementing TLS with Verified Cryptographic Security IEEE Symposium on Security & Privacy (Oakland). 445--462."},{"key":"e_1_3_2_2_18_1","unstructured":"Hanno B\u00f6ck. 2016. Wrong results with Poly1305 functions. https:\/\/mta.openssl.org\/pipermail\/openssl-dev\/2016-March\/006413. (2016)."},{"key":"e_1_3_2_2_19_1","volume-title":"Vale: Verifying High-Performance Cryptographic Assembly Code Proceedings of the USENIX Security Symposium.","author":"Bond Barry","year":"2017","unstructured":"Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson 2017. Vale: Verifying High-Performance Cryptographic Assembly Code Proceedings of the USENIX Security Symposium."},{"key":"e_1_3_2_2_20_1","volume-title":"Practical realisation and elimination of an ECC-related software bug attack. Topics in Cryptology--CT-RSA","author":"Brumley Billy B","year":"2012","unstructured":"Billy B Brumley, Manuel Barbosa, Dan Page, and Frederik Vercauteren 2012. Practical realisation and elimination of an ECC-related software bug attack. Topics in Cryptology--CT-RSA 2012. Springer, 171--186."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660370"},{"key":"e_1_3_2_2_22_1","unstructured":"Quynh H Dang. 2008. The Keyed-Hash Message Authentication Code (HMAC). NIST FIPS-198--1. (2008)."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"crossref","unstructured":"A. Delignat-Lavaud C. Fournet M. Kohlweiss J. Protzenko A. Rastogi N. Swamy S. Zanella-Beguelin K. Bhargavan J. Pan and J. K. Zinzindohoue 2017. Implementing and Proving the TLS 1.3 Record Layer IEEE Symposium on Security and Privacy (Oakland). 463--482.","DOI":"10.1109\/SP.2017.58"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Martin Goll and Shay Gueron 2014. Vectorization on ChaCha stream cipher. In Information Technology: New Generations (ITNG). 612--615.","DOI":"10.1109\/ITNG.2014.33"},{"key":"e_1_3_2_2_25_1","volume-title":"Ironclad apps: End-to-end security via automated full-system verification 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). 165--181","author":"Hawblitzel Chris","unstructured":"Chris Hawblitzel, Jon Howell, Jacob R Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill 2014. Ironclad apps: End-to-end security via automated full-system verification 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). 165--181."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Erick Nascimento \u0141ukasz Chmielewski David Oswald and Peter Schwabe 2016. Attacking embedded ECC implementations through cmov side channels Selected Areas in Cryptology -- SAC 2016 (Lecture Notes in Computer Science).","DOI":"10.1007\/978-3-319-69453-5_6"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"crossref","unstructured":"Pierre-Yves Strub Nikhil Swamy Cedric Fournet and Juan Chen. 2012. Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 571--584.","DOI":"10.1145\/2103621.2103723"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2016.125"},{"key":"e_1_3_2_2_32_1","unstructured":"National Institute of Standards US Department of Commerce and Technology (NIST). 2012. Federal Information Processing Standards Publication 180--4: Secure hash standard (SHS). (2012)."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.28"}],"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.3134043","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133956.3134043","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:03Z","timestamp":1750212663000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133956.3134043"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,30]]},"references-count":33,"alternative-id":["10.1145\/3133956.3134043","10.1145\/3133956"],"URL":"https:\/\/doi.org\/10.1145\/3133956.3134043","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"}}]}}