Paper 2023/246
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium
, University of Porto, INESC TEC, Max Planck Institute for Security and Privacy, Max Planck Institute for Security and Privacy, Inria Centre at Université Côte d'Azur, Eindhoven University of Technology, Max Planck Institute for Security and Privacy, University of Maryland, College Park, University of Maryland, College ParkAbstract
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.
Metadata
- Available format(s)
-
PDF
- Category
- Public-key cryptography
- Publication info
- Preprint.
- Keywords
- 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 - History
- 2023-02-21: approved
- 2023-02-21: received
- See all versions
- Short URL
- https://ia.cr/2023/246
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2023/246,
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{https://eprint.iacr.org/2023/246}},
url = {https://eprint.iacr.org/2023/246}
}
