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

【摘要】：在大數(shù)據(jù)時(shí)代的背景下,研究人員不斷探索數(shù)據(jù)融合與共享的解決方案。與此同時(shí),網(wǎng)絡(luò)信息安全也迎來(lái)了前所未有的挑戰(zhàn),黑客們樂(lè)衷于尋找網(wǎng)絡(luò)中的漏洞來(lái)發(fā)起惡意攻擊,竊取機(jī)密信息。網(wǎng)絡(luò)信息的傳輸主要依賴網(wǎng)絡(luò)協(xié)議,如何設(shè)計(jì)出安全可靠的網(wǎng)絡(luò)協(xié)議是保障網(wǎng)絡(luò)信息安全的關(guān)鍵途徑。形式化方法作為一種基于嚴(yán)格數(shù)學(xué)的技術(shù)手段,可用于驗(yàn)證協(xié)議的安全性質(zhì),找出潛在的漏洞,從而指導(dǎo)安全協(xié)議的設(shè)計(jì)與實(shí)現(xiàn)。為實(shí)現(xiàn)用戶賬號(hào)關(guān)聯(lián)和資源共享,互聯(lián)網(wǎng)工作任務(wù)組設(shè)計(jì)發(fā)布了OAuth 2.0協(xié)議。該協(xié)議實(shí)現(xiàn)用戶在不向第三方應(yīng)用透露用戶名密碼的情況,獲取存儲(chǔ)在資源服務(wù)器的受保護(hù)資源。但該協(xié)議由于自身的缺陷飽受攻擊,給企業(yè)與用戶帶來(lái)巨大損失。主要原因在于OAuth 2.0過(guò)度依賴https通道傳輸數(shù)據(jù)而忽視了自身數(shù)據(jù)的加密,另外https的傳輸效率低下,在網(wǎng)絡(luò)較差的環(huán)境下經(jīng)常中斷,從而招致黑客攻擊。為解決上述問(wèn)題,本文提出采用http通道傳輸OAuth 2.0協(xié)議數(shù)據(jù),并運(yùn)用公鑰體系對(duì)OAuth 2.0協(xié)議進(jìn)行加密改進(jìn)。基于Delvo-Yao攻擊者模型,采用Promela語(yǔ)言對(duì)改進(jìn)協(xié)議建模,以線性時(shí)態(tài)邏輯刻畫協(xié)議的安全性質(zhì)。最后通過(guò)SPIN工具對(duì)模型進(jìn)行檢測(cè)。實(shí)驗(yàn)結(jié)果表明,單憑公鑰加密,并不能保障OAuth 2.0協(xié)議的安全。在此基礎(chǔ)之上,本文再提出采用私鑰簽名對(duì)協(xié)議關(guān)鍵信息進(jìn)行簽名的進(jìn)一步改進(jìn)方案。以同樣的方式對(duì)新協(xié)議進(jìn)行驗(yàn)證,并沒(méi)有發(fā)現(xiàn)新協(xié)議中的漏洞。通過(guò)兩次驗(yàn)證工作的對(duì)比,得到具有高安全性的新協(xié)議;對(duì)比建模時(shí)采用的由類型檢查、靜態(tài)分析、語(yǔ)法重定序構(gòu)成的三種不同組合優(yōu)化策略,獲得新協(xié)議最優(yōu)的安全驗(yàn)證模型。除此之外,本文還提出通過(guò)程序枚舉法代替手工求解攻擊者知識(shí)庫(kù),以降低攻擊者模型構(gòu)建復(fù)雜度,使本文提出的攻擊者模型建模方法適用于擁有更多主體的協(xié)議的分析與驗(yàn)證。
[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.
【學(xué)位授予單位】：華東交通大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類號(hào)】：TP393.08

【相似文獻(xiàn)】

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

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

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

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

4 趙軍;;移動(dòng)IPv6協(xié)議安全機(jī)制優(yōu)化[J];淮陰工學(xué)院學(xué)報(bào);2008年01期

5 陶志紅,Hans KleineBu，

本文編號(hào)：1772397