Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt

Andreas Hülsing; Matthias Meijers; Pierre-Yves Strub

Paper 2022/351

Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt

Andreas Hülsing, 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.

Metadata

Available format(s): PDF
Category: Public-key cryptography
Publication info: Preprint. MINOR revision.
Keywords: public-key cryptography post-quantum cryptography formal verification Saber EasyCrypt
Contact author(s): fv-saber-pke @ mmeijers com
History: 2022-05-10: revised; 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},
      note = {\url{https://eprint.iacr.org/2022/351}},
      url = {https://eprint.iacr.org/2022/351}
}