Paper 2023/246

Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium

Manuel Barbosa, University of Porto, INESC TEC
Gilles Barthe, Max Planck Institute for Security and Privacy
Christian Doczkal, Max Planck Institute for Security and Privacy
Jelle Don, Centrum Wiskunde & Informatica
Serge Fehr, Centrum Wiskunde & Informatica, Leiden University
Benjamin Grégoire, Inria Centre at Université Côte d'Azur
Yu-Hsuan Huang, Centrum Wiskunde & Informatica
Andreas Hülsing, Eindhoven University of Technology
Yi Lee, Max Planck Institute for Security and Privacy, University of Maryland, College Park
Xiaodi Wu, University of Maryland, College Park

We extend and consolidate the security justification for the Dilithium signature scheme. In particular, we identify a subtle but crucial gap that appears in several ROM and QROM security proofs for signature schemes that are based on the Fiat-Shamir with aborts paradigm, including Dilithium. The gap lies in the CMA-to-NMA reduction and was uncovered when trying to formalize a variant of the QROM security proof by Kiltz, Lyubashevsky, and Schaffner (Eurocrypt 2018). The gap was confirmed by the authors, and there seems to be no simple patch for it. We provide new, fixed proofs for the affected CMA-to-NMA reduction, both for the ROM and the QROM, and we perform a concrete security analysis for the case of Dilithium to show that the claimed security level is still valid after addressing the gap. Furthermore, we offer a fully mechanized ROM proof for the CMA-security of Dilithium in the EasyCrypt proof assistant. Our formalization includes several new tools and techniques of independent interest for future formal verification results.

Available format(s)
Public-key cryptography
Publication info
Fiat-Shamir with abortspost-quantum cryptographyrandom oracle modelformal verificationDilithiumQROM
Contact author(s)
mbb @ fc up pt
gilles barthe @ mpi-sp org
christian doczkal @ mpi-sp org
jelle don @ cwi nl
serge fehr @ cwi nl
benjamin gregoire @ inria fr
yhh @ cwi nl
andreas @ huelsing net
ylee1228 @ umd edu
xiaodiwu @ umd edu
2023-02-21: approved
2023-02-21: received
See all versions
Short URL
Creative Commons Attribution


      author = {Manuel Barbosa and Gilles Barthe and Christian Doczkal and Jelle Don and Serge Fehr and Benjamin Grégoire and Yu-Hsuan Huang and Andreas Hülsing and Yi Lee and Xiaodi Wu},
      title = {Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium},
      howpublished = {Cryptology ePrint Archive, Paper 2023/246},
      year = {2023},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.