Machine-checked security for XMSS as in RFC 8391 and SPHINCS\textsuperscript{+}

DOI10.1007/978-3-031-38554-4_14MaRDI QIDQ6190145zbMATH OpenOpenAlexFDO

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

Publication date 6 February 2024

Published in Advances in Cryptology – CRYPTO 2023 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-38554-4_14

zbMATH Keywords

computer-aided cryptographyEasyCryptformal verificationmachine-checked proofsSPHINCS\textsuperscript{+}XMSS

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Cryptography (94A60)

Cites work

• Beyond provable security verifiable IND-CCA security of OAEP
• Breaking category five \(\mathrm{SPHINCS}^+\) with SHA-256
• Computer-aided cryptographic proofs
• Critical perspectives on provable security: fifteen years of ``another look papers
• Formal verification of Saber's public-key encryption scheme in easycrypt
• How to record quantum queries, and applications to quantum indifferentiability
• Mitigating multi-target attacks in hash-based signatures
• Recovering the tight security proof of SPHINCS\textsuperscript{+}
• Tight adaptive reprogramming in the QROM

Cited in

(2)

• Formally verifying Kyber. Episode V: machine-checked IND-CCA security and correctness of ML-KEM in Easycrypt
• A tight security proof for SPHINCS\textsuperscript{+}, formally verified

This page was built for publication: Machine-checked security for XMSS as in RFC 8391 and SPHINCS\textsuperscript{+}

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6190145)