本文基于密码协议的运行特点,采用经典规划理论,分别对密码协议形式化模型、密码协议攻击规划机制和规划算法进行了系统研究。论文的工作主要包括以下几点:(1)相关研究现状分析:踪述了当前密码协议形式化分析方法、智能规划理论及其在密码协议形式化分析领域的研究成果,分析目前的研究热点和存在的不足。(2)密码协议攻击规划理论研究:利用智能规划理论,结合密码协议在实际网络环境中的运行特点,提出了一种密码协议攻击规划理论,建立了相应的密码协议攻击规划问题,给出了描述该问题的基本假设、一阶语法及相关运算语义,基于Dolev-Yao攻击者模型,提出了攻击者动作应用优化策略,构建了密码协议攻击规划系统。(3)密码协议代数语义研究:对密码协议代数语义进行了深入研究和分析,探讨了密码协议中消息项结构的代数性质,提出了密码协议原语操作的代数自由性假设,从代数学的角度讨论了密码协议攻击者的计算能力和攻击行为,通过迁移函数刻画了密码协议中主体的行为和操作,进而,采用函数序列给出了密码协议运行过程的形式化语义,并且利用代数学中的等价变换形式地证明了密码协议攻击规划理论的合理性。(4)密码协议攻击规划算法研究:在分析了密码协议攻击规划问题模型特点的基础上,提出了基于SAT的密码协议攻击规划机制,设计了密码协议攻击规划算法,重点对基于互斥排除和节点有效性判断优化策略的逐层迭代规划图构造算法、基于过载分离动作表示和扩展编码公理的SAT问题编码算法和基于学习机制和空间复杂度优化措施的SAT问题求解算法进行了关键技术研究和算法详细设计。(5)密码协议攻击规划系统设计与开发:基于密码协议攻击规划理论和算法,设计并实现了一个密码协议攻击规划原型系统,并对其性能进行了测试比较。