Formal Research Of The Remote Attestation Protocol Based On User Attributes

With the rapid development of modern information technology,the network has penetrated into the life of people bit by bit.Online shopping is becoming more and more popular,and increasing people through the financial transactions to online payment,the company through a variety of internal network to manage the company's internal information and data sharing,cloud computing provides extensive network security services to the users.People's pay for financial transactions' account and password,the company's important confidential documents and data,cloud environment and user data,these security operations are involved in handling of confidential important data.Because of the openness and complexity of modern network,these data can be collected by attacker to take active attacks,the attacker can intercept the user financial account and password in the communication process,or can attack the company's terminal or server to steal important information data.Before the safe operation of the network,the communication entities in the network need to verify each other to confirm the identity and configuration information of the other party in order to ensure the safety of its own platform,trusted platform TPM and remote attestation protocol proposed by trusted computing,can effectively prevent the occurrence of such attacks based on trusted computing.Remote attestation protocol provides reliable data to ensure the communication entities in the network security and reliability,ensure the legitimacy of the platform and the reliability of the software running on the platform,so the remote attestation protocol in network security payment,network access and trusted cloud services have an important application,can prevent leakage of important data.In the mobile phone payment,remote attestation protocol can provide configuration information and credibility of mobile phone users for financial server,terminal device can be verified to access system for trusted network,can verify the identity and integrity of the state of the cloud node for cloud service system.In this paper,the research of formal analysis of the complete remote attestation protocol is mainly completed as follows:(1)Analyse the remote attestation protocol,and the SPIN model checking tool is used to formal analysis of the protocol.According to the remote attestation process and the security objectives to be met to analysis the protocol,mainly analyzed from the point of view of User and Verifier,discovery protocol is vulnerable to replay attack,impersonation attack and damage attack.Using SPIN to detect the existence of the attack path of the protocol,including destruction of PrivacyCA authentication,destruction of User authentication,destruction of remote Verifier authentication and destruction of user ML confidentiality,etc.Analysis shows that there are security vulnerabilities.(2)Use the user attributes to improve the protocol,formal analysis of the improved protocol.Use the user attributes based on hash SHUA(Secure Hash with with User Attributes Algorithm)method to prove the legal status of the user platform,the one and only attribute added to the protocol for transmission.At the same time using the SVO logic analysis method and SPIN model checking tool to formal analyse the improved remote attestation protocol based on user property,SVO logic forward analysis shows that the protocol meets the security certification goals.SPIN reverse analysis shows that the attack paths of the improved protocol has been eliminated,and the security of the protocol is improved.(3)Design the prototype of protocol to test the protocol energy consumption.Design the protocol prototype,generate APK files,using PowerTutor tools to test the protocol communication energy consumption of CPU and LED,the overall energy consumption of experiments prove that the protocol is not high,for mobile phone mobile payment with lightweight characteristics.