基于CPN的智能合约回滚攻击形式化验证OA
由于区块链具有数据加密和不可篡改等特性,能够保障用户匿名性及数据安全性,博彩行业在区块链上发行彩票,借助智能合约实现自动开奖。区块链具有回滚机制,如果被不法分子利用交易回滚,撤销不符合自己期望的执行结果,从而达成回滚攻击的目的,造成交易抵赖等安全问题。该文选取彩票类Lottery智能合约,使用着色Petri网(Colored Petri Net,CPN)对Lottery合约进行形式化验证:通过CPN Tools建模工具对合约整体及攻击操作进行可视化建模,建立CPN模型;之后对模型进行仿真和状态空间分析,验证了Lottery合约中潜在的回滚攻击漏洞。
李东萌;黄静;韩红桂;公备
北京工业大学信息学部,北京100124 计算智能与系统北京市重点实验室,北京100124北京工业大学信息学部,北京100124 计算智能与系统北京市重点实验室,北京100124北京工业大学信息学部,北京100124 计算智能与系统北京市重点实验室,北京100124北京工业大学信息学部,北京100124 计算智能与系统北京市重点实验室,北京100124
信息技术与安全科学
着色Petri网回滚攻击形式化验证智能合约区块链
《计算机应用与软件》 2026 (7)
P.338-345,361,9
国家重点研发计划项目(2020YFB1005903,2022YFB3305800)。
评论