形式化分析

安全协议分析的主流方法包括逻辑分析方法、定理证明方法、形式化分析方法等. 逻辑分析方法简单
直观, 但是其分析的结果很大程度上依赖逻辑初始假设, 极大增加了协议分析结果的不准确性. 随着现实
敌手不断增强, 逻辑分析方法所支持的安全模型逐渐不适应当前的协议分析. 定理证明方法分析结果虽然
相对准确, 但是使用普适性不强, 对于一般用户, 该方法不易掌握. 形式化分析工具相对逻辑分析法和定
理证明法有着其独特的优势. 首先, 形式化工具代替了人工分析, 减少了人在分析过程中的工作量, 还能
较少人为失误造成的分析不准确; 其次, 形式化工具对协议可能出现的状态进行遍历搜索, 可以发现人工
分析中难以发现的攻击, 经典的例子就是 Needham-Schroeder 协议[1]在提出之后的 17 年里被认为是安全的,
Lowe[2]通过形式化分析工具 FDR 发现了该协议的中间人攻击; 最后, 形式化分析工具一般都有着基于按
钮或网页的用户界面, 用户仅需将协议以及安全属性的形式化描述作为工具的输入, 工具通过对状态空间
的搜索输出分析结果. 综上所述, 协议形式化分析工具在协议分析过程中有着突出的优势, 使得其在协议
的分析与设计过程中发挥重要的作用.
形式化工具的比较研究工作有着重要的意义. 在工具使用方面, 通过对形式化工具各个使用角度进行
对比研究, 掌握不同工具在攻击搜索、运行效率、所支持的安全模型以及形式化描述语言等方面的优劣, 可
以让协议分析者在众多工具中根据目标协议的特点挑选合适的工具, 使得安全模型更加贴合实际, 分析结
果更加准确, 分析过程更加高效. 在工具开发方面, 通过对形式化工具底层算法的比较研究, 可以将工具
性能与算法设计建立联系, 在工具开发过程中, 针对用户需求, 优化底层算法, 开发更加贴合实际应用、 更
加高效的协议分析工具. 因此, 开展全面的对比研究具有较高的理论价值和现实意义.