CryptoDB
Pierre-Yves Strub
ORCID: 0000-0002-8196-7875
Publications
Year
Venue
Title
2023
CRYPTO
Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+
Abstract
This work presents a novel machine-checked tight security proof for XMSS --- a stateful hash-based signature scheme that is (1) standardized in RFC 8391 and NIST SP 800-208, and (2) employed as a primary building block of SPHINCS+, one of the signature schemes recently selected for standardization as a result of NIST's post-quantum competition.
In 2020, Kudinov, Kiktenko, and Fedoro pointed out a flaw affecting the tight security proofs of SPHINCS+ and XMSS. For the case of SPHINCS+, this flaw was fixed in a subsequent tight security proof by Hülsing and Kudinov. Unfortunately, employing the fix from this proof to construct an analogous tight security proof for XMSS would merely demonstrate security with respect to an insufficient notion.
At the cost of modeling the message-hashing function as a random oracle, we complete the tight security proof for XMSS and formally verify it using the EasyCrypt proof assistant. (Note that this merely extends the use of the random oracle model, as this model is already required in other parts of the security analysis to justify the currently standardized parameter values). As part of this endeavor, we formally verify the crucial step common to the security proofs of SPHINCS+ and XMSS that was found to be flawed before, thereby confirming that the core of the aforementioned security proof by Hülsing and Kudinov is correct.
As this is the first work to formally verify proofs for hash-based signature schemes in EasyCrypt, we develop several novel libraries for the fundamental cryptographic concepts underlying such schemes --- e.g., hash functions and digital signature schemes --- establishing a common starting point for future formal verification efforts. These libraries will be particularly helpful in formally verifying proofs of other hash-based signature schemes such as LMS or SPHINCS+.
2023
TCHES
Formally verifying Kyber: Episode IV: Implementation correctness
Abstract
In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present high-assurance open-source implementations of Kyber written in the Jasmin language, along with machine-checked proofs that they are functionally correct with respect to the EasyCrypt specification. We describe a number of improvements to the EasyCrypt and Jasmin frameworks that were needed for this implementation and verification effort, and we present detailed benchmarks of our implementations, showing that our code achieves performance close to existing hand-optimized implementations in C and assembly.
2022
CRYPTO
Formal Verification of Saber’s Public-Key Encryption Scheme in EasyCrypt
📺
Abstract
In this work, we consider the formal verification of the public-key encryption scheme of Saber, one of the selected few post-quantum cipher suites currently considered for potential standardization. We formally verify this public-key encryption scheme's IND-CPA security and delta-correctness properties, i.e., the properties required to transform the public-key encryption scheme into an IND-CCA2 secure and delta-correct key encapsulation mechanism, in EasyCrypt. To this end, we initially devise hand-written proofs for these properties that are significantly more detailed and meticulous than the presently existing proofs. Subsequently, these hand-written proofs serve as a guideline for the formal verification. The results of this endeavor comprise hand-written and computer-verified proofs which demonstrate that Saber's public-key encryption scheme indeed satisfies the desired security and correctness properties.
Coauthors
- José Bacelar Almeida (1)
- Manuel Barbosa (2)
- Gilles Barthe (3)
- Santiago Zanella Béguelin (1)
- Sonia Belaïd (1)
- Karthikeyan Bhargavan (1)
- François Dupressoir (3)
- Sebastian Faust (1)
- Pierre-Alain Fouque (1)
- Cédric Fournet (1)
- Benjamin Grégoire (4)
- Andreas Hülsing (2)
- Markulf Kohlweiss (1)
- Vincent Laporte (1)
- Jean-Christophe Léchenet (1)
- Matthias Meijers (1)
- Joost Meijers (1)
- Tiago Oliveira (1)
- Hugo Pacheco (1)
- Alfredo Pironti (1)
- Miguel Quaresma (1)
- Peter Schwabe (1)
- Antoine Séré (1)
- François-Xavier Standaert (1)