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

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

③ 将消息 Mi 的等待时间 ti?记录到 waittime 中.
④ 如果当前区块标识 Xi?对应的消息总数 SBlockcont Xi?已经达到预定数量 N?, 则不更新 SBlockPMN 和
SBlockcont, 直接将当前的 SBlockPMN 记录到 fishmanPMN 中. 否则更新 SBlockPMN, 将当前 Xi?的承诺值 PMi 加
入其中, 并更新 SBlockcont, 增加对应的计数, fishmanPMN 保持不变.

① 用户将跨链数据

Data发送给收集者
用户 ⑤ 等待下一个 F ⑤ 根据公式
消息
N
PMN=∑ i=1 PM
② 生成Mi, 计算PMi, 得到发送方总承诺
记录IDi和PMi, 并将 SBlockPMN发送
Mi压入出口队列 发送方消息计数器 给钓鱼者
SBlockcont达到该区块 T
Collator S PMN
的消息总数N
Mi={Addi, Ti, Xi, Data}
Mi PMi=Data*G+seed*H 钓鱼者
IDi
PMi
平行链S Validator S
④ 将等待时间
写入区块头的
入口队列 waittime中
③ 记录Mi的
出口队列 等待时间ti 区块头 中继链
图 8 消息收集流程图

代码 17. CollectingMessage.
Addi?: Parachain
Ti?, N?, seedi, PMi, ti?: N
Xi?, Data?, IDi: string
Mi: Message
S, S': Parachain
states, state': Parachain↔ParachainState
MessageID, MessageID': Message→string
MessagePM, MessagePM': Messsage→ N
N
SBlockPMN, SBlockPMN': string→
SBlockcont, SBlockcont': string→ N
ΔFishman
ΔRelaychainState
PMi=mkPromise(Data?, seedi)
Mi=mkMessage(Addi?, Ti?, N?, Xi?, Data?)
MessageID'=MessageID⊕{(Mi→IDi)}
MessagePM'=MessagePM⊕{(Mi→PMI)}
states'
=states
⊕{(S
7→ mkParachainState((states S).ingressQueue,

((states S).egressQueue ∧ 〈M〉)))}
waittime Mi=ti?