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

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

timestamp?: Z
size?: Z
metadata?: Metadata
M: Message
states, states': Parachain↔ParachainState
ΔRelaychainState

M.S=S?
M.D=D?
M.CCdata=ccdata?
M.timestamp=timestamp?
M.size=size?
M.metadata=metadata?
states'
=states
⊕{(S?
7→ mkParachainState((states S?).ingressQueue,
((states S?).egressQueue ∧ 〈M〉)))}
∧ 〈M.metadata&
metadatas'=metadatas
(3) 消息接收模式 (ReceiveMessage)
在消息接收模式中, 平行链 D 的收集者节点在向所有其他收集节点发送请求时, 发现平行链 S 的出口队列中
有以平行链 D 为目的地的跨链消息, 并且消息 M 在 D 的出口队列的队头. 收集者随后检查平行链 D 与平行链 S
之间是否已经建立了单向通道. 如果通道存在, 将消息 M 添加到平行链 D 的入口队列. 具体见代码 8.

代码 8. ReceiveMessage.
states, states': Parachain↔ParachainState
S, D: Parachain
M?: Message
M?.D=D
M?=head(states S).egressQueue
mkChannel(S, D) ∈ openChannels
⇒states'
=states
⊕{(D
7→ mkParachainState(((states D).ingressQueue ∧ 〈M?〉),
(states D).egressQueue))}

(4) 消息验证模式 (ValidateMessage)
在消息验证模式中 (见代码 9), 平行链 D 的验证者接收到跨链消息进入入口队列的消息后, 需在中继链的元
数据序列 metadatas 中查找是否存在满足以下条件的元数据.
● 元数据中的发送者与跨链消息 M 的发送链 S 一致.
● 元数据中的接收者与跨链消息 M 的接收链 D 一致.