Paper 2022/351
Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt
, Eindhoven University of Technology, Eindhoven University of Technology, MetaAbstract
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.
Metadata
- Available format(s)
-
PDF
- Category
- Public-key cryptography
- Publication info
- A major revision of an IACR publication in CRYPTO 2022
- DOI
- 10.1007/978-3-031-15802-5_22
- Keywords
- public-key cryptographypost-quantum cryptographyformal verificationSaberEasyCrypt
- Contact author(s)
-
andreas @ huelsing net
research @ mmeijers com
pierre-yves @ strub nu - History
- 2023-01-13: last of 2 revisions
- 2022-03-18: received
- See all versions
- Short URL
- https://ia.cr/2022/351
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2022/351,
author = {Andreas Hülsing and Matthias Meijers and Pierre-Yves Strub},
title = {Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt},
howpublished = {Cryptology ePrint Archive, Paper 2022/351},
year = {2022},
doi = {10.1007/978-3-031-15802-5_22},
note = {\url{https://eprint.iacr.org/2022/351}},
url = {https://eprint.iacr.org/2022/351}
}
