密码可靠的安全协议形式化分析研究

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