Research On Combination Of Formal Analysis Methods To Security Protocols

With the development of the computer network technology, The Internet play the more and more important role in every filed of the society. The security problems of computer network have benn exposed more and more. Network threatens and attacks affect the society economic, politics and life which run in gear. So, it is very important to protect the information security.Security protocols belong to the communication protocols.The main purpose of security protocol is to realize key agreement and authentication using cryptography. So, security protocols are one of the effective methods and tactics to protect the network security. The security protocols can solve the authentication problem of entitys, and it can use to be transfer the security problem such as the integrality of information, non-repudiation of sender and receiver. But, it is very difficult to design a security protocol or the authentic security protocol's authentication which can accord with the requirement .The measure to analyzed the security protocols usually used the formal analysis methods. By more than the twenty years researches in the information security field, there are many kinds of security protocol formal analysis methods and the corresponding automatic validation tools can be chosen, such as the BAN method belongs to model logic methods, the model checking tools of state search tools and the strand space model of the theorem proving method. Each kind of the security protocol formal analysis methods have their's particular advantages. But it also has been proved the limitation in the practical application. This paper attempts from BAN logic of combining with the model checking, the model checking and the strand space model, as well as different model checking of integration between tools in terms of how to integrate formal analysis methods, play to their respective advantages and enhance security protocol analysis efficiency.This paper analyze the design idea of the new combined security protocol formal analysis methods, and put forward a instance of combined security protocol formal analysis methods which is based on the CAPSL. Use the CAPSL to design the connector which can realize combining two security protocol formal research methods.Finally, this paper put forward ideas and methods of review and analysis, and research on security protocols for the future development trends forecast...