{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T00:29:15Z","timestamp":1766449755192,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,11,6]],"date-time":"2019-11-06T00:00:00Z","timestamp":1572998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100007601","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["779391"],"award-info":[{"award-number":["779391"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000161","name":"National Institute of Standards and Technology","doi-asserted-by":"publisher","award":["60NANB15D248"],"award-info":[{"award-number":["60NANB15D248"]}],"id":[{"id":"10.13039\/100000161","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","award":["PTDC\/CCI-INF\/31698\/2017, SFRH\/BSAB\/143018\/2018"],"award-info":[{"award-number":["PTDC\/CCI-INF\/31698\/2017, SFRH\/BSAB\/143018\/2018"]}]},{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-12-1-0914, N00014-15-1-2750, N00014-19-1-2292"],"award-info":[{"award-number":["N00014-12-1-0914, N00014-15-1-2750, N00014-19-1-2292"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1801564"],"award-info":[{"award-number":["1801564"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008952","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-18-CE25-0014, ANR-17-CE39-0004-01"],"award-info":[{"award-number":["ANR-18-CE25-0014, ANR-17-CE39-0004-01"]}],"id":[{"id":"10.13039\/501100008952","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,11,6]]},"DOI":"10.1145\/3319535.3363211","type":"proceedings-article","created":{"date-parts":[[2019,11,7]],"date-time":"2019-11-07T13:08:32Z","timestamp":1573132112000},"page":"1607-1622","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Machine-Checked Proofs for Cryptographic Standards"],"prefix":"10.1145","author":[{"given":"Jos\u00e9 Bacelar","family":"Almeida","sequence":"first","affiliation":[{"name":"Universidade do Minho & INESC-TEC, Braga, Portugal"}]},{"given":"C\u00e9cile","family":"Baritel-Ruet","sequence":"additional","affiliation":[{"name":"Universit\u00e9 C\u00f4te d'Azur & Inria Sophia-Antipolis, Sophia-Antipolis, France"}]},{"given":"Manuel","family":"Barbosa","sequence":"additional","affiliation":[{"name":"Universidade do Porto & INESC-TEC, Porto, Portugal"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI-SP & IMDEA Software Institute, Bochum, Germany"}]},{"given":"Fran\u00e7ois","family":"Dupressoir","sequence":"additional","affiliation":[{"name":"University of Surrey & University of Bristol, Bristol, United Kingdom"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"Inria Sophia-Antipolis, Sophia-Antipolis, France"}]},{"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[{"name":"Inria, Rennes, France"}]},{"given":"Tiago","family":"Oliveira","sequence":"additional","affiliation":[{"name":"Universidade do Porto & INESC-TEC & FCUP, Porto, Portugal"}]},{"given":"Alley","family":"Stoughton","sequence":"additional","affiliation":[{"name":"Boston University, Boston, MA, USA"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2019,11,6]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Jasmin: High-Assurance and High-Speed Cryptography. In ACM CCS 2017: 24th Conference on Computer and Communications Security","author":"Almeida Jos\u00e9 Bacelar","year":"2017","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Arthur Blot , Benjamin Gr\u00e9goire , Vincent Laporte , Tiago Oliveira , Hugo Pacheco , Benedikt Schmidt , and Pierre-Yves Strub . 2017 . Jasmin: High-Assurance and High-Speed Cryptography. In ACM CCS 2017: 24th Conference on Computer and Communications Security , Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM Press , 1807--1823. https:\/\/doi.org\/10.1145\/3133956.3134078 10.1145\/3133956.3134078 Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Gr\u00e9goire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. 2017. Jasmin: High-Assurance and High-Speed Cryptography. In ACM CCS 2017: 24th Conference on Computer and Communications Security, Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM Press, 1807--1823. https:\/\/doi.org\/10.1145\/3133956.3134078"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516652"},{"volume-title":"Fast Software Encryption -- FSE 2016 (Lecture Notes in Computer Science)","author":"Almeida Jos\u00e9 Bacelar","key":"e_1_3_2_2_3_1","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , and Francois Dupressoir . 2016a. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC . In Fast Software Encryption -- FSE 2016 (Lecture Notes in Computer Science) , Thomas Peyrin (Ed.), Vol. 9783 . Springer , Heidelberg , 163--184. https:\/\/doi.org\/10.1007\/978--3--662--52993--5_9 10.1007\/978--3--662--52993--5_9 Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and Francois Dupressoir. 2016a. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. In Fast Software Encryption -- FSE 2016 (Lecture Notes in Computer Science), Thomas Peyrin (Ed.), Vol. 9783. Springer, Heidelberg, 163--184. https:\/\/doi.org\/10.1007\/978--3--662--52993--5_9"},{"volume-title":"USENIX Security 2016: 25th USENIX Security Symposium","author":"Almeida Jos\u00e9 Bacelar","key":"e_1_3_2_2_4_1","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Francois Dupressoir , and Michael Emmi . 2016b. Verifying Constant-Time Implementations . In USENIX Security 2016: 25th USENIX Security Symposium , Thorsten Holz and Stefan Savage (Eds.). USENIX Association , 53--70. Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, and Michael Emmi. 2016b. Verifying Constant-Time Implementations. In USENIX Security 2016: 25th USENIX Security Symposium, Thorsten Holz and Stefan Savage (Eds.). USENIX Association, 53--70."},{"key":"e_1_3_2_2_5_1","volume-title":"The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR","author":"Almeida Jos\u00e9 Bacelar","year":"2019","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Benjamin Gr\u00e9goire , Adrien Koutsos , Vincent Laporte , Tiago Oliveira , and Pierre-Yves Strub . 2019. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR , Vol. abs\/ 1904 .04606 ( 2019 ). arxiv: 1904.04606 http:\/\/arxiv.org\/abs\/1904.04606 Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Gr\u00e9goire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub. 2019. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR, Vol. abs\/1904.04606 (2019). arxiv: 1904.04606 http:\/\/arxiv.org\/abs\/1904.04606"},{"key":"e_1_3_2_2_6_1","volume-title":"NFM 2012, Norfolk, VA, USA, April 3--5, 2012. Proceedings. 2. https:\/\/doi.org\/10","author":"Appel Andrew W.","year":"2012","unstructured":"Andrew W. Appel . 2012 . Verified Software Toolchain. In NASA Formal Methods - 4th International Symposium , NFM 2012, Norfolk, VA, USA, April 3--5, 2012. Proceedings. 2. https:\/\/doi.org\/10 .1007\/978--3--642--28891--3_2 10.1007\/978--3--642--28891--3_2 Andrew W. Appel. 2012. Verified Software Toolchain. In NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3--5, 2012. Proceedings. 2. https:\/\/doi.org\/10.1007\/978--3--642--28891--3_2"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_2_8_1","volume-title":"Verified Security of Merkle-Damg\u00e5rd. In 25th IEEE Computer Security Foundations Symposium, CSF 2012","author":"Backes Michael","year":"2012","unstructured":"Michael Backes , Gilles Barthe , Matthias Berg , Benjamin Gr\u00e9goire , C\u00e9sar Kunz , Malte Skoruppa , and Santiago Zanella-B\u00e9guelin . 2012 . Verified Security of Merkle-Damg\u00e5rd. In 25th IEEE Computer Security Foundations Symposium, CSF 2012 , Cambridge, MA, USA, June 25--27 , 2012. 354--368. https:\/\/doi.org\/10.1109\/CSF.2012.14 10.1109\/CSF.2012.14 Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Gr\u00e9goire, C\u00e9sar Kunz, Malte Skoruppa, and Santiago Zanella-B\u00e9guelin. 2012. Verified Security of Merkle-Damg\u00e5rd. In 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25--27, 2012. 354--368. https:\/\/doi.org\/10.1109\/CSF.2012.14"},{"key":"e_1_3_2_2_9_1","volume-title":"Formal Security Proof of CMAC and Its Variants. In 31st IEEE Computer Security Foundations Symposium, CSF 2018","author":"Baritel-Ruet Cecile","year":"2018","unstructured":"Cecile Baritel-Ruet , Fran\u00e7ois Dupressoir , Pierre-Alain Fouque , and Benjamin Gr\u00e9goire . 2018 . Formal Security Proof of CMAC and Its Variants. In 31st IEEE Computer Security Foundations Symposium, CSF 2018 , Oxford, United Kingdom, July 9--12 , 2018. 91--104. https:\/\/doi.org\/10.1109\/CSF.2018.00014 10.1109\/CSF.2018.00014 Cecile Baritel-Ruet, Fran\u00e7ois Dupressoir, Pierre-Alain Fouque, and Benjamin Gr\u00e9goire. 2018. Formal Security Proof of CMAC and Its Variants. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9--12, 2018. 91--104. https:\/\/doi.org\/10.1109\/CSF.2018.00014"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866350"},{"key":"#cr-split#-e_1_3_2_2_11_1.1","unstructured":"Gilles Barthe Fran\u00e7ois Dupressoir Benjamin Gr\u00e9goire C\u00e9sar Kunz Benedikt Schmidt and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures. 146--166. https:\/\/doi.org\/10.1007\/978--3--319--10082--1_6 10.1007\/978--3--319--10082--1_6"},{"key":"#cr-split#-e_1_3_2_2_11_1.2","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Fran\u00e7ois Dupressoir Benjamin Gr\u00e9goire C\u00e9sar Kunz Benedikt Schmidt and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII - FOSAD 2012\/2013 Tutorial Lectures. 146--166. https:\/\/doi.org\/10.1007\/978--3--319--10082--1_6","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_3_2_2_12_1","volume-title":"Advances in Cryptology -- CRYPTO 2006 (Lecture Notes in Computer Science)","author":"Bellare Mihir","year":"1818","unstructured":"Mihir Bellare . 2006. New Proofs for NMAC and HMAC: Security without Collision-Resistance . In Advances in Cryptology -- CRYPTO 2006 (Lecture Notes in Computer Science) , Cynthia Dwork (Ed.), Vol. 4117 . Springer , Heidelberg , 602--619. https:\/\/doi.org\/10.1007\/1 1818 175_36 10.1007\/11818175_36 Mihir Bellare. 2006. New Proofs for NMAC and HMAC: Security without Collision-Resistance. In Advances in Cryptology -- CRYPTO 2006 (Lecture Notes in Computer Science), Cynthia Dwork (Ed.), Vol. 4117. Springer, Heidelberg, 602--619. https:\/\/doi.org\/10.1007\/11818175_36"},{"key":"e_1_3_2_2_13_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 . 207--221. https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/beringer 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. 207--221. https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/beringer"},{"volume-title":"Advances in Cryptology -- EUROCRYPT 2008 (Lecture Notes in Computer Science), Nigel P","author":"Bertoni Guido","key":"e_1_3_2_2_14_1","unstructured":"Guido Bertoni , Joan Daemen , Michael Peeters , and Gilles Van Assche . 2008. On the Indifferentiability of the Sponge Construction . In Advances in Cryptology -- EUROCRYPT 2008 (Lecture Notes in Computer Science), Nigel P . Smart (Ed.), Vol. 4965 . Springer , Heidelberg , 181--197. https:\/\/doi.org\/10.1007\/978--3--540--78967--3_11 balance 10.1007\/978--3--540--78967--3_11 Guido Bertoni, Joan Daemen, Michael Peeters, and Gilles Van Assche. 2008. On the Indifferentiability of the Sponge Construction. In Advances in Cryptology -- EUROCRYPT 2008 (Lecture Notes in Computer Science), Nigel P. Smart (Ed.), Vol. 4965. Springer, Heidelberg, 181--197. https:\/\/doi.org\/10.1007\/978--3--540--78967--3_11 balance"},{"key":"e_1_3_2_2_15_1","volume-title":"Verified cryptography for Firefox 57. https:\/\/blog.mozilla.org\/security\/2017\/09\/13\/verified-cryptography-firefox-57\/ Accessed","author":"Beurdouche Benjamin","year":"2019","unstructured":"Benjamin Beurdouche , Franziskus Kiefer , and Tim Taubert . 2017. Verified cryptography for Firefox 57. https:\/\/blog.mozilla.org\/security\/2017\/09\/13\/verified-cryptography-firefox-57\/ Accessed May 14, 2019 . Benjamin Beurdouche, Franziskus Kiefer, and Tim Taubert. 2017. Verified cryptography for Firefox 57. https:\/\/blog.mozilla.org\/security\/2017\/09\/13\/verified-cryptography-firefox-57\/ Accessed May 14, 2019."},{"key":"e_1_3_2_2_16_1","volume-title":"Advances in Cryptology -- CRYPTO","author":"Dodis Yevgeniy","year":"2018","unstructured":"Beno^it Cogliati, Yevgeniy Dodis , Jonathan Katz , Jooyoung Lee , John P. Steinberger , Aishwarya Thiruvengadam , and Zhe Zhang . 2018. Provable Security of (Tweakable) Block Ciphers Based on Substitution-Permutation Networks . In Advances in Cryptology -- CRYPTO 2018 , Part I (Lecture Notes in Computer Science), Hovav Shacham and Alexandra Boldyreva (Eds.), Vol. 10991 . Springer , Heidelberg, 722--753. https:\/\/doi.org\/10.1007\/978--3--319--96884--1_24 10.1007\/978--3--319--96884--1_24 Beno^it Cogliati, Yevgeniy Dodis, Jonathan Katz, Jooyoung Lee, John P. Steinberger, Aishwarya Thiruvengadam, and Zhe Zhang. 2018. Provable Security of (Tweakable) Block Ciphers Based on Substitution-Permutation Networks. In Advances in Cryptology -- CRYPTO 2018, Part I (Lecture Notes in Computer Science), Hovav Shacham and Alexandra Boldyreva (Eds.), Vol. 10991. Springer, Heidelberg, 722--753. https:\/\/doi.org\/10.1007\/978--3--319--96884--1_24"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_27"},{"volume-title":"Advances in Cryptology -- CRYPTO 2005 (Lecture Notes in Computer Science)","author":"Coron Jean-S\u00e9bastien","key":"e_1_3_2_2_18_1","unstructured":"Jean-S\u00e9bastien Coron , Yevgeniy Dodis , C\u00e9cile Malinaud , and Prashant Puniya . 2005. Merkle-Damg\u00e5rd Revisited: How to Construct a Hash Function . In Advances in Cryptology -- CRYPTO 2005 (Lecture Notes in Computer Science) , Victor Shoup (Ed.), Vol. 3621 . Springer , Heidelberg , 430--448. https:\/\/doi.org\/10.1007\/11535218_26 10.1007\/11535218_26 Jean-S\u00e9bastien Coron, Yevgeniy Dodis, C\u00e9cile Malinaud, and Prashant Puniya. 2005. Merkle-Damg\u00e5rd Revisited: How to Construct a Hash Function. In Advances in Cryptology -- CRYPTO 2005 (Lecture Notes in Computer Science), Victor Shoup (Ed.), Vol. 3621. Springer, Heidelberg, 430--448. https:\/\/doi.org\/10.1007\/11535218_26"},{"key":"e_1_3_2_2_19_1","volume-title":"SEFM 2012, Thessaloniki, Greece, October 1--5, 2012. Proceedings. 233--247","author":"Cuoq Pascal","year":"2012","unstructured":"Pascal Cuoq , Florent Kirchner , Nikolai Kosmatov , Virgile Prevosto , Julien Signoles , and Boris Yakobowski . 2012 . Frama-C - A Software Analysis Perspective. In Software Engineering and Formal Methods - 10th International Conference , SEFM 2012, Thessaloniki, Greece, October 1--5, 2012. Proceedings. 233--247 . https:\/\/doi.org\/10.1007\/978--3--642--33826--7_16 10.1007\/978--3--642--33826--7_16 Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2012. Frama-C - A Software Analysis Perspective. In Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1--5, 2012. Proceedings. 233--247. https:\/\/doi.org\/10.1007\/978--3--642--33826--7_16"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49896-5_23"},{"key":"e_1_3_2_2_21_1","volume-title":"Steinberger","author":"Dai Yuanxi","year":"2016","unstructured":"Yuanxi Dai and John P . Steinberger . 2016 . Indifferentiability of 8-Round Feistel Networks. In Advances in Cryptology -- CRYPTO 2016, Part I (Lecture Notes in Computer Science), Matthew Robshaw and Jonathan Katz (Eds.), Vol. 9814 . Springer , Heidelberg, 95--120. https:\/\/doi.org\/10.1007\/978--3--662--53018--4_4 10.1007\/978--3--662--53018--4_4 Yuanxi Dai and John P. Steinberger. 2016. Indifferentiability of 8-Round Feistel Networks. In Advances in Cryptology -- CRYPTO 2016, Part I (Lecture Notes in Computer Science), Matthew Robshaw and Jonathan Katz (Eds.), Vol. 9814. Springer, Heidelberg, 95--120. https:\/\/doi.org\/10.1007\/978--3--662--53018--4_4"},{"key":"e_1_3_2_2_22_1","volume-title":"Generic Indifferentiability Proofs of Hash Designs. In 25th IEEE Computer Security Foundations Symposium, CSF 2012","author":"Daubignard Marion","year":"2012","unstructured":"Marion Daubignard , Pierre-Alain Fouque , and Yassine Lakhnech . 2012 . Generic Indifferentiability Proofs of Hash Designs. In 25th IEEE Computer Security Foundations Symposium, CSF 2012 , Cambridge, MA, USA, June 25--27 , 2012, Stephen Chong (Ed.). IEEE Computer Society, 340--353. https:\/\/doi.org\/10.1109\/CSF.2012.13 10.1109\/CSF.2012.13 Marion Daubignard, Pierre-Alain Fouque, and Yassine Lakhnech. 2012. Generic Indifferentiability Proofs of Hash Designs. In 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25--27, 2012, Stephen Chong (Ed.). IEEE Computer Society, 340--353. https:\/\/doi.org\/10.1109\/CSF.2012.13"},{"key":"#cr-split#-e_1_3_2_2_23_1.1","doi-asserted-by":"crossref","unstructured":"Morris J. Dworkin. 2015. SHA-3 Standard: Permutation-Based Hash and Extendable-Output Functions. http:\/\/dx.doi.org\/10.6028\/NIST.FIPS.202 10.6028\/NIST.FIPS.202","DOI":"10.6028\/NIST.FIPS.202"},{"key":"#cr-split#-e_1_3_2_2_23_1.2","doi-asserted-by":"crossref","unstructured":"Morris J. Dworkin. 2015. SHA-3 Standard: Permutation-Based Hash and Extendable-Output Functions. http:\/\/dx.doi.org\/10.6028\/NIST.FIPS.202","DOI":"10.6028\/NIST.FIPS.202"},{"volume-title":"Without Compromises","author":"Erbsen Andres","key":"e_1_3_2_2_24_1","unstructured":"Andres Erbsen , Jade Philipoom , Jason Gross , Robert Sloan , and Adam Chlipala . 2019. Simple High-Level Code for Cryptographic Arithmetic - With Proofs , Without Compromises . In IEEE Security & Privacy. To appear. Retrieved from http:\/\/adam.chlipala.net\/papers\/FiatCryptoSP19\/FiatCryptoSP19.pdf. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. In IEEE Security & Privacy. To appear. Retrieved from http:\/\/adam.chlipala.net\/papers\/FiatCryptoSP19\/FiatCryptoSP19.pdf."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24638-1_2"},{"key":"e_1_3_2_2_27_1","volume-title":"POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11--18, 2015, Proceedings. 53--72","author":"Petcher Adam","year":"2015","unstructured":"Adam Petcher and Greg Morrisett . 2015 . The Foundational Cryptography Framework. In Principles of Security and Trust - 4th International Conference , POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11--18, 2015, Proceedings. 53--72 . https:\/\/doi.org\/10.1007\/978--3--662--46666--7_4 10.1007\/978--3--662--46666--7_4 Adam Petcher and Greg Morrisett. 2015. The Foundational Cryptography Framework. In Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11--18, 2015, Proceedings. 53--72. https:\/\/doi.org\/10.1007\/978--3--662--46666--7_4"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_2_30_1","volume-title":"Advances in Cryptology -- EUROCRYPT 2011 (Lecture Notes in Computer Science), Kenneth G","author":"Ristenpart Thomas","year":"2046","unstructured":"Thomas Ristenpart , Hovav Shacham , and Thomas Shrimpton . 2011. Careful with Composition: Limitations of the Indifferentiability Framework . In Advances in Cryptology -- EUROCRYPT 2011 (Lecture Notes in Computer Science), Kenneth G . Paterson (Ed.), Vol. 6632 . Springer , Heidelberg , 487--506. https:\/\/doi.org\/10.1007\/978--3--642-- 2046 5--4_27 10.1007\/978--3--642--20465--4_27 Thomas Ristenpart, Hovav Shacham, and Thomas Shrimpton. 2011. Careful with Composition: Limitations of the Indifferentiability Framework. In Advances in Cryptology -- EUROCRYPT 2011 (Lecture Notes in Computer Science), Kenneth G. Paterson (Ed.), Vol. 6632. Springer, Heidelberg, 487--506. https:\/\/doi.org\/10.1007\/978--3--642--20465--4_27"},{"volume-title":"Second-Preimage Resistance, and Collision Resistance. In Fast Software Encryption -- FSE 2004 (Lecture Notes in Computer Science), Bimal K","author":"Rogaway Phillip","key":"e_1_3_2_2_31_1","unstructured":"Phillip Rogaway and Thomas Shrimpton . 2004. Cryptographic Hash-Function Basics: Definitions, Implications, and Separations for Preimage Resistance , Second-Preimage Resistance, and Collision Resistance. In Fast Software Encryption -- FSE 2004 (Lecture Notes in Computer Science), Bimal K . Roy and Willi Meier (Eds.), Vol. 3017 . Springer , Heidelberg , 371--388. https:\/\/doi.org\/10.1007\/978--3--540--25937--4_24 10.1007\/978--3--540--25937--4_24 Phillip Rogaway and Thomas Shrimpton. 2004. Cryptographic Hash-Function Basics: Definitions, Implications, and Separations for Preimage Resistance, Second-Preimage Resistance, and Collision Resistance. In Fast Software Encryption -- FSE 2004 (Lecture Notes in Computer Science), Bimal K. Roy and Willi Meier (Eds.), Vol. 3017. Springer, Heidelberg, 371--388. https:\/\/doi.org\/10.1007\/978--3--540--25937--4_24"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2016.125"},{"key":"e_1_3_2_2_35_1","volume-title":"Appel","author":"Ye Katherine Q.","year":"2017","unstructured":"Katherine Q. Ye , Matthew Green , Naphat Sanguansin , Lennart Beringer , Adam Petcher , and Andrew W . Appel . 2017 . Verified Correctness and Security of mbedTLS HMAC-DRBG. In ACM CCS 2017: 24th Conference on Computer and Communications Security, Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM Press , 2007--2020. https:\/\/doi.org\/10.1145\/3133956.3133974 10.1145\/3133956.3133974 Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel. 2017. Verified Correctness and Security of mbedTLS HMAC-DRBG. In ACM CCS 2017: 24th Conference on Computer and Communications Security, Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM Press, 2007--2020. https:\/\/doi.org\/10.1145\/3133956.3133974"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"CCS '19: 2019 ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"London United Kingdom","acronym":"CCS '19"},"container-title":["Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3319535.3363211","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3319535.3363211","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3319535.3363211","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:32Z","timestamp":1750203872000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3319535.3363211"}},"subtitle":["Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3"],"short-title":[],"issued":{"date-parts":[[2019,11,6]]},"references-count":36,"alternative-id":["10.1145\/3319535.3363211","10.1145\/3319535"],"URL":"https:\/\/doi.org\/10.1145\/3319535.3363211","relation":{},"subject":[],"published":{"date-parts":[[2019,11,6]]},"assertion":[{"value":"2019-11-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}