本文選題：網(wǎng)絡(luò)安全 + OAuth��； 參考：《華東交通大學》2016年碩士論文

【摘要】：在大數(shù)據(jù)時代的背景下,研究人員不斷探索數(shù)據(jù)融合與共享的解決方案。與此同時,網(wǎng)絡(luò)信息安全也迎來了前所未有的挑戰(zhàn),黑客們樂衷于尋找網(wǎng)絡(luò)中的漏洞來發(fā)起惡意攻擊,竊取機密信息。網(wǎng)絡(luò)信息的傳輸主要依賴網(wǎng)絡(luò)協(xié)議,如何設(shè)計出安全可靠的網(wǎng)絡(luò)協(xié)議是保障網(wǎng)絡(luò)信息安全的關(guān)鍵途徑。形式化方法作為一種基于嚴格數(shù)學的技術(shù)手段,可用于驗證協(xié)議的安全性質(zhì),找出潛在的漏洞,從而指導(dǎo)安全協(xié)議的設(shè)計與實現(xiàn)。為實現(xiàn)用戶賬號關(guān)聯(lián)和資源共享,互聯(lián)網(wǎng)工作任務(wù)組設(shè)計發(fā)布了OAuth 2.0協(xié)議。該協(xié)議實現(xiàn)用戶在不向第三方應(yīng)用透露用戶名密碼的情況,獲取存儲在資源服務(wù)器的受保護資源。但該協(xié)議由于自身的缺陷飽受攻擊,給企業(yè)與用戶帶來巨大損失。主要原因在于OAuth 2.0過度依賴https通道傳輸數(shù)據(jù)而忽視了自身數(shù)據(jù)的加密,另外https的傳輸效率低下,在網(wǎng)絡(luò)較差的環(huán)境下經(jīng)常中斷,從而招致黑客攻擊。為解決上述問題,本文提出采用http通道傳輸OAuth 2.0協(xié)議數(shù)據(jù),并運用公鑰體系對OAuth 2.0協(xié)議進行加密改進�；贒elvo-Yao攻擊者模型,采用Promela語言對改進協(xié)議建模,以線性時態(tài)邏輯刻畫協(xié)議的安全性質(zhì)。最后通過SPIN工具對模型進行檢測。實驗結(jié)果表明,單憑公鑰加密,并不能保障OAuth 2.0協(xié)議的安全。在此基礎(chǔ)之上,本文再提出采用私鑰簽名對協(xié)議關(guān)鍵信息進行簽名的進一步改進方案。以同樣的方式對新協(xié)議進行驗證,并沒有發(fā)現(xiàn)新協(xié)議中的漏洞。通過兩次驗證工作的對比,得到具有高安全性的新協(xié)議;對比建模時采用的由類型檢查、靜態(tài)分析、語法重定序構(gòu)成的三種不同組合優(yōu)化策略,獲得新協(xié)議最優(yōu)的安全驗證模型。除此之外,本文還提出通過程序枚舉法代替手工求解攻擊者知識庫,以降低攻擊者模型構(gòu)建復(fù)雜度,使本文提出的攻擊者模型建模方法適用于擁有更多主體的協(xié)議的分析與驗證。
[Abstract]:Against the background of big data's time, researchers have been exploring solutions for data fusion and sharing.At the same time, network information security is facing unprecedented challenges. Hackers are happy to search for loopholes in the network to launch malicious attacks and steal confidential information.The transmission of network information mainly depends on network protocol. How to design a safe and reliable network protocol is a key way to ensure the security of network information.As a technical method based on strict mathematics, formal method can be used to verify the security properties of the protocol, identify potential vulnerabilities, and guide the design and implementation of the security protocol.In order to realize user account association and resource sharing, the Internet Task Force designed and published OAuth 2.0 protocol.This protocol enables users to obtain protected resources stored in resource servers without revealing user names and passwords to third parties.However, the protocol has been attacked because of its own defects, which brings huge losses to enterprises and users.The main reason is that OAuth 2.0 excessively relies on the https channel to transmit data and neglects the encryption of its own data. In addition, the transmission efficiency of https is low, and it is often interrupted in the poor network environment, which leads to hacker attacks.In order to solve the above problems, this paper proposes to use http channel to transmit OAuth 2.0 protocol data, and use public key architecture to encrypt OAuth 2.0 protocol.Based on the Delvo-Yao attacker model, the improved protocol is modeled by Promela language, and the security property of the protocol is described by linear temporal logic.Finally, the model is detected by SPIN tool.Experimental results show that public key encryption alone can not guarantee the security of OAuth 2.0 protocol.On this basis, this paper proposes a further improvement scheme to use private key signature to sign the key information of the protocol.Verification of the new protocol in the same way does not reveal any vulnerabilities in the new protocol.Through the comparison of two verification work, a new protocol with high security is obtained, and three different combinatorial optimization strategies, which are composed of type checking, static analysis and syntax reordering, are adopted in the comparison modeling.The optimal security verification model of the new protocol is obtained.In addition, in order to reduce the complexity of constructing the attacker's model, this paper proposes to replace the manual solution of the attacker's knowledge base by program enumeration.The model modeling method proposed in this paper is suitable for the analysis and verification of protocols with more agents.
【學位授予單位】：華東交通大學
【學位級別】：碩士
【學位授予年份】：2016
【分類號】：TP393.08

【相似文獻】

相關(guān)期刊論文 前10條

1 鄧帆;鄧少鋒;張文政;;安全協(xié)議的規(guī)范化設(shè)計[J];計算機工程與應(yīng)用;2011年18期

2 來學嘉;基于挑戰(zhàn)-響應(yīng)的認證協(xié)議安全的必要條件(英文)[J];中國科學院研究生院學報;2002年03期

3 李莉;張煥國;王張宜;;一種安全協(xié)議的形式化設(shè)計方法[J];計算機工程與應(yīng)用;2006年11期

4 趙軍;;移動IPv6協(xié)議安全機制優(yōu)化[J];淮陰工學院學報;2008年01期

5 陶志紅,Hans KleineBu，

本文編號：1772397