Formal modelling and verifying eIDAS multi-factor authentication with interface-based threat analysis - Software and Systems Modeling

This paper introduces a methodology for the formal modelling and verification of multi-factor authentication (MFA) schemes utilized in eIDAS digital identity cards. Our approach employs an interface-based threat model to systematically analyse potential vulnerabilities and enumerate a range of threat scenarios based on varying attacker capabilities. We demonstrate the automated generation of ProVerif models for these scenarios using the Italian Carta di Identità Elettronica (CIE), an eIDAS-compliant digital identity card, as a practical case study. Our analysis reveals several security weaknesses; notably, an attacker possessing only Level 1 (i.e. single-factor) credentials can, in certain circumstances, achieve Level 2 multi-factor authentication without needing to compromise any communication interface. To mitigate these vulnerabilities, we propose minor modifications to the protocols. Furthermore, at Level 3, our analysis shows that the authentication scheme relying on the CieID smartphone application presents a broader attack surface compared to the method employing a PC with a smart card reader. The interface-based modelling and analysis methodology presented in this work offers a valuable framework that can be adapted for the security assessment of other eIDAS digital identity cards.