论文摘要
近年来,密码协议自动化验证技术越来越多地受到了人们的关注,成为密码协议研究领域的热点之一。本文充分考虑密码协议运行的特点和规律,基于经典规划理论,分别对密码协议形式化模型及其验证机制和验证算法进行了深入研究。论文的工作主要包括以下几点:(1)相关研究现状分析:评述当前密码协议形式化分析方法、自动化验证工具和智能规划等领域的研究成果,分析这些领域中的研究热点和不足。(2)密码协议形式模型研究:将规划理论引入密码协议形式化分析领域,结合密码协议在实际网络环境中的运行特点和规律,提出了密码协议攻击规划理论,建立了一种对密码协议安全性进行验证的形式化模型,给出了模型的基本假设、一阶语法、形式定义及相关运算语义,并结合NS公钥协议详细阐述了模型建立的具体过程。(3)Dolev-Yao模型改进策略研究:分析了经典Dolev-Yao模型的不足之处,基于基本消息元素策略对其进行了改进,并通过增强应用语义来保证改进模型的可行性,从而避免了“状态空间爆炸”问题的发生,提高了密码协议攻击规划问题模型的完备性。(4)密码协议安全性验证机制研究:在分析了密码协议攻击规划问题模型特点的基础上,提出了基于SAT方法的密码协议攻击规划问题模型自动化验证机制,并且针对验证机制中从规划问题到SAT问题的编码,提出了一系列基本准则,形式地证明了遵循这些基本准则的编码方法是可靠且完备的。(5)密码协议安全性验证算法研究:基于上述验证机制,研究并设计了密码协议攻击规划问题模型自动化验证算法,并且对算法中规划图扩展阶段、SAT编码阶段和SAT求解阶段的子算法做了相应的设计,形式地证明了SAT编码算法的正确性。其中,在SAT求解阶段,引入子句权重和学习机制对WalkSAT算法进行了改进,并将改进后的算法应用于SAT问题的求解。(6)密码协议自动化验证原型系统设计与开发:基于密码协议攻击规划问题模型及其自动化验证机制和算法,设计并实现了密码协议自动化验证原型系统ACPV,并对其性能进行了测试。