International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

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

Authors:
Manuel Barbosa , University of Porto (FCUP) and INESC TEC
Gilles Barthe , Max Planck Institute for Security and Privacy, Germany
Christian Doczkal , Max Planck Institute for Security and Privacy, Germany
Jelle Don , Centrum Wiskunde & Informatica, The Netherlands
Serge Fehr , Centrum Wiskunde & Informatica and Leiden University, The Netherlands
Benjamin Grégoire , Université Côte d’Azur, Inria, France
Yu-Hsuan Huang , Centrum Wiskunde & Informatica, The Netherlands
Andreas Hülsing , Eindhoven University of Technology, The Netherlands
Yi Lee , University of Maryland, United States
Xiaodi Wu , University of Maryland, United States
Download:
DOI: 10.1007/978-3-031-38554-4_12 (login may be required)
Search ePrint
Search Google
Presentation: Slides
Conference: CRYPTO 2023
Abstract: 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.
BibTeX
@inproceedings{crypto-2023-33203,
  title={Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium},
  publisher={Springer-Verlag},
  doi={10.1007/978-3-031-38554-4_12},
  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},
  year=2023
}