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

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

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

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

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

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