Research On The Protocol Analysis Based On Strand Space Model

With the popularization of network and flourishing of Internet applications, security protocols are becoming more and more important, so that 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 anslysis. Among all existing theories and methods, formal method is a good one with promising developing prospect recognized by experts at large.FabregaN Herzog and Guttman proposed a kind of formal methods named STRAND SPACE MODEL,which uses a kind of order graph between its nodes existing casual relationship to represent protocol executions. Having fully absorbed the former researching results,strand space model become a practical,intuitive and strict method for security protocols analysis. Strand space model takes advantages as following: (l)State explosion can be reduced because of the simplicity during analyzing. (2) Some problem brought on by nonstandard formal language can be reduced because of standardization of the formal language. That problem often occour in the logic method based on knowledge and belief, such as BAN logic and Kailar logic.Based on the strand space model theory we first study further on the semantics of model. Through analyzing for accountability logic,a strand space semantic description for accountability logic is proposed to resolve the problem that Kailar logic brings about some sementic confusion.This semantic description can provide Karlar logic with a clearer computation model. Second,we discuss further on the authentication test method of strand space model,and point out the flaw in the method, consequently give the improvement scheme to the method.The authentication test method presented by Guttman is proved to be not pefect with applying in NS protocol. The method can not analyze type-flaw attack. Focusing on the type-flaw attack, we provide an improved scheme for authentication test method, which proved to be valid through analyzing for NS protocol. At last,we make use of software maude to simulate the procedure of authentication analyse. Maude is developed for formal programming based on rewriting logic. In this paper, we make use of maude as a programming tool to automate the strand space model and the relating theory.