We present a methodology for formally modelling and verifying multi-factor authentication (MFA) schemes employed in eIDAS digital identity cards. This methodology adopts an interface-based threat model to comprehensively analyse potential vulnerabilities and enumerate threat scenarios based on an attacker’s capabilities. Using CIE, Italy’s eIDAS-compliant digital identity card, as guiding example, we show how to automatically generate ProVerif models of these scenarios. Our analysis exposes some vulnerabilities; e.g., an attacker with Level 1 credentials can gain Level 2 authentication, even without compromising any interface. To address these vulnerabilities, we propose minor modifications to the protocols, whose correctness is proved by further formal analysis.

Formal Analysis of Multi-Factor Authentication Schemes in Digital Identity Cards

Van Eeden R.;Miculan M.
2025-01-01

Abstract

We present a methodology for formally modelling and verifying multi-factor authentication (MFA) schemes employed in eIDAS digital identity cards. This methodology adopts an interface-based threat model to comprehensively analyse potential vulnerabilities and enumerate threat scenarios based on an attacker’s capabilities. Using CIE, Italy’s eIDAS-compliant digital identity card, as guiding example, we show how to automatically generate ProVerif models of these scenarios. Our analysis exposes some vulnerabilities; e.g., an attacker with Level 1 credentials can gain Level 2 authentication, even without compromising any interface. To address these vulnerabilities, we propose minor modifications to the protocols, whose correctness is proved by further formal analysis.
2025
9783031773815
9783031773822
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/1297965
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact