-
题名基于SPIN的MIXCOIN协议形式化分析与验证
被引量：1
- 1
-
-
作者
王西忠
肖美华
杨科
宋佳雯
朱志亮
-
机构
华东交通大学软件学院
-
出处
《广西大学学报（自然科学版）》
CAS
北大核心
2020年第6期1404-1412,共9页
-
基金
国家自然科学基金资助项目(61562026,61962020)
江西省主要学科学术和技术带头人资助计划项目(20172BCB22015)。
-
文摘
区块链混币机制协议是保障区块链安全和隐私的有效手段之一。MIXCOIN协议是一种典型的区块链混币机制协议,针对MIXCOIN协议可能存在泄漏用户地址关联性,导致协议不满足匿名性的问题,提出MIXCOIN协议形式化抽象表示方法,简化协议主体个数,约简加解密钥串表示,定义比特币转移函数,有效地解决了复杂协议难以形式化表示的问题。同时改进Dolev-Yao攻击者建模方法,引入敌手控制通道,可以更好地分析匿名通信协议。运用模型检测工具SPIN对MIXCOIN协议的认证性和匿名性进行验证,结果表明,协议存在中间人攻击和重放攻击,泄漏用户端混币地址的关联性,MIXCOIN协议只满足认证性而不满足匿名性。
-
关键词
混币机制
mixcoin协议
匿名性
形式化方法
模型检测
-
Keywords
mixed coins mechanism
mixcoin protocol
anonymity
formal method
model checking
-
分类号
TP18
[自动化与计算机技术—控制理论与控制工程]
-
