Welcome to the resource topic for 2022/351
Title:
Formal Verification of Saber’s Public-Key Encryption Scheme in EasyCrypt
Authors: Andreas Hülsing, Matthias Meijers, 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.
ePrint: https://eprint.iacr.org/2022/351
Talk: https://www.youtube.com/watch?v=LU4RF0Ya008
Slides: https://iacr.org/submit/files/slides/2022/crypto/crypto2022/195/slides.pptx
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .