Abstract: It is concluded that the inject attack is the necessary method for D-Y attacker to get its aim. Based on the analysis of the inject attack sequence, an inject attack searching algorithm is presented, and a new security protocol verification approach, which based on the algorithm, is also presented. The NS protocol is verified by the approach in the paper, and the experiment shows that the approach can realize automatic security protocol verification, reduce the complexity of security protocol verification, and give attack ways according to the protocol flaws.

Key words: security protocol, verification, inject attack sequence

摘要： 通过对D-Y攻击者模型研究, 可知注入攻击是攻击者实现其攻击目标的必要手段。对注入攻击序列的性质进行分析, 提出了一种在安全协议会话状态空间中搜索注入攻击序列的算法, 基于该算法可实现一种新的安全协议验证方法。利用该方法实现了NS公钥协议的验证。实验表明该方法可以实现对安全协议的自动化验证, 降低了验证的复杂度, 并能给出安全协议漏洞的具体攻击方法。

关键词: 安全协议, 验证分析, 注入攻击序列