Abstract
We introduce a formal modeling in ASLan++ of the twofactor 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.
Cite
CITATION STYLE
Turuani, M., Voegtlin, T., & Rusinowitch, M. (2016). Automated verification of electrum wallet. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9604 LNCS, pp. 27–42). Springer Verlag. https://doi.org/10.1007/978-3-662-53357-4_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
