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

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

待的时间 Ti 并写入平行链 S 的区块头 (区块头包含平行链的状态变化和交易信息). 每当从出口队列发送出区块
Xi 内的一条消息后, Validator S 便记录其 IDi、PMi 等信息, Collator S 则将 PMi 按照如下的公式进行合并, 待发送
的消息到达总数 N 时形成总承诺 PMN. Collator S 将总承诺 PMN 发送给钓鱼者 C, 等待被验证.

N ∑
PMN = PMi (2)
i=1
其中, Pedersen 承诺机制的安全性属性可通过密码学中的归约证明方法证明, 即将攻击者破解 Pedersen 承诺的能
力归约到解决离散对数问题的能力. 如果存在一个能够有效破解 Pedersen 承诺的攻击者, 那么同样可以构造出一
个解决离散对数问题的算法, 这与离散对数问题的困难性假设相矛盾. 因此, Pedersen 承诺机制是安全的.
(3) 消息转移发送
平行链 D 的 Collator D 通过轮询方式 (轮询根据消息发送链的出口队列等待时间的长短, 由长到短进行响应)
选择到一条从平行链 S 发来的跨链消息 Mi. 平行链 D 轮询时, 中继链根据对与自己相连的平行链的区块头的记
录, 协调各平行链之间的消息传递, 令平行链 D 对目前等待时间 ti 最长的平行链 (假设为平行链 S) 做出响应, 本
文使用一种智能合约保证接收平行链在选择发送平行链响应时是否遵循轮询作为检测机制, 智能合约伪代码如算
法 1 所示. 跨链消息借由二者之间的单向通道, 开始进行跨链消息传递.
(4) 消息转移接收
当跨链消息 Mi 被平行链 D 收到后, Validator D 验证 IDi、Xi、Ti、N 等信息, 并根据时间戳检验该消息是否在
有效期 (24 h) 内, 若在有效期内, 则检验是否可用, 若可用将其放入自己的入口队列中, 以待被打包进区块. 若已经
超时或消息不可用, 则丢弃 Mi, 同时将该情况向钓鱼者 C 报告, C 进行判决, 没收失败方的部分 DOT 代币.
(5) 承诺验证
待入口队列中待被打包的消息 Mi 到达总数 N 时. Collator D 将所有消息的承诺 PMi 按照公式 (2) 形成 PMN',
并发送给 Validator D , Validator D 将其转发给钓鱼者 C 进行验证, 钓鱼者 C 收到消息后则比较 PMN 和 PMN'是否相
等. 若不相等则丢弃与跨链消息 Mi 块标识相同的所有消息, 同时钓鱼者 C 调取平行链 S 和平行链 D 中记录的 IDi、
PMi 等信息进行比对验证, 并没收失败方的部分 DOT 代币.
(6) 打包消息成区块
如果 PMN 和 PMN'相等, 则 Collator D 将队列中的跨链 N 个消息 Mi 打包进区块, 同时消息 Mi 会执行平行链
D 上相应的智能合约, 完成资产转移操作.
(7) 添加区块至区块链
Collator D 将新生成的区块 (包含消息 Mi) 提交给 Validator D 进行验证, 当确认无误后该区块将添加到中继链
的尾部, 跨链操作得到确认.
6 协议分析

本节同时采用 Z/EVES 和 Scyther 工具来验证 E-XCMP 协议的功能正确性和信息安全性. Z 语言用于验证跨
链协议的功能正确性, 同时关注协议的规范性和一致性保证. 针对 E-XCMP 协议的扩展功能 (承诺机制、监督机
制、轮询机制), Scyther 补充了其在具体实现阶段的信息安全性验证, 它能够通过模拟实际运行中的协议交互, 检
查是否存在如身份冒充、信息泄露等实际的安全问题. 通过结合两者, 可以最大程度地保证 E-XCMP 协议的正确
性、完整性和安全性, 从理论到实际执行的各个层面都得到充分的验证.
6.1 采用 Z/EVES 验证 E-XCMP 协议
本节使用 Z/EVES 工具用于对 E-XCMP 协议进行严格验证, 以判断其是否满足预设的安全目标. 首先, 基于
Z 语言对协议进行了形式化建模, 将协议的状态和操作以数学方式精确描述. 随后利用 Z/EVES 工具, 构建了 3 个
定理, 并通过自动化的定理证明功能, 严格验证了 E-XCMP 协议对 3 条安全目标的符合性, 确保每条安全目标在
形式化模型中都得到了充分证明.