Research Of Authentication Protocols And Their Formalized Analysis

The computer network is developing at the surprising pace. However, the problems on the security of network become more and more obvious, meanwhile, more and more complicated. It is the primary and difficult problem that the network application should confront. At present, the security protocol is one of the most effective methods to solve the security problem of the network. The communication of network needs to carry on the authentication between the entities through the safety protocol, allocate the key or other secrets safely among the entities, and confirm the non-repudiation of news, which is sent or received, and the like.Identity authentication key agreement protocol has two functions: one is to identify both sides of the communicators, and the other is to consult the secure session key together. Therefore, the security of identity authentication key agreement protocol influences the whole communication field directly. And the influences demand that the protocol must obtain the ability to resist various attacks. It is a challenging job to design and analyze an identity authentication key agreement protocol. The fact shows that a lot of safety protocols which are analyzed, designed and realized conscientiously by security experts still exist defaults, some of which are even found after it has been used for many years.Presently, public-key cryptography system, for its irreplaceable advantages in key management and extensibility, has become a mainstream for designing the authentication key agreement protocol. Take mobile communication as an example,the requirement to security for mobile communication is higher than before, and the security problems can't be ignored either. But the computing capability of mobile device relatively is low. The problem to the authentication key agreement protocol which is used at mobile communication is how to reduce the calculation of mobile device and should be solved. Nowadays, some protocols adopt the hash function to replace the signature to identify authentication. The calculation amount of the mobile device can be reduced by designing the protocols precisely.As the developing of the authentication key agreement protocol, the method of formalized analysis to security protocols must adapt to the new change of the new security protocols. This dissertation has chosen two influential methods on the fields of formalized analysis as the object of the research: one is SVO logic method, and the other is strand space method. The details of the research are as follows.①To expand and improve the SVO logic and the analysis goals of the SVO logic method.②To expand the theory of the strand space and its verification models.③To research a typical mutual authentication protocol, evident the Hijacking attack to the MA can not be founded , and point out an unknown key-share attack for the MA.④To point out a new mutual authentication and key agreement protocol -MAKAP3,which can be used at the field of mobile communication. By comparing the MAKAP-3 with the similar protocols in domesty, the new one gains more superior on the complexity of accounting and usability. Prove the security of the new protocol by using the improved SVO logic method and expanded strand space method separately.