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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Data and Artifact Availability
The artefact [17] includes ProVerif templates for all three Level 2 CieID protocols, scripts to instantiate them into formal models for all threat scenarios, and the complete results of the verification process.
References
Alaca, F., van Oorschot, P.C.: Device fingerprinting for augmenting web authentication: classification and analysis of methods. In: Proceedings of the 32nd Conference on Computer Security Applications, pp. 289–301. ACM (2016)
Armando, A., Carbone, R., Compagna, L., Cuellar, J., Tobarra, L.: Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for Google apps. In: Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering, pp. 1–10 (2008)
Bacci, G., Miculan, M.: Structural operational semantics for continuous state probabilistic processes. In: Pattinson, D., Schröder, L. (eds.) CMCS 2012. LNCS, vol. 7399, pp. 71–89. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32784-1_5
Bacci, G., Miculan, M.: Structural operational semantics for continuous state stochastic transition systems. J. Comput. Syst. Sci. 81(5), 834–858 (2015)
Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: 2017 IEEE Symposium on Security and Privacy (S &P), pp. 483–502 (2017)
Blanchet, B., et al.: Modeling and verifying security protocols with the applied pi calculus and ProVerif. Found. Trends Priv. Secur. 1, 1–135 (2016)
Burco, F., Miculan, M., Peressotti, M.: Towards a formal model for composable container systems. In: Proceedings of the 35th Annual ACM Symposium on Applied Computing, pp. 173–175 (2020)
Cook, A., Viganò, L.: Formal analysis of security protocols with movement. In: Proceedings of the Italian Conference on Cyber Security (ITASEC 2023). CEUR Workshop Proceedings, vol. 3488. CEUR-WS.org (2023)
Dumortier, J.: Regulation EU no 910/2014 on electronic identification and trust services for electronic transactions in the internal market (eIDAS regulation). In: EU Regulation of E-Commerce, pp. 256–289. Edward Elgar Publishing (2017)
Engelbertz, N., Erinola, N., Herring, D., Somorovsky, J., Mladenov, V., Schwenk, J.: Security analysis of eIDAS — the Cross-Country authentication scheme in Europe. In: 12th USENIX Workshop on Offensive Technologies (2018)
Gregušová, D., Halásová, Z., Peráček, T.: eIDAS regulation and its impact on national legislation: the case of the Slovak republic. Admin. Sci. 12(4), 187 (2022)
Jacomme, C., Kremer, S.: An extensive formal analysis of multi-factor authentication protocols. ACM Trans. Priv. Secur. 24, 1–34 (2021)
Kernighan, B., Ritchie, D.: The M4 macro processor. Technical report, Bell Laboratories Murray Hill (1977)
Lips, S., Bharosa, N., Draheim, D.: eIDAS implementation challenges: the case of Estonia and the Netherlands. In: Chugunov, A., Khodachek, I., Misnikov, Y., Trutnev, D. (eds.) EGOSE 2020. CCIS, vol. 1349, pp. 75–89. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-67238-6_6
Mainka, C., Mladenov, V., Feldmann, F., Krautwald, J., Schwenk, J.: Your software at my service: security analysis of SaaS single sign-on solutions in the cloud. In: Proceedings of the 6th ACM Workshop on Cloud Computing Security, pp. 93–104 (2014)
Miculan, M., Urban, C.: Formal analysis of Facebook Connect single sign-on authentication protocol. In: SofSem 2011, Proceedings of Student Research Forum, pp. 99–116. OKAT (2011)
Paier, M., Van Eeden, R., Miculan, M.: Formal Analysis of Multi-Factor Authentication Schemes in Digital Identity Cards - Artifact (2024). https://doi.org/10.5281/zenodo.12586055
Sharif, A., Ranzi, M., Carbone, R., Sciarretta, G., Marino, F.A., Ranise, S.: The eIDAS regulation: a survey of technological trends for European electronic identity schemes. Appl. Sci. 12(24), 12679 (2022)
Sinigaglia, F., Carbone, R., Costa, G., Zannone, N.: A survey on multi-factor authentication for online banking in the wild. Comput. Secur. 95, 101745 (2020)
Somorovsky, J., Heiderich, M., Jensen, M., Schwenk, J., Gruschka, N., Lo Iacono, L.: All your clouds are belong to us: security analysis of cloud management interfaces. In: Proceedings of the 3rd ACM Workshop on Cloud Computing Security Workshop, pp. 3–14 (2011)
Ullah, K., Rashid, I., Afzal, H., Iqbal, M.M.W., Bangash, Y.A., Abbas, H.: SS7 vulnerabilities-a survey and implementation of machine learning vs rule based filtering for detection of SS7 network attacks. IEEE Commun. Surv. Tutor.. 22(2), 1337–1371 (2020)
Acknowledgments
This research has been partially supported by the Department Strategic Project on Artificial Intelligence of the University of Udine (2020–25), and the project SERICS (PE00000014) under the NRRP MUR program funded by EU-NGEU.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Ethics declarations
Disclosure of Interests
The authors have no competing interests to declare that are relevant to the content of this article.
Rights and permissions
Copyright information
© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Paier, M., Van Eeden, R., Miculan, M. (2025). Formal Analysis of Multi-Factor Authentication Schemes in Digital Identity Cards. In: Madeira, A., Knapp, A. (eds) Software Engineering and Formal Methods. SEFM 2024. Lecture Notes in Computer Science, vol 15280. Springer, Cham. https://doi.org/10.1007/978-3-031-77382-2_24
Download citation
DOI: https://doi.org/10.1007/978-3-031-77382-2_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-77381-5
Online ISBN: 978-3-031-77382-2
eBook Packages: Computer ScienceComputer Science (R0)