A Formal Treatment of Hardware Wallets

Myrto Arapinis; Andriana Gkaniatsou; Dimitris Karakostas; Aggelos Kiayias

doi:10.1007/978-3-030-32101-7_26

A Formal Treatment of Hardware Wallets

Myrto Arapinis, Andriana Gkaniatsou, Dimitris Karakostas, Aggelos Kiayias

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Financial Cryptography and Data Security
Subtitle of host publication	23rd International Conference, FC 2019
Publisher	Springer
Pages	426-445
Number of pages	20
ISBN (Electronic)	978-3-030-32101-7
ISBN (Print)	978-3-030-32100-0
DOIs	https://doi.org/10.1007/978-3-030-32101-7_26
Publication status	Published - 30 Sept 2019
Event	Financial Cryptography and Data Security 2019 - St. Kitts Marriott Resort, St Kitts, Saint Kitts and Nevis Duration: 18 Feb 2019 → 22 Feb 2019 https://fc19.ifca.ai/

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Publisher	Springer, Cham
Volume	11598
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Financial Cryptography and Data Security 2019
Abbreviated title	FC 2019
Country/Territory	Saint Kitts and Nevis
City	St Kitts
Period	18/02/19 → 22/02/19
Internet address	https://fc19.ifca.ai/

Access to Document

10.1007/978-3-030-32101-7_26Licence: All Rights Reserved

A Formal Treatment of Hardware WalletsAccepted author manuscript, 540 KB

https://link.springer.com/chapter/10.1007/978-3-030-32101-7_26Licence: All Rights Reserved

FENTEC-Functional Encryption Technologies
Kiayias, A.
EU government bodies
1/01/18 → 28/02/21
Project: Research
Verification of cryptographic protocols: modular analysis of equivalence properties
Arapinis, M.
EPSRC
1/11/16 → 30/09/18
Project: Research

Cite this

@inproceedings{7e7d7566c15d4a90bd779d74c384ffb5,

title = "A Formal Treatment of Hardware Wallets",

abstract = "Bitcoin, being the most successful cryptocurrency, has been repeatedly attacked with many users losing their funds. The industry{\textquoteright}s response to securing the user{\textquoteright}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 paperprovides 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{\textquoteright}s components, their interaction and the potential threats. We deduce the wallet{\textquoteright}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.",

author = "Myrto Arapinis and Andriana Gkaniatsou and Dimitris Karakostas and Aggelos Kiayias",

year = "2019",

month = sep,

day = "30",

doi = "10.1007/978-3-030-32101-7_26",

language = "English",

isbn = "978-3-030-32100-0",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "426--445",

booktitle = "Financial Cryptography and Data Security",

address = "United Kingdom",

note = "Financial Cryptography and Data Security 2019, FC 2019 ; Conference date: 18-02-2019 Through 22-02-2019",

url = "https://fc19.ifca.ai/",

}

Arapinis, M, Gkaniatsou, A, Karakostas, D & Kiayias, A 2019, A Formal Treatment of Hardware Wallets. in Financial Cryptography and Data Security : 23rd International Conference, FC 2019. Lecture Notes in Computer Science (LNCS), vol. 11598, Springer, pp. 426-445, Financial Cryptography and Data Security 2019, St Kitts, Saint Kitts and Nevis, 18/02/19. https://doi.org/10.1007/978-3-030-32101-7_26

TY - GEN

T1 - A Formal Treatment of Hardware Wallets

AU - Arapinis, Myrto

AU - Gkaniatsou, Andriana

AU - Karakostas, Dimitris

AU - Kiayias, Aggelos

PY - 2019/9/30

Y1 - 2019/9/30

N2 - 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 paperprovides 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.

AB - 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 paperprovides 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.

U2 - 10.1007/978-3-030-32101-7_26

DO - 10.1007/978-3-030-32101-7_26

M3 - Conference contribution

SN - 978-3-030-32100-0

T3 - Lecture Notes in Computer Science (LNCS)

SP - 426

EP - 445

BT - Financial Cryptography and Data Security

PB - Springer

T2 - Financial Cryptography and Data Security 2019

Y2 - 18 February 2019 through 22 February 2019

ER -

A Formal Treatment of Hardware Wallets

Abstract / Description of output

Publication series

Conference

Access to Document

Fingerprint

Projects

FENTEC-Functional Encryption Technologies

Verification of cryptographic protocols: modular analysis of equivalence properties

Cite this