## CryptoDB

### Paper: Formal Verification of Saber’s Public-Key Encryption Scheme in EasyCrypt

Authors: Matthias Meijers , Eindhoven University of Technology Andreas Hülsing , Eindhoven University of Technology Pierre-Yves Strub , Meta, France Search ePrint Search Google Slides CRYPTO 2022 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.
##### BibTeX
@inproceedings{crypto-2022-32194,
title={Formal Verification of Saber’s Public-Key Encryption Scheme in EasyCrypt},
publisher={Springer-Verlag},
author={Matthias Meijers and Andreas Hülsing and Pierre-Yves Strub},
year=2022
}