Paper 2023/408

Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$

Manuel Barbosa, University of Porto, INESC TEC
François Dupressoir, University of Bristol
Benjamin Grégoire, Université Côte d’Azur, Inria
Andreas Hülsing, Eindhoven University of Technology
Matthias Meijers, Eindhoven University of Technology
Pierre-Yves Strub, Meta

This work presents a novel machine-checked tight security proof for $\mathrm{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 $\mathrm{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 $\mathrm{SPHINCS}^{+}$ and $\mathrm{XMSS}$. For the case of $\mathrm{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 $\mathrm{XMSS}$ and formally verify it using the EasyCrypt proof assistant. As part of this endeavor, we formally verify the crucial step common to (the security proofs of) $\mathrm{SPHINCS}^{+}$ and $\mathrm{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 $\mathrm{LMS}$ or $\mathrm{SPHINCS}^{+}$.

Note: Revision August 3, 2023: - Changed the property considered for the message compression function from collision resistance to multi-target extended target collision resistance. - Added a term in the bound of the final security theorem that covers the bad event in which the forgery returned by the EUF-CMA adversary considers a message that is in the list of messages provided to the (EUF-RMA) reduction adversary. - Fixed typos.

Available format(s)
Public-key cryptography
Publication info
XMSSSPHINCS+EasyCryptFormal VerificationMachine-Checked ProofsComputer-Aided Cryptography
Contact author(s)
fv-xmss @ mmeijers com
2023-08-03: revised
2023-03-21: received
See all versions
Short URL
Creative Commons Attribution


      author = {Manuel Barbosa and François Dupressoir and Benjamin Grégoire and Andreas Hülsing and Matthias Meijers and Pierre-Yves Strub},
      title = {Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$},
      howpublished = {Cryptology ePrint Archive, Paper 2023/408},
      year = {2023},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.