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.
