基于用戶屬性的遠程證明協(xié)議的形式化研究
發(fā)布時間：2019-05-19 22:28
【摘要】：當(dāng)今信息化技術(shù)迅速發(fā)展,網(wǎng)絡(luò)深入到人們生活中的點點滴滴。網(wǎng)上購物越來越受歡迎,越來越多的人們通過在線支付進行金融交易,公司通過各種內(nèi)部網(wǎng)絡(luò)來管理公司的內(nèi)部信息資料和數(shù)據(jù)共享,云計算向用戶提供了廣泛的網(wǎng)絡(luò)安全服務(wù)。人們金融交易的支付賬號和密碼、公司的重要機密文檔和數(shù)據(jù)、云環(huán)境中的用戶數(shù)據(jù),這些安全操作都涉及了對機密重要數(shù)據(jù)的處理。因為現(xiàn)代網(wǎng)絡(luò)所具有的開放性和復(fù)雜性,這些數(shù)據(jù)容易被攻擊者收集進行攻擊活動,攻擊者可以在通信過程中截取用戶的金融賬戶和密碼,可以惡意攻擊公司的終端或服務(wù)器以竊取重要信息數(shù)據(jù)等。因此在進行網(wǎng)絡(luò)的各種安全操作前,網(wǎng)絡(luò)中的通信實體需要相互驗證確認對方的身份及配置信息以保證自身平臺的安全性,由可信計算組織提出的可信平臺TPM和遠程證明協(xié)議,能夠有效防止此類基于可信計算的攻擊的發(fā)生。遠程證明協(xié)議提供可信數(shù)據(jù)以保證通信實體在網(wǎng)絡(luò)中的安全,確保與通信實體交互的平臺其身份的合法性以及其平臺所運行軟件的可靠性,因此遠程證明協(xié)議在網(wǎng)絡(luò)安全支付、網(wǎng)絡(luò)終端接入和可信云服務(wù)等有重要的應(yīng)用,可以防止重要數(shù)據(jù)的泄露。移動手機支付中,遠程證明協(xié)議能夠為金融服務(wù)器提供手機用戶的配置信息及可信性,可以為可信網(wǎng)絡(luò)驗證所接入系統(tǒng)的終端設(shè)備,可以為云服務(wù)系統(tǒng)驗證云節(jié)點的身份和完整性狀態(tài)。本文針對完整的遠程證明協(xié)議進行形式化分析研究,主要完成了如下工作:(1)對遠程證明協(xié)議進行分析,使用SPIN模型檢測工具對協(xié)議進行形式化分析根據(jù)遠程證明協(xié)議流程及需要滿足的安全目標(biāo)對協(xié)議進行分析,主要從用戶進程User和遠程驗證者Verifier的角度對遠程證明協(xié)議進行分析,發(fā)現(xiàn)協(xié)議容易遭受到重放攻擊、偽裝攻擊和破壞攻擊。使用SPIN檢測到協(xié)議存在的攻擊路徑包括破壞PrivacyCA認證性、破壞用戶User認證性、破壞遠程驗證者Verifier認證性和破壞用戶度量日志ML機密性等。分析得出協(xié)議存在安全漏洞。(2)運用用戶屬性對協(xié)議進行改進,形式化分析改進后的協(xié)議使用了基于用戶屬性加鹽哈希SHUA(Secure Hash with User Attributes Algorithm)方法證明User平臺的合法身份,使用User獨一無二的屬性添加到協(xié)議中進行傳輸。同時使用SVO邏輯分析方法和SPIN模型檢測工具對改進的基于用戶屬性的遠程證明協(xié)議進行形式化分析,SVO邏輯正向分析得出協(xié)議滿足安全認證目標(biāo),SPIN反向分析得出改進協(xié)議的攻擊路徑已消除,協(xié)議的安全性有所提高。(3)設(shè)計協(xié)議原型對協(xié)議能耗進行測試設(shè)計出協(xié)議原型,生成APK文件,采用PowerTutor工具對改進的協(xié)議進行CPU、LED通信能耗測試。實驗證明協(xié)議的總體能耗不高,用于手機移動支付等具有輕量特點。
[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.
【學(xué)位授予單位】：太原理工大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2017
【分類號】：TP309
本文編號：2481117
[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.
【學(xué)位授予單位】：太原理工大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2017
【分類號】：TP309
【參考文獻】
相關(guān)期刊論文 前10條
1 肖美華;朱科;馬成林;;基于SPIN的Andrew Secure RPC協(xié)議并行攻擊模型檢測[J];計算機科學(xué);2015年07期
2 馮偉;馮登國;;基于串空間的可信計算協(xié)議分析[J];計算機學(xué)報;2015年04期
3 張曉偉;王崢;陳永樂;;一種基于用戶屬性的遠程證明方案[J];太原理工大學(xué)學(xué)報;2015年02期
4 田野;彭彥彬;楊玉麗;彭新光;;無線體域網(wǎng)中基于屬性加密的數(shù)據(jù)訪問控制方案[J];計算機應(yīng)用研究;2015年07期
5 冉俊軼;吳盡昭;;基于Spin的安全協(xié)議形式化驗證技術(shù)[J];計算機應(yīng)用;2014年S2期
6 肖茵茵;蘇開樂;;電子商務(wù)支付協(xié)議認證性的SVO邏輯驗證[J];計算機工程與應(yīng)用;2014年08期
7 閆建紅;;一種基于屬性證書的動態(tài)可信證明機制[J];小型微型計算機系統(tǒng);2013年10期
8 范玉濤;蘇桂平;;一種含時間因素的安全協(xié)議形式化分析方法[J];計算機應(yīng)用與軟件;2013年01期
9 譙婷婷;王樂;王芳;葛艷;;基于Coq的軟件安全性驗證[J];計算機應(yīng)用;2012年S2期
10 尤啟房;楊晉吉;;SIP協(xié)議的SPIN模型檢測[J];計算機工程與應(yīng)用;2014年13期
相關(guān)博士學(xué)位論文 前2條
1 付東來;基于可信平臺模塊的遠程證明關(guān)鍵技術(shù)研究及其應(yīng)用[D];太原理工大學(xué);2016年
2 魯來鳳;安全協(xié)議形式化分析理論與應(yīng)用研究[D];西安電子科技大學(xué);2012年
相關(guān)碩士學(xué)位論文 前1條
1 劉俏威;SPIN模型檢測的形式化分析機理研究及應(yīng)用[D];南昌大學(xué);2008年
，本文編號：2481117
本文鏈接：http://sikaile.net/shoufeilunwen/xixikjs/2481117.html
最近更新
教材專著
