The Extension And Application Of Strand Space

With the development of Internet technology, security protocols play a more and more important role in e-business and e-government application. Due to so much attention paid on the field of security protocols analysis, kinds of formal methods for protocol analysis spring up during recent years. we introduce the basic concept and theory of strand space and analyze three branches of strand space in detail, not only their theory but also how to apply them to analyze protocols in practice. the character and advantage of strand space can be demonstrated.Then, by virtue of strand space, we analyze general challeange-response protocol and SSL/TLS handshake protocol in a careful way. By modeling protocols with strand space, we give a detail analysis on corresponding protocols under different cryptography system step by step. As a result, we find the effective attack of these protocols through authentication test and hereby modify the implementation of the protocols. In addition, we obtain some important principles for protocol analysis and design which can be applied to solve related problems in the filed of security protocols. All the above extend the application of strand space, and represent the value of strand space both in theory and practice.Moreover, strand space still has some flaws in some aspects. On the focus of cryptography operation and security goals analyzed by strand space, the reaseach perfects some branches of strand space besides its basic concept, premise and capability of attackers. Specially, applying the extended branch of authentication test to analyze Yahalom protocol, we can get good result to prove the the performance of the amelioration. Furthermore, it can help design protocol to a certain extent.Modeling the protocols by the bundle chart of strand space, the research put forwad a new method for protocol analysis based on message matching. This method not only absorbs the merits of some methods about logic reasoning and model checking, but also has its own complete theory and steps for protocol analysis. Through assigning constants to variable for elements of protocols, honest principles can find attacks by matching the form of message during different roles played by attackers. Take Needham-Schroeder protocol as an example, we execute this method step by step and concequently find the flaw of this protocol. Then we can also combine the exsiting branches of strand space to simplify this new method. In conclusion, This new formal method is an important and useful xtension to strand space .