nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Formal Analysis of the FIDO 1.x Protocol

verfasst von : Olivier Pereira, Florentin Rochet, Cyrille Wiedling

Erschienen in: Foundations and Practice of Security

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Formal Analysis of Combinations of Secure Protocols

Nächstes Kapitel A Roadmap for High Assurance Cryptography

Nur mit Berechtigung zugänglich

[ACC+08]

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)

[AF01]

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

[All]

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

[All16a]

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

[All16b]

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

[BCFS10]

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)

[BHVOS12]

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)

[Bla01]

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

[CCK12]

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 CrossRef

[Che14]

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 CrossRef

[CS13]

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

[CW12]

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 CrossRef

[Goo]

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

[GPS05]

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 CrossRef

[KK16]

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

[KR05]

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 CrossRef

[KS12]

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 CrossRef

[KT08]

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

[Low96]

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 CrossRef

[NS78]

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

[PW03]

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 CrossRef

[Roca]

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

[Rocb]

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

[WRP]

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

Titel: Formal Analysis of the FIDO 1.x Protocol
verfasst von: Olivier Pereira
Florentin Rochet
Cyrille Wiedling
Verlag: Springer International Publishing
Buch: Foundations and Practice of Security
Print ISBN: 978-3-319-75649-3

Electronic ISBN: 978-3-319-75650-9

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-75650-9_5

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"