Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+

Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review


This work presents a novel machine-checked tight security proof for XMSS —a stateful hash-based signature scheme that is (1) standardized in RFC 8391 and NIST SP 800-208, and (2) employed as a primary building block of SPHINCS +, one of the signature schemes recently selected for standardization as a result of NIST’s post-quantum competition. In 2020, Kudinov, Kiktenko, and Fedoro pointed out a flaw affecting the tight security proofs of SPHINCS + and XMSS. For the case of SPHINCS +, this flaw was fixed in a subsequent tight security proof by Hülsing and Kudinov. Unfortunately, employing the fix from this proof to construct an analogous tight security proof for XMSS would merely demonstrate security with respect to an insufficient notion. At the cost of modeling the message-hashing function as a random oracle, we complete the tight security proof for XMSS and formally verify it using the EasyCrypt proof assistant. (Note that this merely extends the use of the random oracle model, as this model is already required in other parts of the security analysis to justify the currently standardized parameter values). As part of this endeavor, we formally verify the crucial step common to the security proofs of SPHINCS + and XMSS that was found to be flawed before, thereby confirming that the core of the aforementioned security proof by Hülsing and Kudinov is correct. As this is the first work to formally verify proofs for hash-based signature schemes in EasyCrypt, we develop several novel libraries for the fundamental cryptographic concepts underlying such schemes—e.g., hash functions and digital signature schemes—establishing a common starting point for future formal verification efforts. These libraries will be particularly helpful in formally verifying proofs of other hash-based signature schemes such as LMS or SPHINCS +.

Originele taal-2Engels
TitelAdvances in Cryptology – CRYPTO 2023
Subtitel43rd Annual International Cryptology Conference, CRYPTO 2023, Santa Barbara, CA, USA, August 20–24, 2023, Proceedings, Part V
RedacteurenHelena Handschuh, Anna Lysyanskaya
Plaats van productieCham
Aantal pagina's34
ISBN van elektronische versie978-3-031-38554-4
ISBN van geprinte versie978-3-031-38553-7
StatusGepubliceerd - 2023
Evenement43rd Annual International Cryptology Conference, CRYPTO 2023 - Santa Barbara, Verenigde Staten van Amerika
Duur: 20 aug. 202324 aug. 2023
Congresnummer: 43

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743
ISSN van elektronische versie1611-3349


Congres43rd Annual International Cryptology Conference, CRYPTO 2023
Verkorte titelCRYPTO 2023
Land/RegioVerenigde Staten van Amerika
StadSanta Barbara


Duik in de onderzoeksthema's van 'Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+'. Samen vormen ze een unieke vingerafdruk.

Citeer dit