An extensive formal analysis of multi-factor authentication protocols

Charlie Jacomme 1 Steve Kremer 2
2 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01922022
Contributor : Steve Kremer <>
Submitted on : Wednesday, November 14, 2018 - 11:39:12 AM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on : Friday, February 15, 2019 - 1:41:19 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Charlie Jacomme, Steve Kremer. An extensive formal analysis of multi-factor authentication protocols. CSF'2018 - 31st IEEE Computer Security Foundations Symposium, Jul 2018, Oxford, United Kingdom. ⟨10.1109/CSF.2018.00008⟩. ⟨hal-01922022⟩

Share

Metrics

Record views

116

Files downloads

311