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)
YubiKey output attack (c)
YubiKey output attack Regular Execution |
|
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.
|
|