BLUE
Login
EU
ePrint Updates
@eprint.bsky.social
Unofficial bot tracking updates to the IACR Cryptology ePrint Archive (eprint.iacr.org/). Maintained by @str4d.xyz. Currently only posts about new papers. Author names are linkified to Bluesky accounts; contact maintainer for inclusion or removal.
407 followers1 following3k posts
EUeprint.bsky.social

A Tight Security Proof for SPHINCS⁺, Formally Verified (Manuel Barbosa, François Dupressoiria.cr/2024/910

Abstract. SPHINCS⁺ is a post-quantum signature scheme that, at the time of writing, is being standardized as SLH-DSA. It is the most conservative option for post-quantum signatures, but the original tight proofs of security were flawed—as reported by Kudinov, Kiktenko and Fedorov in 2020. In this work, we formally prove a tight security bound for SPHINCS⁺ using the EasyCrypt proof assistant, establishing greater confidence in the general security of the scheme and that of the parameter sets considered for standardization. To this end, we reconstruct the tight security proof presented by Hülsing and Kudinov (in 2022) in a modular way. A small but important part of this effort involves a complex argument relating four different games at once, of a form not yet formalized in EasyCrypt (to the best of our knowledge). We describe our approach to overcoming this major challenge, and develop a general formal verification technique aimed at this type of reasoning. Enhancing the set of reusable EasyCrypt artifacts previously produced in the formal verification of stateful hash-based cryptographic constructions, we (1) improve and extend the existing libraries for hash functions and (2) develop new libraries for fundamental concepts related to hash-based cryptographic constructions, including Merkle trees. These enhancements, along with the formal verification technique we develop, further ease future formal verification endeavors in EasyCrypt, especially those concerning hash-based cryptographic constructions.
Image showing part 2 of abstract.
0
EU
ePrint Updates
@eprint.bsky.social
Unofficial bot tracking updates to the IACR Cryptology ePrint Archive (eprint.iacr.org/). Maintained by @str4d.xyz. Currently only posts about new papers. Author names are linkified to Bluesky accounts; contact maintainer for inclusion or removal.
407 followers1 following3k posts
HomePopularExplore