形式化工具Scyther优化与实例分析

摘要：

当前安全协议形式化分析工具发展迅速,针对不同的安全协议、不同的安全模型挑选合适的工具进行分析,不仅可以提高分析结果的可信度和准确性,还可以大大提高协议分析的效率.为此,对当前主流的9种形式化分析工具的性能进行梳理,从使用界面、分析效率、安全模型等综合角度来看,Scyther工具有着较大的优势;为方便国内协议分析者使用和研究,剖析Scyther的底层算法,将其交互界面进行汉化,并增添了时间计算功能,对分析时间进行计算和输出;最后以网络安全协议TLS为例,利用优化后的Scyther工具分别在Delov-Yao模型和强安全模型下对其进行形式化分析.对研究工作者准确、有效地选择和使用形式化分析工具有着理论意义和实践价值.

关键词：形式化分析工具、Scyther工具、比较研究、安全模型、TLS协议

所属期刊栏目：2

分类号：TP309.7(计算技术、计算机技术)

资助基金：密码科学技术国家重点实验室开放课题MMKFKT2015014;洛阳外国语学院科研基金项目2015XYQ004

在线出版日期：2016-10-31（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：272-279