An extensive formal analysis of multi-factor authentication protocols
EasyChair Preprint 79
15 pages•Date: April 20, 2018Abstract
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 multi-factor 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.
Keyphrases: Authentication, automated verification, formal analysis, multi-factor, protocol verification