Research On Formal Analysis Methods Of Security Protocols Based On Strand Space Model

Abstract:Communications security which bases on computer network not only relies on good encryption algorithm, but also relies on the correct security protocol. However, due to the complexity in designing of the security protocol, designing a correct security protocol is a very difficult thing. Therefore, analysis which is located on correctness must be carried on to a new security protocol before it will be put into use.The methods of security protocol analysis were mainly divided into two parts: formal analysis method and non-formal analysis method, of which the first one is a focus of theoretical research for its more profound and more comprehensive analytical capability. In the existing formal analysis methods, Strand Space Model draws more attentions for its succinct, strict and effective characteristics.In this thesis, research mainly focuses on three theory branches of Strand Space Model ,which respectively are minimal element theory, ideals and honesty theory, authentication tests theory,and,according to the concrete protocols the following analysis practice was made:(1) Based on the minimal members theory and ideals theory, from the authentication and secret aspects, formal analysis was carried on to a mutual-authentication cryptographic protocol which was used in network management , and through the analysis the redundancy which exists in the protocol was discovered and the corresponding improvement was proposed; Meanwhile in the aspect of authentication design to the protocol, the difference between the authentication protocols which based on the private-key cryptosystem and one which based on the public-key cryptosystem was pointed out.(2) Based on ideals and honesty theory, from the authentication and secret aspects, formal analysis was carried on for the first time by using the strand space model to a new authentication protocol which was proposed based on the Needham-Schroeder Protocol and Otway-Rees Protocol.(3) Based on authentication tests theory, formal analysis was carried on from the authentication aspect to old Woo-Lam protocol, Corresponding improvement plan to the flaw which exists in the authentication aspect of the old Woo-Lam protocol was proposed, and the improved Woo-Lam protocol was proven that it satisfies the authentication goal by using authentication tests method again.In the end, the extension of the Strand Space Model theory was introduced and the development direction of Strand Spaces Model theory has been discussed.