Cryptology ePrint Archive: Report 2022/351
Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt
Andreas Hülsing and Matthias Meijers and Pierre-Yves Strub
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.
Category / Keywords: public-key cryptography / public-key cryptography, post-quantum cryptography, formal verification, Saber, EasyCrypt
Date: received 14 Mar 2022, last revised 10 May 2022
Contact author: fv-saber-pke at mmeijers com
Available format(s): PDF | BibTeX Citation
Version: 20220510:100642 (All versions of this report)
Short URL: ia.cr/2022/351
[ Cryptology ePrint archive ]