Abstract: 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.

Key words: Security protocol verification, Attack sequence solving, Automatic