本文概要介绍了状态空间约简技术的研究现状,并针对安全协议状态空间中存在的冗余结点问题,对偏序归约技术进行了分析与研究,提出了三种状态空间约简算法,实现了对安全协议形式化自动分析系统SPFA (Security Protocol Formal Analyzer)的改进,主要内容包括:首先,针对状态空间中存在某些动作执行序列与实际运行情况不符的问题,在偏序归约技术的基础上,提出了一种诚实会话中的逆序约简算法,通过删除违反协议规范的状态结点,降低安全协议状态空间的规模。实验结果表明该算法消除了诚实会话中存在的逆序现象,减少了SPFA验证安全协议所需的时间。其次,针对符号化状态空间中存在由迹等价迁移引起的冗余后继现象,在偏序归约技术的基础上,提出了一种迹等价迁移的冗余后继约简算法,根据诚实主体所发送的消息与攻击者知识集的关系,删除迹等价迁移的冗余后继状态。理论分析和实验结果表明该算法减少了状态空间中的结点数,降低了分析安全协议所需的时间。再次,针对迹等价迁移的冗余后继约简算法以动作为基础,粒度较小,对减少状态空间的作用有限的问题,引入“束动作”的概念,将同一会话中的动作序列看作一个束动作,提出了一种束动作迁移的偏序约简算法,根据诚实主体所发送的消息与攻击者知识集的关系,删除迹等价束动作迁移的冗余后继状态。理论分析和实验结果表明该算法比冗余后继约简算法更为有效地约简了符号化状态空间中存在的冗余结点,降低了分析安全协议所需的时间。最后,在上述三种算法的基础上,实现了对安全协议形式化自动分析系统SPFA的改进,并对全文的研究工作进行总结,指出了下一步的研究方向。