A tight security proof for SPHINCS\textsuperscript{+}, formally verified

DOI10.1007/978-981-96-0894-2_2MaRDI QIDQ6965249zbMATH OpenFDO

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

Publication date 3 July 2025

Full work available at URL https://research.tue.nl/en/publications/65dc0cfb-f636-4a0e-b38c-4dc970604054

zbMATH Keywords

computer-aided cryptographyEasyCryptformal verificationmachine-checked proofspost-quantum cryptographySPHINCS\textsuperscript{+}

Mathematics Subject Classification ID

Quantum cryptography (quantum-theoretic aspects) (81P94) Cryptography (94A60)

Cites work

• A formal security analysis of the Signal messaging protocol
• Analysing the HPKE standard
• Computer-Aided Security Proofs for the Working Cryptographer
• Decisional second-preimage resistance: when does SPR imply PRE?
• Formal verification of Saber's public-key encryption scheme in easycrypt
• Machine-checked security for XMSS as in RFC 8391 and SPHINCS\textsuperscript{+}
• Mitigating multi-target attacks in hash-based signatures
• Recovering the tight security proof of SPHINCS\textsuperscript{+}

This page was built for publication: A tight security proof for SPHINCS\textsuperscript{+}, formally verified

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