Room "Sala Seminari" - Abacus Building (U14)
Breaking and Fixing CIEID Formal Verification of the Italian e-ID Multi-Factor Authentication
Speaker
Prof. Marino Miculan
Department of Mathematics, Computer Science and Physics
University of Udine
Abstract: As digital identity becomes the backbone of EU public services under the eIDAS regulation, the security of Multi-Factor Authentication (MFA) schemes is paramount. However, designing error-free MFA protocols remains a significant challenge. In this talk, we present a formal methodology for modeling and verifying the MFA schemes, taking the Italian Carta di Identità Elettronica (CIE) as a case study.
Using an interface-based threat model, we represent the eID architecture as a distributed system where an attacker can gain varying levels of control (read/write) over devices like computers and smartphones. We demonstrate how to automatically generate and verify hundreds of attack scenarios using ProVerif, a state-of-the-art security protocol verifier.
As a result, we identify a "timing attack" in the push-notification scheme that allows an attacker with only Level 1 credentials (username/password) to achieve Level 2 authentication. We propose minor, backward-compatible modifications to the protocols and provide formal proof that these changes effectively mitigate the discovered vulnerabilities.
This work highlights the essential role of formal methods in identifying non-trivial logical flaws in national-scale security infrastructures.
Bio: Marino Miculan is Full Professor of Computer Science at the University of Udine, where he leads the Laboratory of Models and Applications of Distributed Systems (MADS) and coordinates the local unit of the CINI National Cybersecurity Laboratory and the MadrHacks ethical hacking team.
His research focuses on formal methods for the modeling and verification of concurrent and distributed systems, cybersecurity, programming language semantics, and the application of mathematical methods to computer science.
He is (co)author of more than 100 scientific publications in international peer-reviewed journals and conference proceedings, and has participated in more than 15 national and international research projects. He is serving on numerous program committees and organizing committees of leading conferences in the areas of formal methods and cybersecurity. He is also actively engaged in outreach and training activities on cybersecurity and digital technologies.
Contact person for the seminar: alex.graudenzi@unimib.it