@inproceedings{60b309731ddb48a69ff08790000f62ee,
title = "Formal Verification of Saber{\textquoteright}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{\textquoteright}s security and δ -correctness properties, i.e., the properties required to transform the public-key encryption scheme into an secure and δ -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{\textquoteright}s public-key encryption scheme indeed satisfies the desired security and correctness properties.",
keywords = "EasyCrypt, Formal Verification, Saber",
author = "Andreas H{\"u}lsing and Matthias Meijers and Strub, \{Pierre Yves\}",
note = "Publisher Copyright: {\textcopyright} 2022, International Association for Cryptologic Research.; 42nd Annual International Cryptology Conference, CRYPTO 2022 ; Conference date: 15-08-2022 Through 18-08-2022",
year = "2022",
month = jan,
day = "1",
doi = "10.1007/978-3-031-15802-5\_22",
language = "English",
isbn = "9783031158018",
series = "Lecture Notes in Computer Science",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "622--653",
editor = "Yevgeniy Dodis and Thomas Shrimpton",
booktitle = "Advances in Cryptology – CRYPTO 2022 - 42nd Annual International Cryptology Conference, CRYPTO 2022, Proceedings",
}