Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA

TL;DR

This paper presents a fully automated cryptographic protocol analysis of Yubico's YubiKey and YubiHSM devices using Maude-NPA, successfully verifying security properties and uncovering known vulnerabilities.

Contribution

It introduces a novel automated analysis approach for complex cryptographic APIs involving time, mutable memory, event sequences, and exclusive-or reasoning.

Findings

Proved security properties of YubiKey

Discovered known attacks on YubiHSM

Demonstrated the effectiveness of Maude-NPA for complex protocols

Abstract

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.