Skip to Main content Skip to Navigation
Conference papers

Automated Verification of Electrum Wallet

Mathieu Turuani 1 Thomas Voegtlin 2 Michael Rusinowitch 1
1 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We introduce a formal modeling in ASLan++ of the two-factor authentication protocol used by the Electrum Bitcoin wallet. This allows us to perform an automatic analysis of the wallet and show that it is secure for standard scenarios in Dolev Yao model [Dolev 1981]. The result could be derived thanks to some advanced features of the protocol analyzer such as the possibility to specify i) new intruder deduction rules with clauses and ii) non-deducibility constraints.
Complete list of metadata

Cited literature [5 references]  Display  Hide  Download

https://hal.inria.fr/hal-01256397
Contributor : Michaël Rusinowitch Connect in order to contact the contributor
Submitted on : Thursday, January 14, 2016 - 5:05:21 PM
Last modification on : Saturday, October 16, 2021 - 11:26:10 AM
Long-term archiving on: : Friday, November 11, 2016 - 6:23:58 AM

File

longversion.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01256397, version 1

Collections

Citation

Mathieu Turuani, Thomas Voegtlin, Michael Rusinowitch. Automated Verification of Electrum Wallet. 3rd Workshop on Bitcoin and Blockchain Research, Feb 2016, Christ Church, Barbados. ⟨hal-01256397⟩

Share

Metrics

Record views

540

Files downloads

1150