Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA
This work addresses security verification for hardware authentication devices, but it is incremental as it builds on prior automated analyses.
The paper tackled the automated formal verification of YubiKey and YubiHSM devices using Maude-NPA, proving properties for YubiKey and finding known attacks on YubiHSM in a completely automated way.
In this paper, we perform an automated analysis of two devices developed by Yubico: YubiKey, designed to authenticate a user to network-based services, and YubiHSM, Yubicos hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol analyzer. Although previous work has been done applying automated tools to these devices, to the best of our knowledge there has been no completely automated analysis to date. This is not surprising, because both YubiKey and YubiHSM, which make use of cryptographic APIs, involve a number of complex features: (i) discrete time in the form of Lamport clocks, (ii) a mutable memory for storing previously seen keys or nonces, (iii) event-based properties that require an analysis of sequences of actions, and (iv) reasoning modulo exclusive-or. In this work, we have been able to both prove properties of YubiKey and find the known attacks on the YubiHSM, in a completely automated way beyond the capabilities of previous work in the literature.