A Formal Treatment of Hardware Wallets

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationFinancial Cryptography and Data Security
Subtitle of host publication23rd International Conference, FC 2019
PublisherSpringer, Cham
Number of pages20
ISBN (Electronic)978-3-030-32101-7
ISBN (Print)978-3-030-32100-0
Publication statusPublished - 30 Sept 2019
EventFinancial Cryptography and Data Security 2019 - St. Kitts Marriott Resort, St Kitts, Saint Kitts and Nevis
Duration: 18 Feb 201922 Feb 2019

Publication series

NameLecture Notes in Computer Science (LNCS)
PublisherSpringer, Cham
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceFinancial Cryptography and Data Security 2019
Abbreviated titleFC 2019
Country/TerritorySaint Kitts and Nevis
CitySt Kitts
Internet address


Dive into the research topics of 'A Formal Treatment of Hardware Wallets'. Together they form a unique fingerprint.

Cite this