An Extensive Formal Analysis of Multi-factor Authentication Protocols
Charlie Jacomme and Steve Kremer. An Extensive Formal Analysis of Multi-factor Authentication Protocols. ACM Transactions on Privacy and Security, 24(2):13:1–13:34, January 2021.
doi:10.1145/3440712
Download
Abstract
Passwords are still the most widespread means for authenticating users, even though they have been shown to create huge security problems. This motivated the use of additional authentication mechanisms in so-called multi-factor authentication protocols. In this article, we define a detailed threat model for this kind of protocol: While in classical protocol analysis attackers control the communication network, we take into account that many communications are performed over TLS channels, that computers may be infected by different kinds of malware, that attackers could perform phishing, and that humans may omit some actions. We formalize this model in the applied pi calculus and perform an extensive analysis and comparison of several widely used protocols—variants of Google 2-step and FIDO’s U2F (Yubico’s Security Key token). The analysis is completely automated, generating systematically all combinations of threat scenarios for each of the protocols and using the PROVERIF tool for automated protocol analysis. To validate our model and attacks, we demonstrate their feasibility in practice, even though our experiments are run in a laboratory environment. Our analysis highlights weaknesses and strengths of the different protocols. It allows us to suggest several small modifications of the existing protocols that are easy to implement, as well as an extension of Google 2-step that improves security in several threat scenarios.
BibTeX
@Article{JK-tops21,
author = {Jacomme, Charlie and Kremer, Steve},
abstract = {Passwords are still the most widespread means for
authenticating users, even though they have been
shown to create huge security problems. This
motivated the use of additional authentication
mechanisms in so-called multi-factor authentication
protocols. In this article, we define a detailed
threat model for this kind of protocol: While in
classical protocol analysis attackers control the
communication network, we take into account that
many communications are performed over TLS channels,
that computers may be infected by different kinds of
malware, that attackers could perform phishing, and
that humans may omit some actions. We formalize this
model in the applied pi calculus and perform an
extensive analysis and comparison of several widely
used protocols—variants of Google 2-step and FIDO’s
U2F (Yubico’s Security Key token). The analysis is
completely automated, generating systematically all
combinations of threat scenarios for each of the
protocols and using the PROVERIF tool for automated
protocol analysis. To validate our model and
attacks, we demonstrate their feasibility in
practice, even though our experiments are run in a
laboratory environment. Our analysis highlights
weaknesses and strengths of the different
protocols. It allows us to suggest several small
modifications of the existing protocols that are
easy to implement, as well as an extension of Google
2-step that improves security in several threat
scenarios.},
title = {An Extensive Formal Analysis of Multi-factor
Authentication Protocols},
journal = {ACM Transactions on Privacy and Security},
year = 2021,
volume = 24,
number = 2,
pages = {13:1--13:34},
year = 2021,
month = jan,
nmonth = 1,
url = {https://dl.acm.org/doi/10.1145/3440712},
doi = {10.1145/3440712},
}