Research On The Application Of Authentication Tests In Formal Analysis Of Security Protocol

In this paper, we do deep research on the application of Authentication Tests in security protocol analysis, and propose the Expanded Authentication Tests, based on which we design the automatic security protocol analysis system.Authentication Tests is a security protocol analysis method based on Strand Space. The deficiency of Authentication Tests is that it overlooks the relationship between test attribute and encrypted key. Therefore we introduce the definition of Key matrix and focus on the attribute of the authentication tests with different types of encrypted key and propose a series of propositions for protocol analysis and revision. These propositions enhance the original authentication tests model. The analysis and redesign of the Needham-Schroeder protocol , Yahalom protocol and EAP-AKA protocol show that the Expanded Authentication Tests are more efficient compared with the initial one and have the ability to repair the protocol with flaws.Based on Expanded Authentication Tests, we design the automatic security protocol analysis algorithms: P algorithms. This algorithm can prove both initiator and responder at the same time, so it is more efficient. To analyze large amount of protocols efficiently, we design the formal protocol description language P language, and develop the parser based on it. By proving Needham-Schroeder protocol, we show the procedure of P algorithms.At last we introduce the automatic security protocol analysis system, and use this system to verify Needham-Schroeder protocol, NSL protocol and Woo-Lam protocol. The results are coincident with the manual ones.