Skip to Main content Skip to Navigation
Conference papers

YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM

Robert Künnemann 1 Graham Steel 2 
1 SECSI - Security of information systems
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : The Yubikey is a small hardware device designed to authenticate a user against network-based services. Despite its widespread adoption (over a million devices have been shipped by Yubico to more than 20 000 customers including Google and Microsoft), the Yubikey protocols have received relatively little security analysis in the academic literature. In the first part of this paper, we give a formal model for the operation of the Yubikey one-time password (OTP) protocol. We prove security properties of the protocol for an unbounded number of fresh OTPs using a protocol analysis tool, tamarin. In the second part of the paper, we analyze the security of the protocol with respect to an adversary that has temporary access to the authentication server. To address this scenario, Yubico offers a small Hardware Security Module (HSM) called the YubiHSM, intended to protect keys even in the event of server compromise. We show if the same YubiHSM configuration is used both to set up Yubikeys and run the authentication protocol, then there is inevitably an attack that leaks all of the keys to the attacker. Our discovery of this attack lead to a Yubico security advisory in February 2012. For the case where separate servers are used for the two tasks, we give a configuration for which we can show using the same verification tool that if an adversary that can compromise the server running the Yubikey-protocol, but not the server used to set up new Yubikeys, then he cannot obtain the keys used to produce one-time passwords.
Document type :
Conference papers
Complete list of metadata
Contributor : Ben Smyth Connect in order to contact the contributor
Submitted on : Wednesday, September 18, 2013 - 5:37:27 PM
Last modification on : Friday, January 21, 2022 - 3:19:30 AM

Links full text



Robert Künnemann, Graham Steel. YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM. Revised Selected Papers of the 8th Workshop on Security and Trust Management (STM'12), 2012, Pisa, Italy. pp.257-272, ⟨10.1007/978-3-642-38004-4_17⟩. ⟨hal-00863378⟩



Record views