Research On Security Protocol Formal Verification Tools Automatically AVISPA

In recent years, the rapid development of network technology to mankind variousconvenience there is also an increasing number of network and information security problems.According to statistics, by2010, China’s Internet users more than420million but less than40%of Internet users with network security awareness. In2012, China’s e-commercetransactions amounted to more than800million yuan more than400billion yuan, the amountof online shopping.2014defense budget draft submitted by the United States in2013, thenetwork security funds increased significantly from4.7billion to intercept network attacksfrom other countries. Network information security is not only related to the security ofpersonal information related to national security.In order to ensure network and information security, the cryptosystem based on securityprotocol in the network to act as a communication protocol. Security protocols are widelyused in computer networks and distributed systems, has become an important part ofe-commerce and computer communications. However, while these security protocol usesencryption algorithm, but cannot guarantee that the network has been in a safe state, as longas the hackers find the appropriate tools, and soon the network security protocol soon becompromised, the information can easily be stolen, tampering by malicious destruction.Usually attack test methods and formal analysis methods to ensure the safety of thesecurity protocol. The attack test method is based on the various known attacks on securityprotocol analysis, the analysis must be known before a variety of attacks, but in practicalapplications, most of the attacker in the pre-analysis is unknowable. Another security protocolanalysis formal analysis is not required prior to analysis known attacks, formal analysismethods to analyze more in line with the practical application of the security agreement.Formal analysis of security protocols based on automatically through the use of formalverification tools AVISPA analyze the agreement Yalalom, comprehensive automatedverification tools AVISPA security protocol verification. The content of this paper include thefollowing aspects:1、 Described the development and characteristics of the network and informationsecurity, in-depth study of network information security based on the background andsignificance of the thesis. 2、 Through the analysis of the security protocols formalized, detailed analysis of thesecurity protocol formal analysis of classification, applications and related algorithms.3、 Details of the security protocol formal verification tools AVISPA technology,validated and adopted the AVISPA Yalalom agreement. And improve analysis Yalalomagreement.