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}^{+}$.
Note: Revision August 3, 2023:  Changed the property considered for the message compression function from collision resistance to multitarget 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 EUFCMA adversary considers a message that is in the list of messages provided to the (EUFRMA) reduction adversary.  Fixed typos.
Metadata
 Available format(s)
 Category
 Publickey cryptography
 Publication info
 Preprint.
 Keywords
 XMSSSPHINCS+EasyCryptFormal VerificationMachineChecked ProofsComputerAided Cryptography
 Contact author(s)
 fvxmss @ mmeijers com
 History
 20230803: revised
 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} }