CryptoDB
A Tight Security Proof for SPHINCS+, Formally Verified
| Authors: |
|
|---|---|
| Download: | |
| Conference: | ASIACRYPT 2024 |
| Abstract: | SPHINCS+ is a post-quantum signature scheme that, at the time of writing, is being standardized as SLH-DSA. It is the most conser- vative option for post-quantum signatures, but the original tight proofs of security were flawed — as reported by Kudinov, Kiktenko and Fe- dorov 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 param- eter 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 com- plex 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 construc- tions, we (1) improve and extend the existing libraries for hash func- tions 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. |
BibTeX
@inproceedings{asiacrypt-2024-34601,
title={A Tight Security Proof for SPHINCS+, Formally Verified},
publisher={Springer-Verlag},
author={Matthias Meijers and Manuel Barbosa and François Dupressoir and Andreas Hülsing and Pierre-Yves Strub},
year=2024
}