@inproceedings{cab30e95322e4734bbc75e15bb7b6a7b,
title = "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{\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 Pierre-Yves Strub",
year = "2022",
month = oct,
day = "12",
doi = "10.1007/978-3-031-15802-5\_22",
language = "English",
isbn = "978-3-031-15801-8",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer",
pages = "622--653",
editor = "Yevgeniy Dodis and Thomas Shrimpton",
booktitle = "Advances in Cryptology – CRYPTO 2022",
address = "Germany",
note = "42nd Annual International Cryptology Conference, CRYPTO 2022, CRYPTO 2022 ; Conference date: 15-08-2022 Through 18-08-2022",
}