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

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

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

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

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

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