计算可靠的安全协议形式化分析系统研究

本项目继续进行安全协议的形式化方法和系统的研究。在我们提出的基于ASM的语义模型的基础上，进行Game 演化理论的研究。构建该模型中的概率机制，以适应基于计算模型的安全协议的验证。着力突破基于Deliv-Yao模型验证思想，结合模式复合思想，将可证明安全需要的计算复杂性的思想融入我们的模型。发展能应用于实用协议的、可分析具有泛复合性安全协议的形式化分析模型和方法。.项目的目标是：从理论上，建立一种在安全上计算可靠的、形式推演和自动化方面容易操作的、可以应用于实用协议的设计和分析模型。在应用上，设计和分析密码协议的方案，开发协议分析的系统原型。以期发展成为一个实用的安全协议验证模型。 这种模型应该具有较好的复合性分析能力, 是建立在严格可靠可证安全的基础之上, 并且能够自动化或者部分自动化操作, 对于具有漏洞的协议,能够找出漏洞发生的原因,对于协议设计具有较好的指导作用。