安全协议验证中DY模型的构建框架

A framework for constructing DY model in security protocol verification

攻击者建模是安全协议验证工作的一个重要部分,直接影响到验证的效率与质量,但目前却还没有一个可遵循的形式化框架,影响了建模工作的准确性与客观性。针对这一问题,通过对在安全协议验证中具有广泛影响的DY模型进行形式化,建立了一个DY模型的构建框架,刻画了攻击者的构成要素、行为规则以及行为模式,从而保证了攻击者具有合理的行为与能力,并能在攻击过程中获取新的知识,不断增强攻击能力。最后,将该工作运用到Otway-Rees协议的验证中,找出了该协议中所存在的漏洞,从而证明了该构建框架的有效性。

The modelling of intruders is an important part of security protocol verification,which di-rectly affects the efficiency and correctness of verification.There is no available formal framework of introders modelling,which is a disadvantage for modelling work.A framework for formalizing/con-structing DY model that has extensive influence on security protocol verification was proposed.The framework can depict the components,behaviours and behaviour model of the intruders,which en-sures that the intruder has reasonable behaviours and ability and can acquire new knowledges in the attacking process to enhance contantly the attacking ability.The effectiveness of the framework was confirmed in the verification of Otway-Rees protocol in which a fault in the protocol was found.