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

2482 软件学报 2026 年第 37 卷第 6 期

1.5 Scyther
本文借助 Scyther [35,36] 这种形式化的安全协议分析工具, 来全面评估所提出的方案的安全性. Scyther 工具运
用 Athena 自动检查算法 [37] , 它可以自动验证安全协议的正确性, 检测协议是否满足机密性、完整性、认证性等安
全属性, Scyther 采用攻击者模型来模拟敌手的能力, 通过搜索协议的执行轨迹来发现潜在的攻击, 该工具支持多
种协议模型, 包括认证协议、密钥交换协议和组成员协议等, 它使用一种通用的协议表示语言, 可以处理各种加密
原语和协议构造, Scyther 输出的结果包括协议是否安全、发现的攻击轨迹以及安全隐患, 为协议设计者和分析者
提供了一种有效的自动化验证方法, 有助于提高安全协议的可靠性和鲁棒性.
2 协议概况

本节将全面概述 XCMP 协议的系统模型, 并详细描述其工作流程.
2.1 系统模型

在构建系统模型时, 各实体的功能至关重要, 以确保跨链通信的有效性和安全性. 本节根据 XCMP 协议的原
理和要求, 总结出协议模型, 模型如图 2 所示, 并由以下实体构成.

平行链S 平行链D
(1) 触发请求
智能合约 用户 钓鱼者 智能合约

(3) 记录元数据 (7-2) 区块添加 (7-1)
中继链 (6) 区
打 块
包 验
Collator S Collator D 区 证
块
(2) (4-1) (5-2) 消息验证
区 发
块 送 (5-1)
消
构 请 息
建 求 验
Validator S Validator D
证
(4-2) 消息接收
出口队列 入口队列
图 2 XCMP 协议模型

(1) 用户 (User): 发起和接收跨链消息. 他们通过在平行链上触发操作, 如智能合约调用或资产转移, 生成跨链
数据. 这些数据经过平行链的收集者 (Collator) 处理, 并通过中继链传递到目标平行链, 实现跨链数据交互和操作
的完成.
(2) 收集者 (Collator): 生成平行链区块并处理跨链消息. 他们将待发送的跨链消息收集和打包至区块中, 再提
交给验证者. 同时, 收集者会将跨链消息的元数据记录在中继链上, 以便验证者根据中继链记录的元数据进行进一
步验证和确认.
(3) 验证者 (Validator): 负责确保跨链消息的有效性和顺序. 他们通过中继链提供的元数据来验证消息的真实
性, 并确保消息在发送链上已被最终确认. 经过验证的跨链消息会被纳入中继链中, 从而维护系统的数据一致性和
安全性.
(4) 钓鱼者 (Fisherman): 负责监控和验证跨链消息的正确性. 他们通过独立的机制检测平行链或验证者在处理
消息时是否有不正当行为或错误. 钓鱼者提供有关不符合协议的消息或区块的证据, 从而保障网络的安全性和一
致性, 防止恶意操作或错误传播.