Strand Space Theory-based Security Protocol Analysis

Security protocol providing security services, to ensure network's security. In recent years, more and more security protocol is used for protecting the Internet transmission of transactions and the access to computer systems. However, verifying the correctness of security protocol is very difficult. Therefore, we must rely on formal methods to analyse the security protocol.Among lots of formal analysis methods, the strand space model is a combination of theorem proving and protocol trace, pushes formal analysis technology of security protocol to a new level. Strand space model is widely respected because of its high efficiency, a rigorous, intuitionistic feature. In the foundation of reaching Strand space theory, it is the first time to analyse the modified version of NSSK protocol from the aspects of both confidentiality and authentication,using "Ideal" and "Honest" of strand space theory. The analysis proved the correctness of the modified NSSK protocol.The correctness of a security protocol mainly includes agreement and secrecy. Although, comparing with other formal analysis methods, Strand space model is more intuitionistic and simple, but in analysing why protocol is incorrect and how to improve it, strand space model is as weak as other formal methods. In view of this problem, this paper proposed the concept of the parameter-agreement-matrix based on Authentication Tests. Comparing with original method,it is more intuitionistic and simple to anaylse security protocols,can reveal the reasons for the failure of protocols and the corresponding improvement ideas aimed at the causes.