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

Antonio González-BurgeƱo1, Damián Aparicio2, Santiago Escobar2, Catherine Meadows3, José Meseguer4


1   University of Oslo, Norway.
2   DSIC-ELP, Universitat Politècnica de València, Spain.
3   Naval Research Laboratory, Washington DC, USA.
4   University of Illinois at Urbana-Champaign, USA.


In this web page we provide the source files of the Yubikey and the YubiHSM protocols and their corresponding attack patterns
    also sources files of our specification of YubiHSM using exclusive-or using the latest version of Tamarin (1.4.0) :

    Note that you will need both Maude and Maude NPA tools to execute both protocols; find a ZIP file containing both tools Maude with NPA

Find below the specification and the analysis result of both YubiKey and YubiHSM as included in our submitted paper:


YubiKey

YubiHSM


    YubiKey output attack (b)
      Correspondence between pressing the button on a YubiKey and a successful login. In other words, a successful login must have been preceded by a button pressed for the same counter value.
    • Yubikey specification
    • Yubikey output attack (b)

Find below the rewritten specification of YubiHSM to use exclusive-or and checked that both attacks on YubiHSM can be carried out by this recent version of Tamarin.

    YubiHSM
      The specification include the necessary modifications to work with exclusive-or and with the new lemma for validate attack(e) if the intruder has no access to the server running YubiKey, it can use previous YubiHSM nonces to obtain AES keys.
    • YubiHSM specification
    • Execution trace
    YubiHSM multiset
      The specification include the necessary modifications to work with exclusive-or and with the new lemma for validate attack(e) if the intruder has no access to the server running YubiKey, it can use previous YubiHSM nonces to obtain AES keys.
    • YubiHSM multiset specification
    • Execution trace