该文通过对基于Strand空间模型的安全协议分析方法的研究,提出了用于提高安全协议分析效率的改进的状态空间简化技术.在协议分析过程中,将一般的状态空间简化技术与剪枝定理相结合,不但删除了协议运行的冗余状态,而且删除了协议运行的不可达状态,从而有效地简化了状态空间,大大减少了协议分析的工作量.也就是说,在协议分析过程中,令入侵者总是截获诚实主体发送的消息,并以该消息丰富其知识集合,以便增强其攻击能力;同时,入侵者总是等待诚实主体没有消息发送的时候才重发或伪造消息给协议主体,从而使入侵者每次发送消息前,其知识集合都尽可能完备,以便形成最有效的攻击.以上两种简化技术的应用删除了协议运行的大量冗余状态,并且不会遗漏导致攻击的状态.为了删除协议运行的不可达状态,在协议分析时,可根据协议特点,设计适用于该协议的剪枝定理.对于协议分析中的每个状态,首先以剪枝定理判断该状态的可达性,再确定是否需要对该状态进行进一步扩展.剪枝定理的应用删除了协议运行的不可达状态,进一步简化了状态空间.在Strand空间模型的基础上,通过在安全协议分析算法的设计中选择合理的状态结构记录协议的运行情况,使该改进的状态空间简化技术易于实现.即通过使入侵者知识集合尽量完备,并且随着其知识的增加,删除其中的冗余信息,有利于入侵者生成攻击时所需要的消息;通过优先绑定发送消息的节点,并使入侵者总是截获诚实主体发送的消息,有效删除了协议分析中的冗余状态,并将诚实主体发送的消息用于丰富入侵者知识集合,从而增强了入侵者的能力;通过在状态转换前检查状态的可达性,删除了协议分析中的不可达状态以及以这些状态为根的状态转换子树.作为利用该技术简化安全协议分析的实例,在对Needhan-Schroeder-Lowe协议的分析过程中,以认证定理作为剪枝定理,将其与一般的简化技术相结合,简化了该协议的分析过程.并且根据该设计思想,通过VB下的程序设计,实现了对Needhan-Schroeder协议的认证性质分析.总之,在Strand空间模型的基础上,在协议的认证性质分析过程中,通过将状态空间简化技术与剪枝定理相结合,减少了协议分析的工作量,提高了协议分析的效率,达到了预期的设计目标.