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.
Type de document :
Communication dans un congrès
3rd Workshop on Bitcoin and Blockchain Research, Feb 2016, Christ Church, Barbados
Liste complète des métadonnées

Littérature citée [5 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01256397
Contributeur : Michaël Rusinowitch <>
Soumis le : jeudi 14 janvier 2016 - 17:05:21
Dernière modification le : jeudi 11 janvier 2018 - 06:27:43
Document(s) archivé(s) le : vendredi 11 novembre 2016 - 06:23:58

Fichier

longversion.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

347

Téléchargements de fichiers

356