A Formal Treatment of Hardware Wallets

  • Myrto Arapinis
  • Andriana Gkaniatsou
  • Dimitris KarakostasEmail author
  • Aggelos Kiayias
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11598)


Bitcoin, being the most successful cryptocurrency, has been repeatedly attacked with many users losing their funds. The industry’s response to securing the user’s assets is to offer tamper-resistant hardware wallets. Although such wallets are considered to be the most secure means for managing an account, no formal attempt has been previously done to identify, model and formally verify their properties. This paper provides the first formal model of the Bitcoin hardware wallet operations. We identify the properties and security parameters of a Bitcoin wallet and formally define them in the Universal Composition (UC) Framework. We present a modular treatment of a hardware wallet ecosystem, by realizing the wallet functionality in a hybrid setting defined by a set of protocols. This approach allows us to capture in detail the wallet’s components, their interaction and the potential threats. We deduce the wallet’s security by proving that it is secure under common cryptographic assumptions, provided that there is no deviation in the protocol execution. Finally, we define the attacks that are successful under a protocol deviation, and analyze the security of commercially available wallets.



This work was partially supported by the EPSRC grant EP/P002692/1. Research also partly supported by the H2020 project FENTEC, No. 780108.


  1. 1.
    KeepKey (2018). Accessed 1 Sept 2018
  2. 2.
    Ledger Receive Address Attack (2018). Accessed 19 Sept 2018
  3. 3.
    Trezor (2018). Accessed 1 Sept 2018
  4. 4.
    Alois, J.: Ethereum parity hack may impact ETH 500.000 or 146 million (2017). Accessed 1 Sept 2018
  5. 5.
    Atzei, N., Bartoletti, M., Lande, S., Zunino, R.: A formal model of bitcoin transactions. Cryptology ePrint Archive, Report 2017/1124 (2017).
  6. 6.
    Badertscher, C., Maurer, U., Tschudi, D., Zikas, V.: Bitcoin as a transaction ledger: a composable treatment. In: Katz, J., Shacham, H. (eds.) CRYPTO 2017. LNCS, vol. 10401, pp. 324–356. Springer, Cham (2017). Scholar
  7. 7.
    Bamert, T., Decker, C., Wattenhofer, R., Welten, S.: BlueWallet: the secure bitcoin wallet. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 65–80. Springer, Cham (2014). Scholar
  8. 8.
    Bonneau, J., Miller, A., Clark, J., Narayanan, A., Kroll, J.A., Felten, E.W.: SoK: research perspectives and challenges for bitcoin and cryptocurrencies. In: 2015 IEEE Symposium on Security and Privacy (SP), pp. 104–121. IEEE (2015)Google Scholar
  9. 9.
    Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols, pp. 136–145 (2001)Google Scholar
  10. 10.
    Canetti, R.: Universally composable signatures, certification and authentication. Cryptology ePrint Archive, Report 2003/239 (2003).
  11. 11.
    Canetti, R., Krawczyk, H.: Universally composable notions of key exchange and secure channels. Cryptology ePrint Archive, Report 2002/059 (2002).
  12. 12.
    Garay, J., Kiayias, A., Leonardos, N.: The bitcoin backbone protocol: analysis and applications. In: Oswald, E., Fischlin, M. (eds.) EUROCRYPT 2015. LNCS, vol. 9057, pp. 281–310. Springer, Heidelberg (2015). Scholar
  13. 13.
    Gentilal, M., Martins, P., Sousa, L.: Trustzone-backed bitcoin wallet. In: Proceedings of the Fourth Workshop on Cryptography and Security in Computing Systems, pp. 25–28. ACM (2017)Google Scholar
  14. 14.
    Gkaniatsou, A., Arapinis, M., Kiayias, A.: Low-level attacks in bitcoin wallets. In: Nguyen, P., Zhou, J. (eds.) ISC 2017. LNCS, vol. 10599. Springer, Cham (2017). Scholar
  15. 15.
    Heilman, E., Kendler, A., Zohar, A., Goldberg, S.: Eclipse attacks on bitcoin’s peer-to-peer network. In: 24th USENIX Security Symposium (USENIX Security 15), pp. 129–144. USENIX Association, Washington, D.C. (2015).
  16. 16.
    Hsiao, H.C., et al.: A study of user-friendly hash comparison schemes. In: 2009 Annual Computer Security Applications Conference, ACSAC 2009, pp. 105–114. IEEE (2009)Google Scholar
  17. 17.
    Johnson, D., Menezes, A., Vanstone, S.: The elliptic curve digital signature algorithm (ECDSA). Int. J. Inf. Secur. 1(1), 36–63 (2001). Scholar
  18. 18.
    Lim, I.-K., Kim, Y.-H., Lee, J.-G., Lee, J.-P., Nam-Gung, H., Lee, J.-K.: The analysis and countermeasures on security breach of bitcoin. In: Murgante, B., et al. (eds.) ICCSA 2014. LNCS, vol. 8582, pp. 720–732. Springer, Cham (2014). Scholar
  19. 19.
    Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008)Google Scholar
  20. 20.
    Parker, L.: Bitcoin stealing malware evolves again (2016). Accessed 1 Sept 2018
  21. 21.
    Pass, R., Seeman, L., Shelat, A.: Analysis of the blockchain protocol in asynchronous networks. In: Coron, J.-S., Nielsen, J.B. (eds.) EUROCRYPT 2017. LNCS, vol. 10211, pp. 643–673. Springer, Cham (2017). Scholar
  22. 22.
    Penard, W., van Werkhoven, T.: On the secure hash algorithm family. In: Cryptography in Context, pp. 1–18 (2008)Google Scholar
  23. 23.
    Tan, J., Bauer, L., Bonneau, J., Cranor, L.F., Thomas, J., Ur, B.: Can unicorns help users compare crypto key fingerprints? In: Proceedings of the 2017 CHI Conference on Human Factors in Computing Systems, pp. 3787–3798. ACM (2017)Google Scholar
  24. 24.
    Uzun, E., Karvonen, K., Asokan, N.: Usability analysis of secure pairing methods. In: Dietrich, S., Dhamija, R. (eds.) FC 2007. LNCS, vol. 4886, pp. 307–324. Springer, Heidelberg (2007). Scholar
  25. 25.
    Vasek, M., Bonneau, J., Castellucci, R., Keith, C., Moore, T.: The bitcoin brain drain: examining the use and abuse of bitcoin brain wallets. In: Grossklags, J., Preneel, B. (eds.) FC 2016. LNCS, vol. 9603, pp. 609–618. Springer, Heidelberg (2017). Scholar
  26. 26.
    Volotikin, S.: Software attacks on hardware wallets. Black Hat USA 2018 (2018)Google Scholar
  27. 27.
    Wuille, P.: Hierarchical Deterministic Wallets (2018). Accessed 1 Sept 2018
  28. 28.
    Huang, D.Y., et al.: Botcoin: monetizing stolen cycles (2014)Google Scholar

Copyright information

© International Financial Cryptography Association 2019

Authors and Affiliations

  • Myrto Arapinis
    • 1
  • Andriana Gkaniatsou
    • 1
  • Dimitris Karakostas
    • 1
    • 2
    Email author
  • Aggelos Kiayias
    • 1
    • 2
  1. 1.University of EdinburghEdinburghUK
  2. 2.IOHKEdinburghUK

Personalised recommendations