[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1007/978-3-031-38554-4_14guideproceedingsArticle/Chapter ViewAbstractPublication PagesConference Proceedingsacm-pubtype
Article

Machine-Checked Security for  as in RFC 8391 and 

Published: 20 August 2023 Publication History

Abstract

This work presents a novel machine-checked tight security proof for —a stateful hash-based signature scheme that is (1) standardized in RFC 8391 and NIST SP 800-208, and (2) employed as a primary building block of, one of the signature schemes recently selected for standardization as a result of NIST’s post-quantum competition.
In 2020, Kudinov, Kiktenko, and Fedoro pointed out a flaw affecting the tight security proofs of and . For the case of, this flaw was fixed in a subsequent tight security proof by Hülsing and Kudinov. Unfortunately, employing the fix from this proof to construct an analogous tight security proof for would merely demonstrate security with respect to an insufficient notion.
At the cost of modeling the message-hashing function as a random oracle, we complete the tight security proof for and formally verify it using the EasyCrypt proof assistant. (Note that this merely extends the use of the random oracle model, as this model is already required in other parts of the security analysis to justify the currently standardized parameter values). As part of this endeavor, we formally verify the crucial step common to the security proofs of and that was found to be flawed before, thereby confirming that the core of the aforementioned security proof by Hülsing and Kudinov is correct.
As this is the first work to formally verify proofs for hash-based signature schemes in EasyCrypt, we develop several novel libraries for the fundamental cryptographic concepts underlying such schemes—e.g., hash functions and digital signature schemes—establishing a common starting point for future formal verification efforts. These libraries will be particularly helpful in formally verifying proofs of other hash-based signature schemes such as or .

References

[1]
Almeida, J.B., Baritel-Ruet, C., Barbosa, M., Barthe, G., Dupressoir, F., Grégoire, B., Laporte, V., Oliveira, T., Stoughton, A., Strub, P.-Y.: Machine-checked proofs for cryptographic standards: indifferentiability of sponge and secure high-assurance implementations of SHA-3. In: Cavallaro, L., Kinder, J., Wang, X., Katz, J. (eds.) ACM CCS 2019, pp. 1607–1622. ACM Press, Nov. (2019)
[2]
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 (2021)
[3]
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. In: Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, CCS 2021, New York, NY, USA, pp. 2564–2586. Association for Computing Machinery (2021)
[4]
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
[5]
Barthe G, Grégoire B, Lakhnech Y, and Zanella Béguelin S Kiayias A Beyond provable security verifiable IND-CCA security of OAEP Topics in Cryptology – CT-RSA 2011 2011 Heidelberg Springer 180-196
[6]
Bernstein, D.J., Hülsing, A., Kölbl, S., Niederhagen, R., Rijneveld, J., Schwabe, P.: The SPHINCS signature framework. In: Cavallaro, L., Kinder, J., Wang, X., Katz, J. (eds.) ACM CCS 2019, pp. 2129–2146. ACM Press (2019)
[7]
Bos, J.W., Hülsing, A., Renes, J., van Vredendaal, C.: Rapidly verifiable XMSS signatures. IACR TCHES 2021(1), 137–168 (2021). https://tches.iacr.org/index.php/TCHES/article/view/8730
[8]
Cooper, D., Apon, D., Dang, Q., Davidson, M., Dworkin, M., Miller, C.: Recommendation for stateful hash-based signature schemes (2020)
[9]
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 (2017)
[10]
Grilo AB, Hövelmanns K, Hülsing A, and Majenz C Tibouchi M and Wang H Tight adaptive reprogramming in the QROM Advances in Cryptology – ASIACRYPT 2021 2021 Cham Springer 637-667
[11]
Grumbling, E., Horowitz, M.: Quantum Computing: Progress and Prospects. National Academies of Sciences, Engineering, and Medicine. The National Academies Press, 1st edn. (2019)
[12]
Huelsing, A., Butin, D., Gazdag, S.-L., Rijneveld, J., Mohaisen, A.: XMSS: eXtended Merkle Signature Scheme. RFC 8391 (2018)
[13]
Hülsing A and Kudinov M Agrawal S and Lin D Recovering the tight security proof of SPHINCS Advances in Cryptology - ASIACRYPT 2022 2022 Cham Springer 3-33
[14]
Hülsing A, Meijers M, and Strub P-Y Dodis Y and Shrimpton T Formal verification of Saber’s public-key encryption scheme in EasyCrypt Advances in Cryptology - CRYPTO 2022 2022 Cham Springer 622-653
[15]
Hülsing A, Rijneveld J, and Song F Cheng C-M, Chung K-M, Persiano G, and Yang B-Y Mitigating multi-target attacks in hash-based signatures Public-Key Cryptography – PKC 2016 2016 Heidelberg Springer 387-416
[16]
Koblitz, N., Menezes, A.J.: Critical perspectives on provable security: fifteen years of “another look” papers. Adv. Math. Commun. 13(4), 517–558 (2019)
[17]
Kudinov, M., Kiktenko, E., Fedorov, A.: [pqc-forum] round 3 official comment: Sphincs+ (2020). https://csrc.nist.gov/CSRC/media/Projects/post-quantum-cryptography/documents/round-3/official-comments/Sphincs-Plus-round3-official-comment.pdf. Accessed 1 Feb 2022
[18]
McGrew, D., Curcio, M., Fluhrer, S.: Leighton-Micali Hash-Based Signatures. RFC 8554 (2019)
[19]
Mosca M Cybersecurity in an era with quantum computers: will we be ready? IEEE Secur. Priv. 2018 16 38-41
[20]
NIST. National Institute for Standards and Technology. announcing request for nominations for public-key post-quantum cryptographic algorithms (2016). https://csrc.nist.gov/News/2016/Public-Key-Post-Quantum-Cryptographic-Algorithms
[21]
NIST. National Institute for Standards and Technology. PQC standardization process: Announcing four candidates to be standardized, plus fourth round candidates (2022). https://csrc.nist.gov/News/2022/pqc-candidates-to-be-standardized-and-round-4
[22]
Perlner R, Kelsey J, and Cooper D Cheon JH and Johansson T Breaking category five SPHINCS with SHA-256 Post-Quantum Cryptography 2022 Cham Springer 501-522
[23]
Zhandry M Boldyreva A and Micciancio D How to record quantum queries, and applications to quantum indifferentiability CRYPTO 2019 2019 Heidelberg Springer 239-268

Cited By

View all
  • (2024)Formally Verifying KyberAdvances in Cryptology – CRYPTO 202410.1007/978-3-031-68379-4_12(384-421)Online publication date: 18-Aug-2024

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings
Advances in Cryptology – CRYPTO 2023: 43rd Annual International Cryptology Conference, CRYPTO 2023, Santa Barbara, CA, USA, August 20–24, 2023, Proceedings, Part V
Aug 2023
883 pages
ISBN:978-3-031-38553-7
DOI:10.1007/978-3-031-38554-4

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 20 August 2023

Author Tags

  1. EasyCrypt
  2. Formal Verification
  3. Machine-Checked Proofs
  4. Computer-Aided Cryptography

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 01 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Formally Verifying KyberAdvances in Cryptology – CRYPTO 202410.1007/978-3-031-68379-4_12(384-421)Online publication date: 18-Aug-2024

View Options

View options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media