摘要
目前安全协议分析的偏序归约算法较为复杂、不易实现,限制了其适用范围,且以动作为基础,粒度较小,对减少状态空间的作用有限。针对该问题提出了一种束动作偏序约简算法,将同一会话中的动作序列看做一个束动作,根据攻击者截获的消息与攻击者知识集间的关系,判断迹等价的束动作迁移所到达的后继状态是否为冗余节点,以约简状态空间。该算法思想简单、易于实现;实例表明它有效地约简了安全协议的状态空间。
At present,the partial-order reduction algorithms used for the verification of security protocols are complicated,and uneasy to carry out,resulting in a limited scope of applicability.Furthermore it permutes based on actions,leading to a limited effect of reduction.To solve the above problems,this paper considered the action sequences in the same session as a stuttering action,and proposed a stuttering action reduction algorithm on the base of partial-order reduction.It judged whether the successors of stutter-equivalent stuttering transitions were redundant based on the relation between messages achieved by the intruder and the intruder knowledges,in order to reduce the state space.This algorithm has a clear structure and easy to implement.Experiment clearly implies that the adopted reduction method is effective.
出处
《计算机应用研究》
CSCD
北大核心
2011年第9期3488-3491,共4页
Application Research of Computers
基金
国家"863"计划资助项目(2007AA01Z471)
关键词
安全协议
状态空间约简
偏序归约
束动作
迹等价迁移
security protocol
state space reduction
partial-order reduction
stuttering action
stutter-equivalent transitions