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

吕永阳 等: XCMP 协议的形式化验证与改进: 提升跨链交互安全性 2501

(1) 目标 3: 完整接收消息
CompleteBlockReception 定理在 Z/EVES 中的验证结果如图 12 所示. 定理证明了当平行链 D 的区块标识 Xi?
在钓鱼者 fishmanPMN 中存在但与 DBlockPMN 不匹配时 ( DBlockPMN Xi? , fishmanPMN Xi?), 则 Xi?必未被标记
为已验证的区块. 换句话说, 如果钓鱼者记录的承诺值与平行链 D 中记录的承诺值不一致, 则该区块标识 Xi?没有
经过验证, 这确保了只有那些承诺值匹配的区块标识才会被标记为已验证, 从而保持了消息接收的完整性和准确
性. 因此提出的 E-XCMP 协议通过其加强的消息验证机制, 能够有效防止重放攻击, 来进一步保障跨链操作的安
全性.

图 12 CompleteBlockReception 定理验证结果

(2) 目标 7: 公平消息接收
FairMessageReception 定理在 Z/EVES 中的验证结果如图 13 所示. 定理确保了在平行链 D 接收到消息 Mi 时,
消息的接收是公平的. 如果消息的目的地为 D ( Mi.Add=D), 且该消息为目前等待时间最长的消息 ( maxwaittime Mi = 1),
且发送链和接收链之间的通道已经打开 ( mkChannel(S,D) ∈ openChannels), 并且消息到达时间与记录时间的差值
不超过规定的延迟 ( arrivetime?−T 0 Mi.X ⩽ ddl), 则消息 Mi 会被正确地添加到平行链 D 的入口队列中. 这保证了
消息的及时处理和公平接收, 即在规定的时间内, 所有符合条件的消息都将被平等地接收和处理. 因此, E-XCMP
协议通过其设计有效抵御拒绝服务攻击, 维护系统的整体稳定性和公正性.

图 13 FairMessageReception 定理验证结果

(3) 目标 10: 消息持久化
FishmanTimeout 定理在 Z/EVES 中的验证结果如图 14 所示. 定理处理了消息超时的情况. 如果消息 Mi 的目
的地为 D ( Mi.Add = D), 该消息为目前等待时间最长的消息 ( maxwaittime Mi = 1), 并且发送链和接收链之间的
通道已经打开 ( mkChannel(S,D) ∈ openChannels), 同时消息的到达时间与记录时间的差值超过了规定的延迟
( arrivetime?−T 0 Mi.X > ddl), 则该消息 Mi.X 将被删除 (DeleteMessage Mi.X=1), 并且会扣除过错方的 DOT 代币
( deductDot(S,D) = 1). 这确保了超时消息被正确删除, 并对发送链和接收链实施了惩罚措施, 从而维持了系统的消
息持久性和及时性. 因此 E-XCMP 协议通过此设计有效防止延迟攻击, 确保消息在规定时间内被正确处理, 提升
系统的整体可靠性.