More Web Proxy on the site http://driver.im/

Article

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

Authors:

Andreas Hülsing,

Matthias Meijers,

Pierre-Yves StrubAuthors Info & Claims

Advances in Cryptology – CRYPTO 2022: 42nd Annual International Cryptology Conference, CRYPTO 2022, Santa Barbara, CA, USA, August 15–18, 2022, Proceedings, Part I

Pages 622 - 653

https://doi.org/10.1007/978-3-031-15802-5_22

Published: 15 August 2022 Publication History

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 [inline-graphic not available: see fulltext] security and

δ

-correctness properties, i.e., the properties required to transform the public-key encryption scheme into an [inline-graphic not available: see fulltext] 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’s public-key encryption scheme indeed satisfies the desired security and correctness properties.

References

[1]

Almeida, J.B., Barbosa, M., Barthe, G., Grégoire, B., Koutsos, A., Laporte, V., Oliveira, T., Strub, P.-Y.: The last mile: high-assurance and high-speed cryptographic implementations. In: 2020 IEEE Symposium on Security and Privacy, pp. 965–982. IEEE Computer Society Press, May 2020

[2]

Banerjee A, Peikert C, and Rosen A Pointcheval D and Johansson T Pseudorandom functions and lattices Advances in Cryptology – EUROCRYPT 2012 2012 Heidelberg Springer 719-737

Digital Library

[3]

Barbosa, M., Barthe, G., Bhargavan, K., Blanchet, B., Cremers, C., Liao, K., Parno, B.: SoK: computer-aided cryptography. In: 2021 IEEE Symposium on Security and Privacy (SP), pp. 777–795. IEEE Computer Society, May 2021

[4]

Barbosa, M., Barthe, G., Fan, X., Grégoire, B., Hung, S.-H., Katz, J., Strub, P.-Y., Wu, X., Zhou, L.: EasyPQC: verifying post-quantum cryptography. Cryptology ePrint Archive, Report 2021/1253 (2021)

[5]

Barthe G, Crespo JM, Grégoire B, Kunz C, and Zanella Béguelin S Beringer L and Felty A Computer-aided cryptographic proofs Interactive Theorem Proving 2012 Heidelberg Springer 11-27

[6]

Bellare M and Rogaway P Vaudenay S The security of triple encryption and a framework for code-based game-playing proofs Advances in Cryptology - EUROCRYPT 2006 2006 Heidelberg Springer 409-426

Digital Library

[7]

Boneh D, Dagdelen Ö, Fischlin M, Lehmann A, Schaffner C, and Zhandry M Lee DH and Wang X Random Oracles in a quantum world Advances in Cryptology – ASIACRYPT 2011 2011 Heidelberg Springer 41-69

Digital Library

[8]

Cremers, C., Horvat, M., Hoyland, J., Scott, S., van der Merwe, T.: A comprehensive symbolic analysis of TLS 1.3. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.) ACM CCS 2017, pp. 1773–1788. ACM Press, October/November 2017

[9]

D’Anvers, J.-P.: Design and security analysis of lattice-based post-quantum encryption. Ph.D. dissertation, KU Leuven Arenberg Doctoral School, May 2021

[10]

D’Anvers J-P, Karmakar A, Sinha Roy S, and Vercauteren F Joux A, Nitaj A, and Rachidi T Saber: Module-LWR based key exchange, CPA-secure encryption and CCA-secure KEM Progress in Cryptology – AFRICACRYPT 2018 2018 Cham Springer 282-305

[11]

Duman, J., Hövelmanns, K., Kiltz, E., Lyubashevsky, V., Seiler, G.: Faster Kyber and Saber via a generic Fujisaki-Okamoto transform for multi-user security in the QROM (2021)

[12]

Hofheinz D, Hövelmanns K, and Kiltz E Kalai Y and Reyzin L A modular analysis of the Fujisaki-Okamoto transformation Theory of Cryptography 2017 Cham Springer 341-371

Digital Library

[13]

Hülsing, A., Meijers, M., Strub, P.-Y.: Formal verification of Saber’s public-key encryption scheme in EasyCrypt. Cryptology ePrint Archive, Paper 2022/351 (2022). https://eprint.iacr.org/2022/351

[14]

