Based On Strand Space Model Of Security Protocol Verification Algorithm

With the popularization of network and Internet applications, security issues are becoming more and more important. Only depending on the fine encryption algorithm to guarantee the secutiry of the information is insufficient. In practical applications, we need a credible mechanism for the distribution of the key between independent communication entities, and also for the identity authentication. This makes people come up with various security protocols.Security protocol, also be known as the cipher protocol, which uses the cryptographic methods for network communication. Its goal is to provide security services in the complex and insecure environment. The purpose of the security protocol is to ensure the security of the information. But if there are some leaks in the protocol itself, attackers will use the leaks to cause harm to the legitimate entities. Hence we need to analyze and test the protocol to verify that the protocol is expected to achieve its security goals.Strand Space Model is a formal approach for the analysis of the security protocols, which was proposed by Fabrega, Herzog and Guttman in 1998. The proposing of the model may make the designation and analysis of the security protocols easier. It is the most direct, simple and strict method of all the fomal methods for analysing the protocols. We have made the following aspects of work on the basis of the study of the model:1)We have studied the security property of the security protocols, in particular the confidentiality and the authentication.2)This paper analyzed MY-Helsinki protocol which is an improved protocol of Helsinki based on the SSM. It demonstrated the correctness of MY-Helsinki on secrecy and authentication, and indicated the reason of Helsinki's drawbacks.3)We have studied the application of ideal and authentication test in analysis of the security protocols. In this paper, the authentication of Weakened-Yahalom protocol is analyzed by ideal and authentication test respectively along with a comparison of them. 4)An overview of state space reduction technique is given in this paper via the study of the dynamic strand space model. Through studying the application of Authentication Test in protocol analysis, we bring forward a pruning theorem based on Authentication Test. We mend the node-binding algorithm and add several rules for bundle-extending. The pruning theorem is used in the process of the analyzing the authentication of protocols. This can reduce the state space and improve the efficiency of protocols analysis. The add of the rules for bundle-expanding enables the algorithm suitable to the protocols which including initiator, responder and server. Finally, two examples is given to illuminate the validity of the modification of the algorithm.