SPOOC: Automated Verification of Electrum Wallet

Automated Verification of Electrum Wallet

Mathieu Turuani, Thomas Voegtlin, and Michael Rusinowitch. Automated Verification of Electrum Wallet. In 3rd Workshop on Bitcoin and Blockchain Research, Christ Church, Barbados, February 2016.
doi:0.1007/978-3-662-53357-4_3

Download

[PDF] [HTML]

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.

BibTeX

@inproceedings{TVR-bitcoin16,
  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. },
  TITLE =	 {Automated Verification of Electrum Wallet},
  AUTHOR =	 {Turuani, Mathieu and Voegtlin, Thomas and
                  Rusinowitch, Michael},
  URL =		 {https://hal.inria.fr/hal-01256397},
  BOOKTITLE =	 {{3rd Workshop on Bitcoin and Blockchain Research}},
  ADDRESS =	 {Christ Church, Barbados},
  YEAR =	 2016,
  MONTH =	 Feb,
  PDF =
                  {https://hal.inria.fr/hal-01256397/file/longversion.pdf},
  doi =		 {0.1007/978-3-662-53357-4_3},
}