Page 183 - 《软件学报》2026年第6期
P. 183
2502 软件学报 2026 年第 37 卷第 6 期
图 14 FishmanTimeout 定理验证结果
6.2 基于 Scyther 工具的形式化验证
为进一步验证 E-XCMP 的安全性和可靠性, 证明其能够抵御重放攻击, 拒绝服务攻击和延迟攻击. 本节基于
Scyther 工具对 E-XCMP 进行形式化建模和模型检测.
Scyther 作为目前流行的自动形式验证工具之一, 被安全与隐私领域的研究人员广泛用来对认证方案的可靠
性和安全性进行分析、证明和验证 [36] . 它的工作原理是在用于设计安全协议的所有密码操作的假设下都是完美
的, 常被用于检测从使用加密操作开发协议的方式中可能发生的问题或攻击.
Scyther 工具与安全协议描述语言 (SPDL) 相结合, 用于定义和验证协议设计的安全性. 它能够根据定义的假
设识别协议中的潜在安全问题. Scyther 提供了 4 种声明方式: 存活性 (Alive)、弱协议性 (Weakagree)、非单调一
致性 (Niagree) 和非单射同步性 (Nisynch), 这些声明与 SPDL 语言结合使用, 为协议安全性分析提供了全面的视
角, 确保了验证过程的全面性和准确性. 基于 Scyther 工具进行形式化验证的流程如图 15 所示.
S_Collator 形 实体声明 安 存活性 验证结果分析
创 式 全
建 S_Validator 建模 化 协议流程 建模 属 弱协议性 检测 检测结果展示
协
角 D_Collator 议 性
色 建 建 非单调一致性
模
D_Validator 模 建模实现 非单射同步性 结果窗口解释
图 15 基于 Scyther 工具进行形式化验证的流程
6.2.1 形式化协议建模
本模型创建了 4 个不同角色: 平行链 S 的收集者 S_Collator, 平行链 S 的验证者 S_Validator, 平行链 D 的收集
者 D_Collator, 平行链 D 的验证者 D_Validator.
(1) 实体声明
1. usertype text;
2. usertype Timestamp;
3. hashfunction H;
其中, hashfunction 为内置哈希函数, usertype 为用户自定义类型.
(2) 建模实现
本文的 E-XCMP 协议关键流程形式化建模源码如后文表 3 所示.
6.2.2 形式化安全属性建模
Scyther 形式化验证工具没有对认证性的直接形式化验证, 需要通过机密性、存活性、弱协议性、非单调一
致性以及非单射同步性等验证其保密性, 表 4 对协议形式化验证中关于安全属性建模进行举例分析.
