Paper 2023/408
Machine-Checked Security for as in RFC 8391 and
Abstract
This work presents a novel machine-checked tight security
proof for
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. Revision June 11, 2024: - Fixed typos (particularly, if-guard in definition of PRF oracle). - Fixed formatting issues. - Change ORCIDs.
Metadata
- Available format(s)
-
PDF
- Category
- Public-key cryptography
- Publication info
- A major revision of an IACR publication in CRYPTO 2023
- DOI
- 10.1007/978-3-031-38554-4_14
- Keywords
- XMSSSPHINCS⁺EasyCryptFormal VerificationMachine-Checked ProofsComputer-Aided Cryptography
- Contact author(s)
- fv-xmss @ mmeijers com
- History
- 2024-06-11: last of 2 revisions
- 2023-03-21: 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 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}, doi = {10.1007/978-3-031-38554-4_14}, url = {https://eprint.iacr.org/2023/408} }