基于用户属性的远程证明协议的形式化研究

发布时间：2019-05-19 22:28

【摘要】：当今信息化技术迅速发展,网络深入到人们生活中的点点滴滴。网上购物越来越受欢迎,越来越多的人们通过在线支付进行金融交易,公司通过各种内部网络来管理公司的内部信息资料和数据共享,云计算向用户提供了广泛的网络安全服务。人们金融交易的支付账号和密码、公司的重要机密文档和数据、云环境中的用户数据,这些安全操作都涉及了对机密重要数据的处理。因为现代网络所具有的开放性和复杂性,这些数据容易被攻击者收集进行攻击活动,攻击者可以在通信过程中截取用户的金融账户和密码,可以恶意攻击公司的终端或服务器以窃取重要信息数据等。因此在进行网络的各种安全操作前,网络中的通信实体需要相互验证确认对方的身份及配置信息以保证自身平台的安全性,由可信计算组织提出的可信平台TPM和远程证明协议,能够有效防止此类基于可信计算的攻击的发生。远程证明协议提供可信数据以保证通信实体在网络中的安全,确保与通信实体交互的平台其身份的合法性以及其平台所运行软件的可靠性,因此远程证明协议在网络安全支付、网络终端接入和可信云服务等有重要的应用,可以防止重要数据的泄露。移动手机支付中,远程证明协议能够为金融服务器提供手机用户的配置信息及可信性,可以为可信网络验证所接入系统的终端设备,可以为云服务系统验证云节点的身份和完整性状态。本文针对完整的远程证明协议进行形式化分析研究,主要完成了如下工作:(1)对远程证明协议进行分析,使用SPIN模型检测工具对协议进行形式化分析根据远程证明协议流程及需要满足的安全目标对协议进行分析,主要从用户进程User和远程验证者Verifier的角度对远程证明协议进行分析,发现协议容易遭受到重放攻击、伪装攻击和破坏攻击。使用SPIN检测到协议存在的攻击路径包括破坏PrivacyCA认证性、破坏用户User认证性、破坏远程验证者Verifier认证性和破坏用户度量日志ML机密性等。分析得出协议存在安全漏洞。(2)运用用户属性对协议进行改进,形式化分析改进后的协议使用了基于用户属性加盐哈希SHUA(Secure Hash with User Attributes Algorithm)方法证明User平台的合法身份,使用User独一无二的属性添加到协议中进行传输。同时使用SVO逻辑分析方法和SPIN模型检测工具对改进的基于用户属性的远程证明协议进行形式化分析,SVO逻辑正向分析得出协议满足安全认证目标,SPIN反向分析得出改进协议的攻击路径已消除,协议的安全性有所提高。(3)设计协议原型对协议能耗进行测试设计出协议原型,生成APK文件,采用PowerTutor工具对改进的协议进行CPU、LED通信能耗测试。实验证明协议的总体能耗不高,用于手机移动支付等具有轻量特点。
[Abstract]:Nowadays, with the rapid development of information technology, the network goes deep into people's lives. Online shopping is becoming more and more popular, more and more people carry out financial transactions through online payment, and companies manage the company's internal information and data sharing through a variety of internal networks. Cloud computing provides users with a wide range of network security services. The payment account and password of people's financial transactions, the important confidential documents and data of the company, and the user data in the cloud environment all involve the processing of confidential and important data. Because of the openness and complexity of modern networks, this data is easily collected and attacked by attackers, who can intercept users' financial accounts and passwords during communication. Can maliciously attack the company's terminal or server to steal important information and data, and so on. Therefore, before carrying out all kinds of secure operations of the network, the communication entities in the network need to verify and confirm each other's identity and configuration information in order to ensure the security of their own platform. The trusted platform TPM and remote certification protocol proposed by the trusted computing organization. It can effectively prevent such attacks based on trusted computing. The remote certification protocol provides trusted data to ensure the security of the communication entity in the network, to ensure the legitimacy of the identity of the platform interacting with the communication entity and the reliability of the software running on the platform, so the remote certification protocol pays securely in the network, Network terminal access and trusted cloud service have important applications, which can prevent the leakage of important data. In the mobile phone payment, the remote proof protocol can provide the configuration information and credibility of the mobile phone user for the financial server, and can verify the terminal equipment of the accessed system for the trusted network. You can verify the identity and integrity of cloud nodes for cloud service systems. In this paper, the formal analysis of the complete remote certification protocol is carried out, and the main work is as follows: (1) the remote certification protocol is analyzed. The formal analysis of the protocol is carried out by using SPIN model detection tool according to the process of remote certification protocol and the security objectives to be satisfied, and the remote certification protocol is analyzed mainly from the point of view of user process User and remote verifier Verifier. It is found that the protocol is vulnerable to replay attack, camouflage attack and sabotage attack. The attack paths detected by SPIN include destroying PrivacyCA authentication, destroying user User authentication, destroying remote verifier Verifier authentication and destroying user metric log ML confidentiality. It is concluded that there are security vulnerabilities in the protocol. (2) the user attribute is used to improve the protocol, and the improved protocol is formally analyzed by using the method of user attribute plus salt SHUA (Secure Hash with User Attributes Algorithm) to prove the legal identity of the User platform. Use User unique properties to add to the protocol for transmission. At the same time, SVO logic analysis method and SPIN model detection tool are used to formalize the improved remote proof protocol based on user attributes. SVO logic forward analysis shows that the protocol meets the security authentication goal. SPIN reverse analysis shows that the attack path of the improved protocol has been eliminated, and the security of the protocol has been improved. (3) the protocol prototype is designed to test the energy consumption of the protocol, and the APK file is generated. PowerTutor tool is used to test the energy consumption of CPU,LED communication. The experimental results show that the overall energy consumption of the protocol is not high, and it is light to be used in mobile payment.
【学位授予单位】：太原理工大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP309

【参考文献】