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

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

问题. 在建模实现的过程中, 本文定义平行链、DOT (Polkadot 网络的原生代币)、字符串等基本类型, 并重点设计
出平行链状态模式、中继链状态模式和通道状态模式 3 个基本实体模式和 6 个操作模式, 还原 XCMP 协议的跨
链消息传递与资产转移等功能, 并支持模型扩展和改进. Z/EVES 模型检测的结果显示, 在 10 条安全目标中存在 3
条安全目标未满足要求, 该协议存在亟待解决的安全漏洞.
(3) 基于未满足的安全目标提出 E-XCMP 协议. 通过分析 XCMP 协议存在的问题, 本文扩展 XCMP 各个实体
的功能, 引入承诺机制、监督机制和轮询机制, 提出了 E-XCMP 协议, 该协议的功能实现覆盖以上 10 条安全目标
并且具有良好的安全性和可靠性. 其中, 引入承诺 Pedersen 机制, 用以监控同一区块消息的完备性; 引入轮询机制
并设计轮询检测智能合约, 以保证接收平行链公平地接收各个发件方的消息; 引入了一个高效的监督机制, 即利用
钓鱼者 (Fishermen) 作为消息有效性的智能验证者, 并加入 Pedersen 承诺机制和轮询机制, 使得整个跨链生态系统
更加健壮与可信.
(4) 对 E-XCMP 协议进行形式化建模和安全性分析. 基于所提出的 E-XCMP 协议, 本文利用 Scyther 工具和
Z/EVES 工具对其进行安全性分析以保证其正确性与可靠性. 经 Scyther 工具验证, E-XCMP 协议能解决重放攻击、
拒绝服务攻击、延迟攻击等问题, 满足存活性、弱协议性、非单调一致性和非单射同步性. 形式化建模验证表明,
E-XCMP 协议可解决原协议存在的安全漏洞, 并满足机密性、认证性、完整性和非否认性等安全属性.
本文第 1 节介绍本文用到的一些基础知识, 包括 Polkadot 平台的相关架构知识和 Pedersen 承诺的核心知识,
以及 Z 语言、Z/EVES 工具和 Scyther 工具的基本语法和符号. 第 2 节对 XCMP 协议的系统模型进行概述, 并简述
该协议的工作流. 第 3 节基于 XCMP 协议的参与者和实体提出了安全假设, 定义了协议的安全目标, 并使用一阶
逻辑对 10 个安全目标进行形式化描述. 第 4 节采用 Z 语言对安全目标和协议模式进行形式化建模与安全性分析,
并基于 Z/EVES 的分析结果检验 XCMP 协议对各安全目标的满足情况, 最后对未满足的 3 个安全目标进行深入
分析. 第 5 节主要介绍 E-XCMP 协议的系统模型, 并详细阐述该协议的具体内容. 第 6 节采用 Z/EVES 和 Scyther
工具对 E-XCMP 进行形式化建模和安全性验证, 并分析最终的检测结果, 确保其有效性与可靠性. 第 7 节讨论国
内外的相关工作. 第 8 节总结全文.

1 预备知识

1.1 Polkadot 平台及 XCMP 协议
自 2008 年比特币诞生以来, 区块链技术在许多领域都产生了重大影响. 然而, 不同的独立区块链之间缺乏有
效的沟通, 限制了区块链产业的促进和生态发展. 在此背景下, 跨链技术迅速发展, 成为一个新的研究热点. Polkadot
就是一种允许独立区块链互相交换信息的系统 [14,15] , 目标是实现各个链之间资产与数据的互相流通, 它的创建可
以追溯到 2016 年, 由以太坊共同创始人之一的 Wood [15] 提出, 并由 Web3 基金会推动开发. Polkadot 项目在 2017
年进行了一次成功的 ICO, 并于 2020 年 5 月 26 日正式启动其主网 (relay chain). 在 Polkadot 平台上的跨链满足数
据跨链、资产跨链和互操作性的功能, Polkadot 系统由平行链、中继链和转接桥组成, 中继链为主链, 加入进来的
区块链称为平行链. Polkadot 平台的基本结构如图 1 所示.

中继链 验证人 平行链 收集人

图 1 Polkadot 平台基本结构