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

2478 软件学报 2026 年第 37 卷第 6 期

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

区块链 (blockchain, BC) 是一种分布式账本技术 [1] , 它通过密码学方法 [2] 将各个“区块”相互连接, 形成一个安
全可信的网络. 自 2008 年 10 月 31 日 Nakamoto 发表开创性论文以来 [3] , 这一技术以其独特的去中心化特性和加
密安全性, 迅速吸引了全球的关注. 在区块链技术的快速发展过程中, 以比特币 [3] 和以太坊 [4] 为代表的各种不同的
区块链系统如雨后春笋般涌现, 它们在设计和应用上各具特色, 满足了多样化的业务需求, 截至 2023 年 12 月, 全
球共有区块链企业 10 291 家 [5] . 然而, 由于这些区块链系统针对不同的目的和应用程序采用了不同的技术框架和
设计理念, 它们往往各自独立运作, 形成了一座座“数据孤岛”. 不同区块链之间的数据和资产无法直接互通, 这限
制了区块链技术的整体效能和广泛应用. 例如, 以太坊支持智能合约并使用权益证明 (proof of stake, PoS) 机制来
[7]
达成共识 [6] , 而比特币主要是被设计为基于工作量证明 (proof of work, PoW) 的加密货币. 在异构和隔离的区块
链 [8] 之间缺乏有效的通信方法. 为了打破这些隔阂, 同时为满足区块链技术发展中的关键需求: 扩展性 [9] 和互操作
性 [10] , 实现不同区块链网络间的互联互通, 跨链技术应运而生. 跨链技术的核心在于允许不同的区块链平台进行
通信和数据交换, 甚至实现资产的转移和交易 [11] . 它就像是一座桥梁, 将不同的区块链网络连接起来, 构建了一个
更加广阔和协同的区块链生态系统.
跨链技术作为连接不同区块链世界的桥梁, 实现了数据和信息交换的功能. 它不仅促进了公共区块链之间的
资产的交换, 还推动了多链结构的发展, 为去中心化应用 (DApp) 的互操作性和扩展性提供了新的可能性. 公共区
块链之间的资产交换是跨链技术最初的驱动力之一. 然而, 由于这些区块链的异构性和独立性, 直接的资产转移面
临着技术和安全上的挑战. 多链结构的发展进一步扩展了跨链技术的视野, 为用户提供了更高的灵活性和吞吐量 [12] .
它不仅关注单一的资产交换, 还着眼于构建一个由多个区块链组成的生态系统, 每个链都可以根据其特定的需求
和优势进行优化. 例如, Cosmos 通过其 Hub 和 Zone 的架构, 实现了不同区块链之间的互操作性 [13] . Polkadot 则通
过共享安全性和无需信任的跨链交互, 允许其平行链进行高效的通信和数据交换 [13,14] . 在构建多链框架时, 除了资
产交换之外, 还需要一种更根本且具有普遍性的手段, 以便在不同的区块链之间实现互通. 这种手段被称为跨链通
信协议. Polkadot 网络中的跨链消息传递 (cross-chain message passing, XCMP) 协议作为最流行的跨链通信协议之
一, 使得 Polkadot 生态中的不同区块链 (称为平行链) 之间可以直接交换信息和价值 [14,15] , 目前, Web3 基金会已经
完成了 XCMP 的技术原型设计 [16] , Polkadot 生态中的多个项目 (如 Acala、Moonbeam 等) 已经为 XCMP 的落地
做好了准备 [17] , 具有广泛的应用前景.
与其他跨链通信协议相比, XCMP 协议能够高效、安全地实现跨链通信 [18,19] , 解决了区块链孤岛问题, 使得多
个独立的区块链能够互通并协同工作. 它通过去中心化的结构提升了系统的可靠性, 确保数据和价值能够在不同
的平行链之间流动而不依赖中心化的中介 [18] . 随着 DeFi、NFT 等多种去中心化应用的崛起, 跨链技术的需求日益
增长, XCMP 协议作为 Polkadot 生态的核心协议之一, 将成为支持未来区块链生态繁荣的关键技术之一 [20–22] . 此