Research On Formal Modeling And Verification For Trusted Authentication And Authorization Protocol

With the development of network diversification and the emergence of new tech-nologies,such as mobile payment and social network,the authentication and authoriza-tion technology in the field of information security has been greatly developed.Trusted authentication protocol and authorization protocol have drawn more and more attention in recent years.These protocols have the characteristics of security attributes of diver-sity and logical structure complexity,which makes it difficult to construct the verifi-cation model and accurately describe the security attributes of the protocol.Therefore,the problems of security analysis on trusted authentication protocol and authorization protocol become a difficult and critical issue in security research.Formal verification of security protocols is an important method,mainly used for automated verification of security protocols.Its principle is to convert the security protocol into a mathematical model,and the security requirements to meet the agreement converted to a mathemat-ical formula.This method,based on rigorous mathematical logic,is recognized as an effective method to prove the security of the protocol.In order to solve the above problems,this dissertation focuses on the formal mod-eling and verification of a trusted attribute authentication system and authorization pro-tocol dynamic client registration protocol.Firstly,the formalized model frame of the attribute authentication system for optional disclosure is presented.Secondly,the for-mal analysis and security verification of the complex trusted attribute authentication protocol U-Prove are carried out.Finally,the thesis formal models the client dynamic registration protocol in the authorization protocol.During the process of modeling,it is found that the protocol has security risks in a specific environment,and then the improvement measures are proposed.The improved protocol is verified by formal ver-ification method.Specific research contents are as follows:(1)Aiming at the requirement of formal modeling of trusted authentication system,a formal model framework of attribute authentication system for selective disclosure is proposed.The abstract structure of the optional disclosure attribute authentica-tion system is described,and the attribute structure,entity structure and behavior characteristics of the system are described.The type definition is added to the dif-ferent attributes of the user.The classification functions and the specific behavior descriptions are given,and the interaction behaviors during entities of the sestem is ed.The process description of execution conditions and specific behaviors are given.Security features are defined according to the privacy of signature un-forgeability,anonymity and attributes that the system needs to satisfy.The model has practical significance for system design and security analysis.(2)Based on the previous work,the model detection method is applied to the formal verification of a trusted authentication protocol—U-Prove.U-Prove is a new com-plex cryptography technology,whose core is a U-Prove token with attributes em-bedded.Through the token,the user can identify his identity without revealing any private information.Firstly,the formalized modeling of U-Prove protocol and the formal modeling of the security attributes satisfied by the protocol are com-pleted by using the above model analysis method.Then,the verification of the related security attributes of the protocol is accomplished through the ProVerif tool.Experimental results show that the protocol model can meet the relevant security attributes.(3)Furthermore,in the formalized analysis of client dynamic registration protocol in the open authorization protocol,it is found that it has the security hidden danger,and the corresponding improvement measures are put forward.The improved client dynamic registration protocol is formalized.In the original open authorization pro-tocol,the user completely trusts the authorization server,and lacks the checking mechanism for the correctness and integrity of the registered client registration in-formation.Once the authorization server is attacked in the application layer after the client is registered,the attacker can tamper with or forge the registration in-formation of the client at will,resulting in the user being redirected to a malicious site when authorized.In this paper,an improved method is put forward to protect the registration information by introducing the security registry to protect the reg-istration information,so that the user can analyze the reliability of the registration information of the client when authorized,thus avoiding the above attacks.In order to verify the security characteristics of the improved protocol,the new protocol is modeled and formally verified.The experimental results show that the improved protocol can avoid the attack in the original protocol and has higher security.