基于用戶屬性的遠(yuǎn)程證明協(xié)議的形式化研究.pdf

1、當(dāng)今信息化技術(shù)迅速發(fā)展，網(wǎng)絡(luò)深入到人們生活中的點(diǎn)點(diǎn)滴滴。網(wǎng)上購物越來越受歡迎,越來越多的人們通過在線支付進(jìn)行金融交易，公司通過各種內(nèi)部網(wǎng)絡(luò)來管理公司的內(nèi)部信息資料和數(shù)據(jù)共享，云計(jì)算向用戶提供了廣泛的網(wǎng)絡(luò)安全服務(wù)。人們金融交易的支付賬號(hào)和密碼、公司的重要機(jī)密文檔和數(shù)據(jù)、云環(huán)境中的用戶數(shù)據(jù)，這些安全操作都涉及了對(duì)機(jī)密重要數(shù)據(jù)的處理。因?yàn)楝F(xiàn)代網(wǎng)絡(luò)所具有的開放性和復(fù)雜性，這些數(shù)據(jù)容易被攻擊者收集進(jìn)行攻擊活動(dòng)，攻擊者可以在通信過程中截取用戶的金融

2、賬戶和密碼，可以惡意攻擊公司的終端或服務(wù)器以竊取重要信息數(shù)據(jù)等。因此在進(jìn)行網(wǎng)絡(luò)的各種安全操作前，網(wǎng)絡(luò)中的通信實(shí)體需要相互驗(yàn)證確認(rèn)對(duì)方的身份及配置信息以保證自身平臺(tái)的安全性，由可信計(jì)算組織提出的可信平臺(tái)TPM和遠(yuǎn)程證明協(xié)議，能夠有效防止此類基于可信計(jì)算的攻擊的發(fā)生。
　　遠(yuǎn)程證明協(xié)議提供可信數(shù)據(jù)以保證通信實(shí)體在網(wǎng)絡(luò)中的安全，確保與通信實(shí)體交互的平臺(tái)其身份的合法性以及其平臺(tái)所運(yùn)行軟件的可靠性，因此遠(yuǎn)程證明協(xié)議在網(wǎng)絡(luò)安全支付、網(wǎng)絡(luò)終端接

3、入和可信云服務(wù)等有重要的應(yīng)用，可以防止重要數(shù)據(jù)的泄露。移動(dòng)手機(jī)支付中，遠(yuǎn)程證明協(xié)議能夠?yàn)榻鹑诜?wù)器提供手機(jī)用戶的配置信息及可信性，可以為可信網(wǎng)絡(luò)驗(yàn)證所接入系統(tǒng)的終端設(shè)備，可以為云服務(wù)系統(tǒng)驗(yàn)證云節(jié)點(diǎn)的身份和完整性狀態(tài)。本文針對(duì)完整的遠(yuǎn)程證明協(xié)議進(jìn)行形式化分析研究，主要完成了如下工作：
　?。?）對(duì)遠(yuǎn)程證明協(xié)議進(jìn)行分析，使用SPIN模型檢測(cè)工具對(duì)協(xié)議進(jìn)行形式化分析
　　根據(jù)遠(yuǎn)程證明協(xié)議流程及需要滿足的安全目標(biāo)對(duì)協(xié)議進(jìn)行分析，主要

4、從用戶進(jìn)程 User和遠(yuǎn)程驗(yàn)證者 Verifier的角度對(duì)遠(yuǎn)程證明協(xié)議進(jìn)行分析，發(fā)現(xiàn)協(xié)議容易遭受到重放攻擊、偽裝攻擊和破壞攻擊。使用SPIN檢測(cè)到協(xié)議存在的攻擊路徑包括破壞PrivacyCA認(rèn)證性、破壞用戶User認(rèn)證性、破壞遠(yuǎn)程驗(yàn)證者Verifier認(rèn)證性和破壞用戶度量日志ML機(jī)密性等。分析得出協(xié)議存在安全漏洞。
　?。?）運(yùn)用用戶屬性對(duì)協(xié)議進(jìn)行改進(jìn)，形式化分析改進(jìn)后的協(xié)議
　　使用了基于用戶屬性加鹽哈希SHUA（Secu

5、re Hash with User Attributes Algorithm）方法證明 User平臺(tái)的合法身份，使用 User獨(dú)一無二的屬性添加到協(xié)議中進(jìn)行傳輸。同時(shí)使用SVO邏輯分析方法和SPIN模型檢測(cè)工具對(duì)改進(jìn)的基于用戶屬性的遠(yuǎn)程證明協(xié)議進(jìn)行形式化分析，SVO邏輯正向分析得出協(xié)議滿足安全認(rèn)證目標(biāo)，SPIN反向分析得出改進(jìn)協(xié)議的攻擊路徑已消除，協(xié)議的安全性有所提高。
　?。?）設(shè)計(jì)協(xié)議原型對(duì)協(xié)議能耗進(jìn)行測(cè)試
　　設(shè)計(jì)出協(xié)