| 引用本文: | 吕永阳,冯睿韬,王子墨,刘俊超,吴汉炜,李晓红.XCMP协议的形式化验证与改进: 提升跨链交互安全性.软件学报,2026,37(6):2477-2509 |
| |
|
| |
|
|
| 本文已被：浏览 710次 下载 668次 |
码上扫一扫！ |
|
|
| XCMP协议的形式化验证与改进: 提升跨链交互安全性 |
|
吕永阳1, 冯睿韬2, 王子墨1, 刘俊超1, 吴汉炜1,3, 李晓红1
|
|
1.天津大学 智能与计算学部, 天津 300354;2.Faculty of Science and Engineering, Southern Cross University, Gold Coast QLD 4225, Australia;3.海南大学 网络空间安全学院, 海南 海口 570228
|
|
| 摘要: |
| 随着区块链技术及应用的不断发展, 人们对区块链之间的交互需求日益增加. 然而, 不同区块链系统之间缺乏有效的互操作性, 限制了区块链技术的进一步发展. 为解决区块链异构互联互通问题, 跨链技术应运而生, 并迅速成为新的研究热点. 其中, 跨链消息传递(cross-chain massage passing, XCMP)协议作为最流行的跨链通信协议之一, 不仅提供了一个安全高效的跨链通信机制, 还为未来的区块链创新和应用提供了广阔的平台. 然而, XCMP协议仍然处于不断发展和完善的阶段, 面临着重放攻击、拒绝服务攻击、延迟攻击等安全问题. 对XCMP协议进行了形式化验证与改进, 旨在为在其基础上构建更安全、功能更丰富的去中心化应用提供坚实支撑. 首先, 利用一种以经典集合论和一阶谓词逻辑为基础的形式化描述语言——Z语言, 对XCMP协议的10条关键安全目标、协议内容进行总结提炼与形式化建模, 并借助支持Z语言的自动化验证工具Z/EVES验证XCMP协议是否满足安全目标. 验证结果表明XCMP协议未满足3条安全目标. 其次, 通过对验证结果进行全面分析, 针对XCMP协议未满足的安全目标, 引入承诺机制、监督机制和轮询机制, 提出了E-XCMP (enhanced cross-chain message passing)协议. 最后, 将E-XCMP协议形式化建模, 并借助安全协议分析工具Scyther和自动化验证工具Z/EVES对其安全性和可靠性进行评估, 评估结果表明E-XCMP协议不仅满足上述未满足要求的3条安全目标, 并且能够有效解决重放攻击、拒绝服务攻击、延迟攻击等安全问题, 具有较好的安全性和可靠性. |
| 关键词: 跨链协议 跨链消息传递(XCMP) 形式化分析 Z语言 Scyther 模型检测 Pedersen承诺 |
| DOI：10.13328/j.cnki.jos.007479 |
| 分类号:TP311 |
| 基金项目:国家重点研发计划(2021YFF1201102) |
|
| Formal Verification and Improvement of XCMP Protocol: Improving Security of Cross-chain Interaction |
|
LYU Yong-Yang1, FENG Rui-Tao2, WANG Zi-Mo1, LIU Jun-Chao1, WU Han-Wei1,3, LI Xiao-Hong1
|
|
1.College of Intelligence and Computing, Tianjin University, Tianjin 300354, China;2.Faculty of Science and Engineering, Southern Cross University, Gold Coast QLD 4225, Australia;3.School of Cyberspace Security, Hainan University, Haikou 570228, China
|
| Abstract: |
| With the continuous development of blockchain technology and applications, the demand for interaction between blockchains is increasing. However, the lack of effective interoperability between different blockchain systems limits the further development of blockchain technology. To address the problem of heterogeneous interconnection between blockchains, cross-chain technology has emerged and quickly become a prominent research topic. Specifically, the XCMP protocol, one of the most popular cross-chain communication protocols, not only provides a secure and efficient communication mechanism but also offers a broad platform for future blockchain innovation and applications. However, the cross-chain massage passing (XCMP) protocol is still in a phase of continuous development and improvement, facing security challenges such as replay attacks, denial of service attacks, and delay attacks. This study formally verifies and improves the XCMP protocol, aiming to provide solid support for the development of more secure and feature-rich decentralized applications based on it. First, Z language, a formal description language based on classical set theory and first-order predicate logic, is used to summarize, refine, and formally model the 10 key security goals and protocol contents of the XCMP protocol. The security goals are then verified using Z/EVES, an automated verification tool supporting the Z language. The verification results show that the XCMP protocol does not meet three of the security goals. Second, after a comprehensive analysis of the verification results, the study introduces a commitment mechanism, a supervision mechanism, and a polling mechanism to address unmet security goals of the XCMP protocol, proposing an enhanced cross-chain message passing (E-XCMP) protocol. Finally, the E-XCMP protocol is formally modeled, and its security and reliability are evaluated using the security protocol analysis tool Scyther and the automatic verification tool Z/EVES. The evaluation results show that the E-XCMP protocol not only meets the three previously unmet security goals but also effectively solves security issues such as replay attacks, denial of service attacks, and delay attacks, demonstrating strong security and reliability. |
| Key words: cross-chain protocol cross-chain message passing (XCMP) formal analysis Z language Scyther model checking Pedersen commitment |
|
|
|
|
