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 metadatas

Cited literature [5 references]  Display  Hide  Download

https://hal.inria.fr/hal-01256397
Contributor : Michaël Rusinowitch <>
Submitted on : Thursday, January 14, 2016 - 5:05:21 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
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

428

Files downloads

678