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

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

′
T 0 , T : string→ N
0
arrivetime?: N
Mi.Add=D
maxwaittime Mi=1
mkChannel(S, D) ∈ openChannels

⇒ (if Mi.X < dom DBlockcont
then T = T 0 ⊕{(Mi.X 7→ arrivetime?)}
′
0
else T = T 0 )
′
0
T Mi.X≤ddl
′
if arrivetime?– 0
then states'
=states
⊕{(D
7→ mkParachainState (((states D).ingressQueue ∧ 〈Mi〉),
(states D).egressQueue))}
∧(if DBlockcont Mi.X=Mi.N

then (DBlockPMN'=DBlockPMN ∧ DBlockcont'=DBlockcont)
else (DBlockPMN'
= DBlockPMN⊕{(Mi.X 7→ DBlockPMN Mi.X+MessagePM Mi)}
∧ DBlockcont'

=DBlockcont⊕{(Mi.X 7→ DBlockcont Mi.X+1)}))
else DeleteMessage Mi.X=1 ∧ deductDot(S, D)=1

(c) 承诺验证模式 (PromiseValidate)
在 PromiseValidate 模式中, 承诺验证的流程如图 10 所示, 详细代码如代码 19 所示. 进行跨链消息承诺的验
证时, 主要步骤如下.

③ 丢弃与Miॶѓ
PMN ്相同的所有消
F 息, 并扣除失败方
的部分DOT代币
② 将DBlockPMN与钓鱼者C记录
的fishmanPMN进行对比验证
钓鱼者 DBlockPMN=fishmanPMN
① 发送DBlockPMN到
钓鱼者C ③ Collator D 将队列的N
个消息Mi打包进区块,
Validator D 平行链D Collator D T 同时消息Mi会执行平
行链D上相应的智能合
约, 完成资产转移操作
图 10 承诺验证流程图

① 首先检查平行链 D 的 DBlockcont 中标识为 Xi?的区块的消息数量是否等于预期总数 N?. 确保接收到的消
息数量与预期一致.
② 确认块标识 Xi?存在于 fishmanPMN 中, 并且 DBlockPMN 中对应 Xi?的承诺值与 fishmanPMN 中存储的值
相匹配.
③ 如果上述验证通过, 则根据块标识 Xi?生成新块 newBlock, 并确认该块通过 AssetTransfer 函数验证为有效