Paper 2023/408
MachineChecked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$
Abstract
This work presents a novel machinechecked tight security proof for $\mathrm{XMSS}$ — a stateful hashbased signature scheme that is (1) standardized in RFC 8391 and NIST SP 800208, 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 postquantum 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 messagehashing 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 hashbased 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 hashbased signature schemes such as $\mathrm{LMS}$ or $\mathrm{SPHINCS}^{+}$.
Metadata
 Available format(s)
 Category
 Publickey cryptography
 Publication info
 Preprint.
 Keywords
 XMSSSPHINCS+EasyCryptFormal VerificationMachineChecked ProofsComputerAided Cryptography
 Contact author(s)

mbb @ fc up pt
f dupressoir @ bristol ac uk
benjamin gregoire @ inria fr
andreas @ huelsing net
research @ mmeijers com
strubpy @ meta com  History
 20230324: approved
 20230321: received
 See all versions
 Short URL
 https://ia.cr/2023/408
 License

CC BY
BibTeX
@misc{cryptoeprint:2023/408, author = {Manuel Barbosa and François Dupressoir and Benjamin Grégoire and Andreas Hülsing and Matthias Meijers and PierreYves Strub}, title = {MachineChecked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$}, howpublished = {Cryptology ePrint Archive, Paper 2023/408}, year = {2023}, note = {\url{https://eprint.iacr.org/2023/408}}, url = {https://eprint.iacr.org/2023/408} }