Based On Strand Space Model To Verify The Password Security Agreement,

With the popularization of network and flourishing of Internet applications, security protocols are becoming more and more important, furthermore, ensuring the security of cryptographic protocols has become an important research task. Scientists have been making great efforts to take the challenge for past 20 years, which in a sense shows the difficulty of security protocols analysis. Among all existing theories and methods, formal method is an outstanding one with promising developing prospect recognized by experts at large. This paper makes a summary of these methods in the second chapter.Having fully absorbed the former researching results, F' abrega, Herzog and Guttman brought forward a kind of formal method named STRAND SPACE, which is a practical, intuitive and strict one for security protocols analysis. The model uses a kind of order graph between its nodes existing casual relationship to represent protocol executions. D.Song has made an extension to SSM and has developed an automatic verification tool, ATHENA.This paper does a further study on the SSM and makes an extension to the model in theorem and algorithm. About theorem, the paper introduces the syntax of ideal, also the first time uses concept of honest ideal to define secrecy goal of protocol and utilizes honest ideal logic to specify secrecy property. At the same time, this paper corrects one not so perfect lemma proving in a literature written by F' abrega, Herzog and Guttman. About algorithm, the paper addes a new state pruning rule and makes strict proving. Additionally, the paper revises the model-checking algorithm so that it can find all available count-examples under the searching depth limitiation. We implemented the model-checking algorithm with Java and developed a new automatic verification tool named AVSP. We have done some experiments and the results showed that the paper's extension to the model is correct and effective. With AVSP, we found a new attack on the Woo-Lam4 authentic protocol, which hadn't been released by existing papers.