Welcome to the resource topic for 2024/910
Title:
A Tight Security Proof for \mathrm{SPHINCS^{+}}, Formally Verified
Authors: Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
Abstract:\mathrm{SPHINCS^{+}} is a post-quantum signature scheme that, at the time of writing, is being standardized as \mathrm{SLH\text{-}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 \mathrm{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.
ePrint: https://eprint.iacr.org/2024/910
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .