{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:57:53Z","timestamp":1743073073295,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":25,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819608935"},{"type":"electronic","value":"9789819608942"}],"license":[{"start":{"date-parts":[[2024,12,13]],"date-time":"2024-12-13T00:00:00Z","timestamp":1734048000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,12,13]],"date-time":"2024-12-13T00:00:00Z","timestamp":1734048000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-981-96-0894-2_2","type":"book-chapter","created":{"date-parts":[[2024,12,13]],"date-time":"2024-12-13T00:48:03Z","timestamp":1734050883000},"page":"35-67","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Tight Security Proof for SPHINCS$$^{+}$$, Formally Verified"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6848-5564","authenticated-orcid":false,"given":"Manuel","family":"Barbosa","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3497-3110","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Dupressoir","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2215-4134","authenticated-orcid":false,"given":"Andreas","family":"H\u00fclsing","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5351-991X","authenticated-orcid":false,"given":"Matthias","family":"Meijers","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8196-7875","authenticated-orcid":false,"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,12,13]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"J.\u00a0B. Almeida, M.\u00a0Barbosa, G.\u00a0Barthe, B.\u00a0Gr\u00e9goire, A.\u00a0Koutsos, V.\u00a0Laporte, T.\u00a0Oliveira, and P.-Y. Strub. The last mile: High-assurance and high-speed cryptographic implementations. In 2020 IEEE Symposium on Security and Privacy, pages 965\u2013982, San Francisco, CA, USA, May\u00a018\u201321, 2020. IEEE Computer Society Press.","key":"2_CR1","DOI":"10.1109\/SP40000.2020.00028"},{"issue":"3","key":"2_CR2","doi-asserted-by":"publisher","first-page":"164","DOI":"10.46586\/tches.v2023.i3.164-193","volume":"2023","author":"JB Almeida","year":"2023","unstructured":"J.\u00a0B. Almeida, M.\u00a0Barbosa, G.\u00a0Barthe, B.\u00a0Gr\u00e9goire, V.\u00a0Laporte, J.-C. L\u00e9chenet, T.\u00a0Oliveira, H.\u00a0Pacheco, M.\u00a0Quaresma, P.\u00a0Schwabe, A.\u00a0S\u00e9r\u00e9, and P.-Y. Strub. Formally verifying kyber episode IV: Implementation correctness. IACR Transactions on Cryptographic Hardware and Embedded Systems, 2023(3):164\u2013193, 2023.","journal-title":"IACR Transactions on Cryptographic Hardware and Embedded Systems"},{"doi-asserted-by":"crossref","unstructured":"J.\u00a0B. Almeida, C.\u00a0Baritel-Ruet, M.\u00a0Barbosa, G.\u00a0Barthe, F.\u00a0Dupressoir, B.\u00a0Gr\u00e9goire, V.\u00a0Laporte, T.\u00a0Oliveira, A.\u00a0Stoughton, and P.-Y. Strub. Machine-checked proofs for cryptographic standards: Indifferentiability of sponge and secure high-assurance implementations of SHA-3. In L.\u00a0Cavallaro, J.\u00a0Kinder, X.\u00a0Wang, and J.\u00a0Katz, editors, ACM CCS 2019: 26th Conference on Computer and Communications Security, pages 1607\u20131622, London, UK, Nov.\u00a011\u201315, 2019. ACM Press.","key":"2_CR3","DOI":"10.1145\/3319535.3363211"},{"doi-asserted-by":"crossref","unstructured":"J.\u00a0Alwen, B.\u00a0Blanchet, E.\u00a0Hauck, E.\u00a0Kiltz, B.\u00a0Lipp, and D.\u00a0Riepel. Analysing the HPKE standard. In A.\u00a0Canteaut and F.-X. Standaert, editors, Advances in Cryptology \u2013 EUROCRYPT\u00a02021, Part\u00a0I, volume 12696 of Lecture Notes in Computer Science, pages 87\u2013116, Zagreb, Croatia, Oct.\u00a017\u201321, 2021. Springer, Heidelberg, Germany.","key":"2_CR4","DOI":"10.1007\/978-3-030-77870-5_4"},{"doi-asserted-by":"crossref","unstructured":"M.\u00a0Barbosa, G.\u00a0Barthe, K.\u00a0Bhargavan, B.\u00a0Blanchet, C.\u00a0Cremers, K.\u00a0Liao, and B.\u00a0Parno. SoK: Computer-aided cryptography. In 2021 IEEE Symposium on Security and Privacy, pages 777\u2013795, San Francisco, CA, USA, May\u00a024\u201327, 2021. IEEE Computer Society Press.","key":"2_CR5","DOI":"10.1109\/SP40001.2021.00008"},{"doi-asserted-by":"crossref","unstructured":"M.\u00a0Barbosa, F.\u00a0Dupressoir, B.\u00a0Gr\u00e9goire, A.\u00a0H\u00fclsing, M.\u00a0Meijers, and P.-Y. Strub. Machine-checked security for XMSS as in RFC 8391 and SPHINCS$$^{+}$$. In H.\u00a0Handschuh and A.\u00a0Lysyanskaya, editors, Advances in Cryptology \u2013 CRYPTO 2023, volume 14085, pages 421\u2013454, Cham, Aug. 2023. Springer Nature Switzerland.","key":"2_CR6","DOI":"10.1007\/978-3-031-38554-4_14"},{"doi-asserted-by":"crossref","unstructured":"G.\u00a0Barthe, B.\u00a0Gr\u00e9goire, S.\u00a0Heraud, and S.\u00a0Zanella B\u00e9guelin. Computer-aided security proofs for the working cryptographer. In P.\u00a0Rogaway, editor, Advances in Cryptology \u2013 CRYPTO\u00a02011, volume 6841 of Lecture Notes in Computer Science, pages 71\u201390, Santa Barbara, CA, USA, Aug.\u00a014\u201318, 2011. Springer, Heidelberg, Germany.","key":"2_CR7","DOI":"10.1007\/978-3-642-22792-9_5"},{"doi-asserted-by":"crossref","unstructured":"D.\u00a0J. Bernstein and A.\u00a0H\u00fclsing. Decisional second-preimage resistance: When does SPR imply PRE? In S.\u00a0D. Galbraith and S.\u00a0Moriai, editors, Advances in Cryptology \u2013 ASIACRYPT\u00a02019, Part\u00a0III, volume 11923 of Lecture Notes in Computer Science, pages 33\u201362, Kobe, Japan, Dec.\u00a08\u201312, 2019. Springer, Heidelberg, Germany.","key":"2_CR8","DOI":"10.1007\/978-3-030-34618-8_2"},{"doi-asserted-by":"crossref","unstructured":"D.\u00a0J. Bernstein, A.\u00a0H\u00fclsing, S.\u00a0K\u00f6lbl, R.\u00a0Niederhagen, J.\u00a0Rijneveld, and P.\u00a0Schwabe. The SPHINCS$$^+$$ signature framework. In L.\u00a0Cavallaro, J.\u00a0Kinder, X.\u00a0Wang, and J.\u00a0Katz, editors, ACM CCS 2019: 26th Conference on Computer and Communications Security, pages 2129\u20132146, London, UK, Nov.\u00a011\u201315, 2019. ACM Press.","key":"2_CR9","DOI":"10.1145\/3319535.3363229"},{"doi-asserted-by":"crossref","unstructured":"D.\u00a0J. Bernstein and T.\u00a0Lange. Post-quantum cryptography. Nature, 549(7671):188\u2013194, Sep. 2017.","key":"2_CR10","DOI":"10.1038\/nature23461"},{"doi-asserted-by":"crossref","unstructured":"K.\u00a0Cohn-Gordon, C.\u00a0Cremers, B.\u00a0Dowling, L.\u00a0Garratt, and D.\u00a0Stebila. A formal security analysis of the Signal messaging protocol. Journal of Cryptology, 33(4):1914\u20131983, Oct. 2020.","key":"2_CR11","DOI":"10.1007\/s00145-020-09360-1"},{"doi-asserted-by":"crossref","unstructured":"D.\u00a0Cooper, D.\u00a0Apon, Q.\u00a0Dang, M.\u00a0Davidson, M.\u00a0Dworkin, and C.\u00a0Miller. Recommendation for stateful hash-based signature schemes, 2020-10-29 00:10:00 2020.","key":"2_CR12","DOI":"10.6028\/NIST.SP.800-208"},{"doi-asserted-by":"crossref","unstructured":"C.\u00a0Cremers, M.\u00a0Horvat, J.\u00a0Hoyland, S.\u00a0Scott, and T.\u00a0van der Merwe. A comprehensive symbolic analysis of TLS 1.3. In B.\u00a0M. Thuraisingham, D.\u00a0Evans, T.\u00a0Malkin, and D.\u00a0Xu, editors, ACM CCS 2017: 24th Conference on Computer and Communications Security, pages 1773\u20131788, Dallas, TX, USA, Oct.\u00a031\u00a0\u2013\u00a0Nov.\u00a02, 2017. ACM Press.","key":"2_CR13","DOI":"10.1145\/3133956.3134063"},{"unstructured":"A.\u00a0Fedorov, E.\u00a0Kiktenko, and M.\u00a0Kudinov. [pqc-forum] round 3 official comment: SPHINCS$$^+$$. https:\/\/csrc.nist.gov\/CSRC\/media\/Projects\/post-quantum-cryptography\/documents\/round-3\/official-comments\/Sphincs-Plus-round3-official-comment.pdf, 2020. Accessed: 22-05-2024.","key":"2_CR14"},{"doi-asserted-by":"crossref","unstructured":"E.\u00a0Grumbling and M.\u00a0Horowitz. Quantum Computing: Progress and Prospects. National Academies of Sciences, Engineering, and Medicine. The National Academies Press, 1st edition, Apr. 2019.","key":"2_CR15","DOI":"10.17226\/25196"},{"doi-asserted-by":"crossref","unstructured":"A.\u00a0Huelsing, D.\u00a0Butin, S.-L. Gazdag, J.\u00a0Rijneveld, and A.\u00a0Mohaisen. XMSS: eXtended Merkle Signature Scheme. RFC 8391, May 2018.","key":"2_CR16","DOI":"10.17487\/RFC8391"},{"doi-asserted-by":"crossref","unstructured":"A.\u00a0H\u00fclsing and M.\u00a0A. Kudinov. Recovering the tight security proof of SPHINCS$$^+$$. In S.\u00a0Agrawal and D.\u00a0Lin, editors, Advances in Cryptology \u2013 ASIACRYPT\u00a02022, Part\u00a0IV, volume 13794 of Lecture Notes in Computer Science, pages 3\u201333, Taipei, Taiwan, Dec.\u00a05\u20139, 2022. Springer, Heidelberg, Germany.","key":"2_CR17","DOI":"10.1007\/978-3-031-22972-5_1"},{"doi-asserted-by":"crossref","unstructured":"A.\u00a0H\u00fclsing, M.\u00a0Meijers, and P.-Y. Strub. Formal verification of Saber\u2019s public-key encryption scheme in EasyCrypt. In Y.\u00a0Dodis and T.\u00a0Shrimpton, editors, Advances in Cryptology \u2013 CRYPTO\u00a02022, Part\u00a0I, volume 13507 of Lecture Notes in Computer Science, pages 622\u2013653, Santa Barbara, CA, USA, Aug.\u00a015\u201318, 2022. Springer, Heidelberg, Germany.","key":"2_CR18","DOI":"10.1007\/978-3-031-15802-5_22"},{"doi-asserted-by":"crossref","unstructured":"A.\u00a0H\u00fclsing, L.\u00a0Rausch, and J.\u00a0Buchmann. Optimal parameters for $${\\rm XMSS}^{\\rm MT}$$. In A.\u00a0Cuzzocrea, C.\u00a0Kittl, D.\u00a0E. Simos, E.\u00a0Weippl, and L.\u00a0Xu, editors, Security Engineering and Intelligence Informatics, pages 194\u2013208, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg.","key":"2_CR19","DOI":"10.1007\/978-3-642-40588-4_14"},{"doi-asserted-by":"crossref","unstructured":"A.\u00a0H\u00fclsing, J.\u00a0Rijneveld, and F.\u00a0Song. Mitigating multi-target attacks in hash-based signatures. In C.-M. Cheng, K.-M. Chung, G.\u00a0Persiano, and B.-Y. Yang, editors, PKC\u00a02016: 19th International Conference on Theory and Practice of Public Key Cryptography, Part\u00a0I, volume 9614 of Lecture Notes in Computer Science, pages 387\u2013416, Taipei, Taiwan, Mar.\u00a06\u20139, 2016. Springer, Heidelberg, Germany.","key":"2_CR20","DOI":"10.1007\/978-3-662-49384-7_15"},{"unstructured":"M.\u00a0A. Kudinov, E.\u00a0O. Kiktenko, and A.\u00a0K. Fedorov. Security analysis of the w-ots$$ ^{\\text{+}}$$ signature scheme: Updating security bounds. CoRR, abs\/2002.07419, 2020.","key":"2_CR21"},{"doi-asserted-by":"crossref","unstructured":"D.\u00a0McGrew, P.\u00a0Kampanakis, S.\u00a0Fluhrer, S.-L. Gazdag, D.\u00a0Butin, and J.\u00a0Buchmann. State management for hash-based signatures. Cryptology ePrint Archive, Report 2016\/357, 2016. https:\/\/eprint.iacr.org\/2016\/357.","key":"2_CR22","DOI":"10.1007\/978-3-319-49100-4_11"},{"unstructured":"M.\u00a0Mosca and M.\u00a0Piani. Quantum threat timeline report 2023. Technical report, Global Risk Insitute, dec 2023.","key":"2_CR23"},{"unstructured":"NIST. National Institute for Standards and Technology. announcing request for nominations for public-key post-quantum cryptographic algorithms., Dec. 2016. https:\/\/csrc.nist.gov\/News\/2016\/Public-Key-Post-Quantum-Cryptographic-Algorithms.","key":"2_CR24"},{"unstructured":"NIST. National Institute for Standards and Technology. PQC standardization process: Announcing four candidates to be standardized, plus fourth round candidates., Mar. 2022. https:\/\/csrc.nist.gov\/News\/2022\/pqc-candidates-to-be-standardized-and-round-4.","key":"2_CR25"}],"container-title":["Lecture Notes in Computer Science","Advances in Cryptology \u2013 ASIACRYPT 2024"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-0894-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,13]],"date-time":"2024-12-13T01:02:35Z","timestamp":1734051755000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-0894-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,13]]},"ISBN":["9789819608935","9789819608942"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-0894-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,12,13]]},"assertion":[{"value":"13 December 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"All authors are members of the Formosa Crypto consortium. Fran\u00e7ois Dupressoir is a member of the technical evaluation committee for PEPR en Cybers\u00e9curit\u00e9.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"ASIACRYPT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on the Theory and Application of Cryptology and Information Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kolkata","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"asiacrypt2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/asiacrypt.iacr.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}