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

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

表 3 Scyther 建模实现

协议步骤 建模实现
fresh T1: Timestamp;
fresh Data, N: Nonce;
S_Collator生成Mi, PMi, IDi fresh Addi, Ti, Xi, PMi, IDi, Mi: text;
match(PMi, H(Data));
match(Mi, H(Addi, N, Xi, mi));
S_Collator向S_Validator发消息 send_1(S_Collator, S_Validator, {S_Collator, S_Validator, IDi, PMi, T1}pk(S_Validator));
S_Validator接收S_Collator的消息 recv_1(S_Collator, S_Validator, {S_Collator, S_Validator, IDi, PMi, T1}pk(S_Validator));
fresh T2: Timestamp;
S_Validator进行验证操作 var T1: Timestamp;
var ACK1, IDi, PMi: text;
match(ACK1, H(IDi, PMi));
S_Collator向D_Collator发消息 send_2(S_Collator, D_Collator, {S_Collator, D_Collator, PMi, Mi, IDi, T1}pk(D_Collator));
D_Collator接收S_Collator的消息 recv_2(S_Collator, D_Collator, {S_Collator, D_Collator, PMi, Mi, IDi, T1}pk(D_Collator));
fresh T3: Timestamp;
S_Collator打包生成区块 var BLOCK, IDi, Mi, PMi: text;
var T1: Timestamp;
match(BLOCK, H(PMi, Mi, IDi, T1));
D_Collator向D_Validator发送区块 send_3(D_Collator, D_Validator, {D_Collator, D_Validator, BLOCK, T1}pk(D_Validator));
D_Validator接收D_Collator的区块 recv_3(D_Collator, D_Validator, {D_Collator, D_Validator, BLOCK, T1}pk(D_Validator));
fresh T4: Timestamp;
D_Validator进行验证操作 var T1: Timestamp;
var ACK2, BLOCK: text;
match(ACK2, H(BLOCK, T1));

表 4 安全属性建模举例

安全属性 描述定义 建模
机密性 Secret claim(A, Secret, MAC)
存活性 Aliveness claim(A, Alive);
弱协议性 Weak agreement claim(A, Weakness);
非单调一致性 Non-injective agreement claim(A, Niagree);
非单射同步性 Non-injective synchronisation claim(A, Nisynch);

表 4 中, 存活性、弱协议性、非单调一致性以及非单射同步性的认证性强度依次增大. Alive 即存活性认证, 是
一种基本的认证, 确保了预期的通信方 A 是存在的; Weakagree 即弱协议认证, 要求在协议执行期间表示参与方之
间的某些状态或值应保持一致; Niagree 即非单调一致性认证, 用于描述在协议执行期间, 参与方之间的通信或协商
结果不能被否认. Nisynch 即非单射同步性认证, 表示在攻击者获取代理 A 的私钥的情况下, 声明事件 (claim event)
之前的所有发送事件或接收事件 (send/recv) 都能被正确的代理 A 以正确的顺序和内容执行, 此性质保证接收者收
到的信息都满足完整性, 同样用于描述在协议中参与方之间的通信或协商结果不能被否认, 并且保持一致性.
Nisynch 与 Niagree 的定义十分相似, 但不同点在于 Nisynch 增加了对于预期次序的要求, 因此有更强的认证性.
6.2.3 形式化验证结果分析
在 Scyther 工具中, 本文创建 S_Collator、S_Validator、D_Collator 和 D_Validator 这 4 个不同角色, 在其中的
任意二者进行信息传输时, 选取时间戳保证了消息的时效性. 用 SPDL 描述本文的协议, 首先 S_Collator 收到用户
调用智能合约触发的跨链数据 Data 并形成消息 Mi, 同时产生消息标识 IDi 和承诺 PMi, 将 PMi、Mi、IDi 一起发
送给 D_Collator, 并将 IDi、PMi 发送给 S_Validator. S_Validator 收到后将 IDi 和 PMi 形成 ACK1, 对消息进行验
证确认. D_Collator 收到 S_Collator 发送的消息后, 利用 PMi、Mi、IDi 和时间戳打包形成区块 BLOCK, 并发送给
D_Validator. D_Validator 收到后对 BLOCK 进行验证, 确认无误后形成 ACK2. 运行本协议的 SPDL 模型, 并且测