一种基于攻击序列求解的安全协议验证新算法

基于完美加密机制前提及D-Y攻击者模型,指出注入攻击是协议攻击者实现攻击目标的必要手段.分析了注入攻击及其形成的攻击序列的性质,并基于此提出了搜索攻击序列的算法,基于该算法实现了对安全协议的验证.提出和证明了该方法对于规则安全协议的搜索是可终止的,并通过实验实现了NS公钥协议的验证.实验结果表明,与OFMC等同类安全协议验证工具相比,该算法不仅能实现安全协议验证自动化,而且由于规则安全协议验证的可终止性,使得本算法更具实用性.

New Security Protocol Verification Approach Based on Attack Sequence Solving

With the premises of the prefect encryption mechanism and the ICY attacker model, it concluded that the inject attack is the necessarily method for attackers to realize their aims. In this paper, the attributes of inject attack and attack sequences which come from inject attacks were analyzed. Based on those conclusions,it presented an algorithm to determine whether there is an attack sequence in a security protocol. And an new security protocol automatic verification approach was brought up based on this algorithm It was also proved that the algorithm can be terminated in the verificanon process for a regular security protocol. In the paper, the NSPK was verified by the algorithm The experimental results show that compared with other security protocol verification tools, as OFMC, the algorithm can not only realize security protocol automatic verification, but also more practicability for it can be terminated in regular protocol verification process.