An extensive formal analysis of multi-factor authentication protocols

EasyChair Preprint no. 79

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 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

@Booklet{EasyChair:79,
  author = {Charlie Jacomme and Steve Kremer},
  title = {An extensive formal analysis of multi-factor authentication protocols},
  howpublished = {EasyChair Preprint no. 79},
  doi = {10.29007/xrx7},
  year = {EasyChair, 2018}}