Abstract:

In recent years, authentication tests has been improved and applied to the analysis of various security protocols. However, these improvement theorems also have certain defects in terms of application scope and accuracy. In response to these defects, in this paper, improved incoming test theorem and encryption test theorem are proposed, and proof of the improvement theorem is given. This paper points out the defects of the authentication test in use by analyzing the judgment of the normal nodes in the authentication test, the errors in the proof process, and the inaccuracies and errors in the process of parameter consistency verification. Based on these defects, an improved formal analysis method recursion test is proposed. This method is used to prove BAN-Yahalom protocol, the result proves this method has expanded the scope of the use of authentication tests, and can analyze the security protocol effectively, accurately.

Key words: strand space, authentication tests, formal analysis method, security protocol