{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T20:28:39Z","timestamp":1782937719153,"version":"3.54.5"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2021,1,21]],"date-time":"2021-01-21T00:00:00Z","timestamp":1611187200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR","award":["Sequoia"],"award-info":[{"award-number":["Sequoia"]}]},{"name":"ERC","award":["No 645865-SPOOC"],"award-info":[{"award-number":["No 645865-SPOOC"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Priv. Secur."],"published-print":{"date-parts":[[2021,5,31]]},"abstract":"<jats:p>\n            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\u2014variants of\n            <jats:italic>Google 2-step<\/jats:italic>\n            and\n            <jats:italic>FIDO\u2019s U2F<\/jats:italic>\n            (Yubico\u2019s Security Key token). The analysis is completely automated, generating systematically all combinations of threat scenarios for each of the protocols and using the P\n            <jats:sc>ROVERIF<\/jats:sc>\n            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\n            <jats:italic>Google 2-step<\/jats:italic>\n            that improves security in several threat scenarios.\n          <\/jats:p>","DOI":"10.1145\/3440712","type":"journal-article","created":{"date-parts":[[2021,1,21]],"date-time":"2021-01-21T11:31:58Z","timestamp":1611228718000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["An Extensive Formal Analysis of Multi-factor Authentication Protocols"],"prefix":"10.1145","volume":"24","author":[{"given":"Charlie","family":"Jacomme","sequence":"first","affiliation":[{"name":"LSV, CNRS, ENS, Paris-Saclay, Inria, and Universit\u00e9 Paris-Saclay"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steve","family":"Kremer","sequence":"additional","affiliation":[{"name":"LORIA, Inria Nancy-Grand Est, CNRS, and Universit\u00e9 de Lorraine"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127586"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/373243.360213"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38631-2_63"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.30"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.21"},{"key":"e_1_2_1_6_1","volume-title":"Dirk Balfanz, Alexei Czeskis, Arnar Birgisson, Jeff Hodges, Michael B. Jones, Rolf Lindemann, and J. C. Jones.","author":"Bharadwaj Vijay","year":"2017","unstructured":"Vijay Bharadwaj , Hubert Le Van Gong , Dirk Balfanz, Alexei Czeskis, Arnar Birgisson, Jeff Hodges, Michael B. Jones, Rolf Lindemann, and J. C. Jones. 2017 . Web Authentication : An API for Accessing Public Key Credentials. Retrieved from https:\/\/www.w3.org\/TR\/2017\/WD-webauthn-20171205\/. Vijay Bharadwaj, Hubert Le Van Gong, Dirk Balfanz, Alexei Czeskis, Arnar Birgisson, Jeff Hodges, Michael B. Jones, Rolf Lindemann, and J. C. Jones. 2017. Web Authentication: An API for Accessing Public Key Credentials. Retrieved from https:\/\/www.w3.org\/TR\/2017\/WD-webauthn-20171205\/."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1561\/3300000004"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.44"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1981.32"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.49"},{"key":"e_1_2_1_11_1","unstructured":"FIDO. 2018. Universal 2nd Factor (U2F). Retrieved from https:\/\/fidoalliance.org\/specs\/fido-u2f-v1.2-ps-20170411\/FIDO-U2F-COMPLETE-v1.2-ps-20170411.pdf.  FIDO. 2018. Universal 2nd Factor (U2F). Retrieved from https:\/\/fidoalliance.org\/specs\/fido-u2f-v1.2-ps-20170411\/FIDO-U2F-COMPLETE-v1.2-ps-20170411.pdf."},{"key":"e_1_2_1_12_1","volume-title":"Google 2 Step Verification.Retrieved","author":"Google","year":"2018","unstructured":"Google 2018. Google 2 Step Verification.Retrieved January 2018 from https:\/\/www.google.com\/landing\/2step\/. Google 2018. Google 2 Step Verification.Retrieved January 2018 from https:\/\/www.google.com\/landing\/2step\/."},{"key":"e_1_2_1_13_1","volume-title":"Theofanos","author":"Grassi Paul A.","year":"2017","unstructured":"Paul A. Grassi , James L. Fenton , Elaine M. Newton , Ray A. Perlner , Andrew R. Regenscheid , William E. Burr , Justin P. Richer , Naomi B. Lefkovitz , Jamie M. Danker , Kristen K. Choong , Yee-Yin Greene , and Mary F . Theofanos . 2017 . NIST Special Publication 800-63B: Digital Identity Guidelines\u2014Authentication and Lifecycle Management. Retrieved from https:\/\/doi.org\/10.6028\/NIST.SP.800-63b. 10.6028\/NIST.SP.800-63b Paul A. Grassi, James L. Fenton, Elaine M. Newton, Ray A. Perlner, Andrew R. Regenscheid, William E. Burr, Justin P. Richer, Naomi B. Lefkovitz, Jamie M. Danker, Kristen K. Choong, Yee-Yin Greene, and Mary F. Theofanos. 2017. NIST Special Publication 800-63B: Digital Identity Guidelines\u2014Authentication and Lifecycle Management. Retrieved from https:\/\/doi.org\/10.6028\/NIST.SP.800-63b."},{"key":"e_1_2_1_14_1","volume-title":"Fenton","author":"Grassi Paul A.","year":"2017","unstructured":"Paul A. Grassi , Michael E. Garcia , and James L . Fenton . 2017 . NIST Special Publication 800-63-3: Digital Identity Guidelines. Retrieved from https:\/\/doi.org\/10.6028\/NIST.SP.800-63-3. 10.6028\/NIST.SP.800-63-3 Paul A. Grassi, Michael E. Garcia, and James L. Fenton. 2017. NIST Special Publication 800-63-3: Digital Identity Guidelines. Retrieved from https:\/\/doi.org\/10.6028\/NIST.SP.800-63-3."},{"key":"e_1_2_1_15_1","volume-title":"Spectre Attacks: Exploiting Speculative Execution.","author":"Kocher Paul","year":"2018","unstructured":"Paul Kocher , Daniel Genkin , Daniel Gruss , Werner Haas , Mike Hamburg , Moritz Lipp , Stefan Mangard , Thomas Prescher , Michael Schwarz , and Yuval Yarom . 2018 . Spectre Attacks: Exploiting Speculative Execution. Retrieved from https:\/\/spectreattack.com\/spectre.pdf. Paul Kocher, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2018. Spectre Attacks: Exploiting Speculative Execution. Retrieved from https:\/\/spectreattack.com\/spectre.pdf."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-160556"},{"key":"#cr-split#-e_1_2_1_17_1.1","doi-asserted-by":"crossref","unstructured":"Robert K\u00fcnnemann and Graham Steel. 2013. YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM. Springer Berlin 257--272. DOI:https:\/\/doi.org\/10.1007\/978-3-642-38004-4_17 10.1007\/978-3-642-38004-4_17","DOI":"10.1007\/978-3-642-38004-4_17"},{"key":"#cr-split#-e_1_2_1_17_1.2","doi-asserted-by":"crossref","unstructured":"Robert K\u00fcnnemann and Graham Steel. 2013. YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM. Springer Berlin 257--272. DOI:https:\/\/doi.org\/10.1007\/978-3-642-38004-4_17","DOI":"10.1007\/978-3-642-38004-4_17"},{"key":"e_1_2_1_18_1","unstructured":"Moritz Lipp Michael Schwarz Daniel Gruss Thomas Prescher Werner Haas Stefan Mangard Paul Kocher Daniel Genkin Yuval Yarom and Mike Hamburg. 2018. Meltdown. Retrieved from https:\/\/meltdownattack.com\/meltdown.pdf.  Moritz Lipp Michael Schwarz Daniel Gruss Thomas Prescher Werner Haas Stefan Mangard Paul Kocher Daniel Genkin Yuval Yarom and Mike Hamburg. 2018. Meltdown. Retrieved from https:\/\/meltdownattack.com\/meltdown.pdf."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/359168.359172"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 10th International Symposium on Foundations 8 Practice of Security,Lecture Notes in Computer Science. Springer.","author":"Pereira Olivier","year":"2017","unstructured":"Olivier Pereira , Florentin Rochet , and Cyrille Wiedling . 2017 . Formal analysis of the Fido 1.x protocol . In Proceedings of the 10th International Symposium on Foundations 8 Practice of Security,Lecture Notes in Computer Science. Springer. Olivier Pereira, Florentin Rochet, and Cyrille Wiedling. 2017. Formal analysis of the Fido 1.x protocol. In Proceedings of the 10th International Symposium on Foundations 8 Practice of Security,Lecture Notes in Computer Science. Springer."},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Andrey Popov Magnus Nystrom Dirk Balfanz Adam Langley Nick Harper and Jeff Hodges. 2018. Token Binding over HTTP. Retrieved from draft-ietf-tokbind-https-12 and https:\/\/datatracker.ietf.org\/doc\/html\/draft-ietf-tokbind-https-12.  Andrey Popov Magnus Nystrom Dirk Balfanz Adam Langley Nick Harper and Jeff Hodges. 2018. Token Binding over HTTP. Retrieved from draft-ietf-tokbind-https-12 and https:\/\/datatracker.ietf.org\/doc\/html\/draft-ietf-tokbind-https-12.","DOI":"10.17487\/RFC8473"},{"key":"e_1_2_1_22_1","unstructured":"Source files 2018. Proverif source files and scripts. https:\/\/gitlab.inria.fr\/cjacomme\/multi-factor-authentication-proverif-examples.  Source files 2018. Proverif source files and scripts. https:\/\/gitlab.inria.fr\/cjacomme\/multi-factor-authentication-proverif-examples."},{"key":"e_1_2_1_23_1","unstructured":"G Suite team. 2017. G Suite updates. Retrieved from https:\/\/gsuiteupdates.googleblog.com\/2017\/02\/improved-phone-prompts-for-2-step.html.  G Suite team. 2017. G Suite updates. Retrieved from https:\/\/gsuiteupdates.googleblog.com\/2017\/02\/improved-phone-prompts-for-2-step.html."},{"key":"e_1_2_1_24_1","volume-title":"Retrieved","author":"Yubikey Yubico","year":"2018","unstructured":"Yubico 2018. FIDO Yubikey . Retrieved January 2018 from https:\/\/www.yubico.com\/solutions\/fido-u2f\/. Yubico 2018. FIDO Yubikey. Retrieved January 2018 from https:\/\/www.yubico.com\/solutions\/fido-u2f\/."}],"container-title":["ACM Transactions on Privacy and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3440712","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3440712","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:18Z","timestamp":1750195698000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3440712"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,21]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,5,31]]}},"alternative-id":["10.1145\/3440712"],"URL":"https:\/\/doi.org\/10.1145\/3440712","relation":{},"ISSN":["2471-2566","2471-2574"],"issn-type":[{"value":"2471-2566","type":"print"},{"value":"2471-2574","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,21]]},"assertion":[{"value":"2019-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-01-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}