Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Foundations and Practice of Security

FPS 2017: Foundations and Practice of Security pp 68–82Cite as

Formal Analysis of the FIDO 1.x Protocol

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 10723))

Abstract

This paper presents a formal analysis of FIDO, a protocol developed by the FIDO Alliance project, and which aims to provide either a passwordless experience or an extra security layer for user authentication over the Internet. We model the protocol using the applied pi-calculus and run our analysis using ProVerif. Our analysis shows that ignoring some optional steps of the standard could lead to the implementation of a flawed authentication process. On the contrary, we prove that these steps are sufficient to ensure the expected security properties.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Armando, A., Carbone, R., Compagna, L., Cuellar, J., Tobarra, L.: Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for Google apps. In: Proceedings of the 6th ACM workshop on Formal Methods in Security Engineering, pp. 1–10. ACM (2008)

    Google Scholar 

  2. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th ACM Symposium on Principles of Programming Languages (POPL) (2001)

    Google Scholar 

  3. FIDO Alliance: FIDO Documentation. https://fidoalliance.org/specifications/download/

  4. FIDO Alliance: Fido security reference, September 2016. https://fidoalliance.org/specs/fido-u2f-v1.1-id-20160915/fido-security-ref-v1.1-id-20160915.html

  5. FIDO Alliance: FIDO U2F JavaScript API, September 2016. https://fidoalliance.org/specs/fido-u2f-v1.1-id-20160915/fido-u2f-javascript-api-v1.1-id-20160915.html

  6. Bortolozzo, M., Centenaro, M., Focardi, R., Steel, G.: Attacking and fixing PKCS#11 security tokens. In: ACM Conference on Computer and Communications Security (CCS) (2010)

    Google Scholar 

  7. Bonneau, J., Herley, C., Van Oorschot, P.C., Stajano, F.: The quest to replace passwords: a framework for comparative evaluation of web authentication schemes. In: 2012 IEEE Symposium on Security and Privacy (SP), pp. 553–567. IEEE (2012)

    Google Scholar 

  8. Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW) (2001)

    Google Scholar 

  9. Chadha, R., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 108–127. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28869-2_6

    Chapter  Google Scholar 

  10. Cheval, V.: APTE: an algorithm for proving trace equivalence. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 587–592. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_50

    Chapter  Google Scholar 

  11. Cortier, V., Smyth, B.: Attacking and fixing Helios: an analysis of ballot secrecy. J. Comput. Secur. 21(1), 89–148 (2013)

    Article  Google Scholar 

  12. Cortier, V., Wiedling, C.: A formal analysis of the Norwegian E-voting protocol. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 109–128. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28641-4_7

    Chapter  Google Scholar 

  13. Google: Chrome browser download. http://google-chrome.en.uptodown.com/ubuntu/old. Accessed 13 Jan 2016

  14. Groß, T., Pfitzmann, B., Sadeghi, A.-R.: Browser model for security analysis of browser-based protocols. In: di Vimercati, S.C., Syverson, P., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 489–508. Springer, Heidelberg (2005). https://doi.org/10.1007/11555827_28

    Chapter  Google Scholar 

  15. Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. J. Comput. Secur. 24(5), 583–616 (2016)

    Article  Google Scholar 

  16. Kremer, S., Ryan, M.: Analysis of an electronic voting protocol in the applied Pi calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186–200. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31987-0_14

    Chapter  Google Scholar 

  17. Künnemann, R., Steel, G.: YubiSecure? Formal security analysis results for the Yubikey and YubiHSM. In: Jøsang, A., Samarati, P., Petrocchi, M. (eds.) STM 2012. LNCS, vol. 7783, pp. 257–272. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38004-4_17

    Chapter  Google Scholar 

  18. Küsters, R., Truderung, T.: Reducing protocol analysis with XOR to the XOR-free Case in the Horn Theory based approach. CoRR (2008)

    Google Scholar 

  19. Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61042-1_43

    Chapter  Google Scholar 

  20. Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)

    Article  MATH  Google Scholar 

  21. Pfitzmann, B., Waidner, M.: Federated identity-management protocols. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2003. LNCS, vol. 3364, pp. 153–174. Springer, Heidelberg (2005). https://doi.org/10.1007/11542322_20

    Chapter  Google Scholar 

  22. Rochet, F.: Fido compliant library and Java web application example. https://github.com/frochet/java-u2flib-server. Accessed 13 Jan 2016

  23. Rochet, F.: Modified fido client as a chrome extension. https://github.com/frochet/u2f-ref-code. Accessed 13 Jan 2016

  24. Wiedling, C., Rochet, F., Pereira, O.: Proverif implementation of the fido protocol. https://git-crypto.elen.ucl.ac.be/frochet/fido_proverif

Download references

Acknowledgement

We would like to thank the anonymous reviewers for their valuable feedback. This work was partially supported by the Innoviris C-Cure project and the Region Wallonne TrueDev project.

Author information

Authors and Affiliations

  1. UCL Crypto Group, Louvain-la-Neuve, Belgium

    Olivier Pereira, Florentin Rochet & Cyrille Wiedling

Authors
  1. Olivier Pereira
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Florentin Rochet
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Cyrille Wiedling
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Florentin Rochet .

Editor information

Editors and Affiliations

  1. University of Lorraine, Villers-lès-Nancy, France

    Abdessamad Imine

  2. Polytechnique de Montréal, Montreal, Québec, Canada

    José M. Fernandez

  3. LORIA, Vandœuvre-lès-Nancy, France

    Jean-Yves Marion

  4. Université du Québec en Outaouais, Gatineau, Québec, Canada

    Luigi Logrippo

  5. Télécom SudParis, Evry Cedex, France

    Joaquin Garcia-Alfaro

A Attack on a Real FIDO Authentication

A Attack on a Real FIDO Authentication

We detail the steps to test the attack from Sect. 5.2 in a local test-bed.

  • Clone repositories [Roca, Rocb] and download chrome [Goo].

  • From chrome tab extensions, activate the developer mode and load the unpacked u2f-chrome-extension.

  • Inside java-u2flib-server, do mvn clean install then cd inside u2f-server-demo and configure two .yml files, one for the compromised server and one for the honest server. Use the available model, you just need to provide a different port number.

  • Run:

    • java -jar target/u2flib-server-demo.jar server [your_consigDishonest_file.yml] localhost [port_honest_server] https://localhost:[port_dishonest_server] ]&

    • java -jar target/u2flib-server-demo.jar server [your_consigHonest_file.yml]

      http://localhost:[port_honest_server]&

  • Use chrome and your FIDO-compliant authenticator to register in both services then try to authenticate.

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Pereira, O., Rochet, F., Wiedling, C. (2018). Formal Analysis of the FIDO 1.x Protocol. In: Imine, A., Fernandez, J., Marion, JY., Logrippo, L., Garcia-Alfaro, J. (eds) Foundations and Practice of Security. FPS 2017. Lecture Notes in Computer Science(), vol 10723. Springer, Cham. https://doi.org/10.1007/978-3-319-75650-9_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-75650-9_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-75649-3

  • Online ISBN: 978-3-319-75650-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation