网络信息安全协议的形式化分析和验证研究

项目开展对GNY逻辑系统及其形式化工具SPEARII的研究，提出用于复杂网络信息安全协议的形式化分析和设计的协议进化模型方法，扩展GNY逻辑规则，进而利用协议进化模型和GNY推理逻辑分析典型的复杂网络信息安全协议（SSL协议）的安全性，设计自动证明试验，给出安全性探讨。项目拟设计一个形式化分析、设计和验证集成工具的框架，提出一种高效的基于攻击逻辑协议验证方法，研究在SWI-Prolog编译器上实现攻击逻辑分析模块，以便作为独立模块添加到本项目提出的形式化方法集成工具上，这种验证方法将弥补基于推理逻辑的形式化分析方法在攻击检测方面的空白。因此项目既具有重要的理论意义，又具有很高的应用价值，值得深入研究。