Koblitz N and Menezes AJ Critical perspectives on provable security: fifteen years of “another look” papers Adv. Math. Commun. 2019 13 4 517-558

[15]

Lazar, D., Chen, H., Wang, X., Zeldovich, N.: Why does cryptographic software fail? A case study and open problems. In: Proceedings of 5th Asia-Pacific Workshop on Systems, APSys 2014, pp. 1–7. Association for Computing Machinery (2014)

[16]

Mosca M Cybersecurity in an era with quantum computers: will we be ready? IEEE Security & Privacy 2018 16 5 38-41

Digital Library

[17]

Shor, P.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proceedings 35th Annual Symposium on Foundations of Computer Science, pp. 124–134 (1994)

[18]

Unruh D Moriai S and Wang H Post-quantum verification of Fujisaki-Okamoto Advances in Cryptology – ASIACRYPT 2020 2020 Cham Springer 321-352

Digital Library

[19]

Yan SY Quantum Attacks on Public-Key Cryptosystems 2013 1 Boston Springer

Cited By

Almeida JArranz Olmos SBarbosa MBarthe GDupressoir FGrégoire BLaporte VLéchenet JLow COliveira TPacheco HQuaresma MSchwabe PStrub P(2024)Formally Verifying KyberAdvances in Cryptology – CRYPTO 202410.1007/978-3-031-68379-4_12(384-421)Online publication date: 18-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-68379-4_12
Barbosa MDupressoir FGrégoire BHülsing AMeijers MStrub P(2023)Machine-Checked Security for as in RFC 8391 and Advances in Cryptology – CRYPTO 202310.1007/978-3-031-38554-4_14(421-454)Online publication date: 20-Aug-2023
https://dl.acm.org/doi/10.1007/978-3-031-38554-4_14

Index Terms

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

Index terms have been assigned to the content through auto-classification.

Recommendations

Secure public-key encryption scheme without random oracles

Since the first practical and secure public-key encryption scheme without random oracles proposed by Cramer and Shoup in 1998, Cramer-Shoup's scheme and its variants remained the only practical and secure public-key encryption scheme without random ...
Public-Key encryption from ID-Based encryption without one-time signature
OTM'06: Proceedings of the 2006 international conference on On the Move to Meaningful Internet Systems: AWeSOMe, CAMS, COMINF, IS, KSinBIT, MIOS-CIAO, MONET - Volume Part I

Design a secure public key encryption scheme and its security proof are one of the main interests in cryptography In 2004, Canetti, Halevi and Katz [8] constructed a public key encryption (PKE) from a selective identity-based encryption scheme with a ...
A new public-key encryption scheme

This paper proposes a new public-key encryption scheme which removes one element from the public-key tuple of the original Cramer-Shoup scheme. As a result, a ciphertext is not a quadruple but a triple at the cost of a strong assumption, the third ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Advances in Cryptology – CRYPTO 2022: 42nd Annual International Cryptology Conference, CRYPTO 2022, Santa Barbara, CA, USA, August 15–18, 2022, Proceedings, Part I

Aug 2022

821 pages

ISBN:978-3-031-15801-8

DOI:10.1007/978-3-031-15802-5

Editors:
Yevgeniy Dodis
https://ror.org/0190ak572New York University, New York, NY, USA
,
Thomas Shrimpton
https://ror.org/02y3ad647University of Florida, Gainesville, FL, USA

© International Association for Cryptologic Research 2022.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 15 August 2022

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Almeida JArranz Olmos SBarbosa MBarthe GDupressoir FGrégoire BLaporte VLéchenet JLow COliveira TPacheco HQuaresma MSchwabe PStrub P(2024)Formally Verifying KyberAdvances in Cryptology – CRYPTO 202410.1007/978-3-031-68379-4_12(384-421)Online publication date: 18-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-68379-4_12
Barbosa MDupressoir FGrégoire BHülsing AMeijers MStrub P(2023)Machine-Checked Security for as in RFC 8391 and Advances in Cryptology – CRYPTO 202310.1007/978-3-031-38554-4_14(421-454)Online publication date: 20-Aug-2023
https://dl.acm.org/doi/10.1007/978-3-031-38554-4_14

View Options

View options

Media

Figures

Other

Tables

View Table of Contents