Automated Verification of Electrum Wallet
Automated Verification of Electrum Wallet
复制标题
电子钱包的自动验证
DOI：
10.1007/978-3-662-53357-4_3
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
M. Rusinowitch
中科院分区：
文献类型：
--
作者：
Mathieu Turuani;T. Voegtlin;M. Rusinowitch
我们用Aslan++对Electrum比特币钱包使用的双因素认证协议进行了形式化建模。这使我们能够对钱包进行自动分析，并表明对于Dolv姚模型[Dolev 1981]中的标准场景，它是安全的。这要归功于协议分析器的一些高级功能，例如可以指定(I)带有子句的新的入侵者演绎规则和(Ii)不可演绎约束。
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.