An extensive formal analysis of multi-factor authentication protocols

Charlie Jacomme and Steve Kremer. An extensive formal analysis of multi-factor authentication protocols. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18), pp. 1–15, IEEE Computer Society Press, Oxford, UK, July 2018.
doi:10.1109/CSF.2018.00008

Download

[PDF] [HTML] 

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 used in so-called multifactor authentication protocols. In this paper we define a detailed threat model for this kind of protocols: 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 malwares, 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. 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. Our analysis highlights weaknesses and strengths of the different protocols, and allows us to suggest several small modifications of the existing protocols which are easy to implement, yet improve their security in several threat scenarios.

BibTeX

@inproceedings{JK-csf18,
  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 used in so-called multifactor
                  authentication protocols. In this paper we define a
                  detailed threat model for this kind of protocols:
                  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 malwares, 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. 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.  Our analysis
                  highlights weaknesses and strengths of the different
                  protocols, and allows us to suggest several small
                  modifications of the existing protocols which are
                  easy to implement, yet improve their security in
                  several threat scenarios.},
  address =	 {Oxford, UK},
  author =	 {Jacomme, Charlie and Kremer, Steve},
  booktitle =	 {{P}roceedings of the 31st IEEE Computer Security
                  Foundations Symposium (CSF'18)},
  month =	 jul,
  pages =	 1--15,
  publisher =	 {{IEEE} Computer Society Press},
  title =	 {An extensive formal analysis of multi-factor
                  authentication protocols},
  year =	 2018,
  acronym =	 {{CSF}'18},
  nmonth =	 7,
                  ={https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=8429292},
  doi =		 {10.1109/CSF.2018.00008}
}