Page 158 - 《软件学报》2026年第6期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2026,37(6):2477−2509 [doi: 10.13328/j.cnki.jos.007479] [CSTR: 32375.14.jos.007479] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
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)
通信作者: 李晓红, E-mail: Xiaohongli@tju.edu.cn

摘 要: 随着区块链技术及应用的不断发展, 人们对区块链之间的交互需求日益增加. 然而, 不同区块链系统之间
缺乏有效的互操作性, 限制了区块链技术的进一步发展. 为解决区块链异构互联互通问题, 跨链技术应运而生, 并
迅速成为新的研究热点. 其中, 跨链消息传递 (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 承诺
中图法分类号: TP311

中文引用格式: 吕永阳, 冯睿韬, 王子墨, 刘俊超, 吴汉炜, 李晓红. XCMP协议的形式化验证与改进: 提升跨链交互安全性. 软件学
报, 2026, 37(6): 2477–2509. http://www.jos.org.cn/1000-9825/7479.htm
英文引用格式: Lyu Y, Feng RT, Wang ZM, Liu JC, Wu HW, Li XH. Formal Verification and Improvement of XCMP Protocol:
Improving Security of Cross-chain Interaction. Ruan Jian Xue Bao/Journal of Software, 2026, 37(6): 2477–2509 (in Chinese). http://
www.jos.org.cn/1000-9825/7479.htm

Formal Verification and Improvement of XCMP Protocol: Improving Security of Cross-chain
Interaction
1,3
2
1
1
1
LYU Yong-Yang , FENG Rui-Tao , WANG Zi-Mo , LIU Jun-Chao , WU Han-Wei , LI Xiao-Hong 1
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

* 基金项目: 国家重点研发计划 (2021YFF1201102)
收稿时间: 2024-10-23; 修改时间: 2025-01-26; 采用时间: 2025-05-29; jos 在线出版时间: 2025-12-03
CNKI 网络首发时间: 2025-12-04