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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.