Skip to Main content Skip to Navigation
New interface
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
Contributor : Michaël Rusinowitch Connect in order to contact the contributor
Submitted on : Thursday, January 14, 2016 - 5:05:21 PM
Last modification on : Friday, February 4, 2022 - 3:30:15 AM
Long-term archiving on: : Friday, November 11, 2016 - 6:23:58 AM


Files produced by the author(s)


  • HAL Id : hal-01256397, version 1



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⟩



Record views


Files downloads