Stuttering partial-order reduction algorithm in verification of security protocols
安全协议状态空间的束动作偏序约简算法*

目前安全协议分析的偏序归约算法较为复杂、不易实现，限制了其适用范围，且以动作为基础，粒度较小，对减少状态空间的作用有限。针对该问题提出了一种束动作偏序约简算法，将同一会话中的动作序列看做一个束动作，根据攻击者截获的消息与攻击者知识集间的关系，判断迹等价的束动作迁移所到达的后继状态是否为冗余节点，以约简状态空间。该算法思想简单、易于实现；实例表明它有效地约简了安全协议的状态空间。