基于Spin的安全攻击仿真设计(4)
2.3.1 Casper/FDR工具
CSP[11]（Communication Sequential Process）是由牛津大学的C.A.R.Hoare提出的用于并行系统设计和分析的代数理论。Formal Systems LTd.公司基于CSP研究出了通用模型检测工具FDR[12]（Failure Divergence Refinement）。由于直接使用CSP来描述协议非常困难，于是开发出了Casper[13]软件，Casper软件可以极大的简化了FDR工具的操作复杂度并降低了使用难度。
2.3.2 AVISPA工具
AVISPA[14]（Automated Validation of Internet Security Protocols and Application）项目旨在开发一个工业级技术，来分析大型安全协议。AVISPA工具采用HLPSL（High Level Protocol Specification Language）语言建立安全协议的分析模型。已从33个工业级的安全协议中检测出215个安全问题。分析终端共包含4种后端分析工具，包括OFMC、CL-AtSc、SATMC和TA4SP。如果协议不安全，该工具会给出攻击路径，可以以此找出协议的安全漏洞。
2.4 本章小结
本章介绍了安全协议的基本概念，安全协议的常见攻击方法，安全协议的设计规范以及安全协议的分析方法等相关背景知识。并对安全协议形式化分析所用到的模型检测工具进行了简要介绍。