本文關(guān)鍵詞：OAuth協(xié)議的形式化建模與驗(yàn)證

  更多相關(guān)文章： 可滿足性 OAuth協(xié)議 模型檢驗(yàn) ASLan++建模語言

【摘要】：過去的幾年內(nèi),互聯(lián)網(wǎng)日趨火熱,各行各業(yè)的系統(tǒng)愈發(fā)需要與互聯(lián)網(wǎng)進(jìn)行融合,來優(yōu)化自身系統(tǒng)架構(gòu),提升系統(tǒng)性能,進(jìn)而創(chuàng)造更多的經(jīng)濟(jì)價(jià)值。同時(shí),互聯(lián)網(wǎng)內(nèi)部的系統(tǒng)也迫切需要通過信息的共享以及信息的整合來達(dá)到強(qiáng)化系統(tǒng)并提供更好的服務(wù)的目的。為了實(shí)現(xiàn)信息的共享,2010年4月互聯(lián)網(wǎng)工程任務(wù)組的OAuth工作組發(fā)布了OAuth1.0協(xié)議,規(guī)范了授權(quán)標(biāo)準(zhǔn),提供了統(tǒng)一授權(quán)流程。通過OAuth,第三方應(yīng)用可以訪問用戶授權(quán)的資源,而不需要用戶提供其登錄信息。OAuth定義了第三方應(yīng)用和授權(quán)服務(wù)器以及用戶之間的行為,通過規(guī)范不同角色的行為來實(shí)現(xiàn)信息的安全可靠共享。但是,如何保證不同角色在交互過程中,系統(tǒng)依舊能夠提供安全可靠的服務(wù)呢?基于這個(gè)問題,本文采用了嚴(yán)格的數(shù)學(xué)方法——形式化方法,以最新版本OAuth 2.0協(xié)議中的授權(quán)碼模型為實(shí)例,采用了ASLan++語言對授權(quán)協(xié)議進(jìn)行了十分完善的形式化建模。ASLan++是AVANTSSAR平臺的形式化建模語言,專門用來形式化描述建立在傳輸層和應(yīng)用層上的對于安全十分敏感的組合Web服務(wù)的架構(gòu),并且規(guī)范化與這個(gè)架構(gòu)相關(guān)聯(lián)的安全策略和安全性質(zhì)。本文在使用ASLan++語言建立的授權(quán)碼形式化模型基礎(chǔ)之上,從機(jī)密性,驗(yàn)證性,授權(quán)性,一致性,錯(cuò)誤處理,令牌時(shí)效性六個(gè)方面進(jìn)行模型分析,并通過線性時(shí)態(tài)邏輯公式表達(dá)這些性質(zhì),最后,采用AVANTSSAR的后臺驗(yàn)證工具——SAT模型檢查器,對這六個(gè)方面的性質(zhì)進(jìn)行自動化檢查,最終找出了狀態(tài)碼、授權(quán)碼的泄露以及用戶授權(quán)存在不一致性等問題,針對這些問題,本文最后分析了出現(xiàn)這些問題的原因,并給予了解決方案。
【關(guān)鍵詞】：可滿足性 OAuth協(xié)議 模型檢驗(yàn) ASLan++建模語言
【學(xué)位授予單位】：華東師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：TP393.04
【目錄】：

• 中文摘要6-7
• Abstract7-12
• 第一章 引言12-18
• 1.1 OAuth協(xié)議簡介12-13
• 1.2 OAuth協(xié)議研究現(xiàn)狀13-14
• 1.3 本文研究目標(biāo)及貢獻(xiàn)14-15
• 1.4 本文結(jié)構(gòu)15-18
• 第二章 OAuth 2.0概述及授權(quán)碼模型18-26
• 2.1 OAuth 2.0概述18-19
• 2.2 OAuth 2.0授權(quán)碼模型架構(gòu)及詳細(xì)流程19-24
• 2.3 OAuth 2.0授權(quán)碼模型實(shí)例24-25
• 2.4 本章小結(jié)25-26
• 第三章 AVANTSSAR形式化模型架構(gòu)及語法規(guī)則26-32
• 3.1 AVANTSSAR形式化模型架構(gòu)26-27
• 3.2 ASLan++語法規(guī)則27-31
• 3.3 AVANTSSAR后臺驗(yàn)證工具31
• 3.4 本章小結(jié)31-32
• 第四章 建立OAuth 2.0授權(quán)碼形式化模型32-46
• 4.1 搭建OAuth 2.0授權(quán)碼形式化模型框架32-35
• 4.2 形式化描述OAuth.2.0授權(quán)碼模型的用戶登錄階段35-38
• 4.3 形式化描述OAuth 2.0授權(quán)碼模型的授權(quán)碼交換階段38-39
• 4.4 形式化描述OAuth 2.0授權(quán)碼模型的獲取資源階段39-41
• 4.5 形式化描述OAuth 2.0授權(quán)碼模型的令牌更新階段41-43
• 4.6 本章小結(jié)43-46
• 第五章 OAuth 2.0授權(quán)碼模型性質(zhì)分析與驗(yàn)證46-62
• 5.1 OAuth 2.0授權(quán)碼模型性質(zhì)分析46-48
• 5.2 對OAuth 2.0授權(quán)碼模型性質(zhì)進(jìn)行建模48-57
• 5.3 OAuth 2.0授權(quán)碼模型性質(zhì)驗(yàn)證及結(jié)果分析57-60
• 5.4 本章小結(jié)60-62
• 第六章 總結(jié)及展望62-64
• 6.1 總結(jié)62-63
• 6.2 展望63-64
• 參考文獻(xiàn)64-68
• 附錄 授權(quán)碼形式化模型源代碼68-78
• 作者研究生階段參加的項(xiàng)目及發(fā)表文章情況78-80
• 致謝80

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 余潔;李曦;周學(xué)海;高妍妍;;基于事件B的處理器形式化建模方法的研究[J];系統(tǒng)仿真學(xué)報(bào);2007年03期

2 陳瀟怡;何炎祥;;一種可擴(kuò)展的數(shù)字權(quán)限表達(dá)語言的形式化建模及分析[J];武漢大學(xué)學(xué)報(bào)(理學(xué)版);2013年01期

3 馬忠貴;葉斌;曾廣平;涂序彥;;基于π演算的軟件人群體形式化建模[J];北京理工大學(xué)學(xué)報(bào);2006年02期

4 仲輝;陳超;王維平;李群;;基于π演算的指揮決策行為形式化建模研究[J];系統(tǒng)仿真學(xué)報(bào);2007年15期

5 王世進(jìn);;分布式制造調(diào)度體系結(jié)構(gòu)的π演算形式化建模[J];計(jì)算機(jī)工程與應(yīng)用;2010年09期

6 陳偉芳;金智勇;高濟(jì);周斌斌;;MAS應(yīng)用域本體的形式化建模及變換[J];浙江樹人大學(xué)學(xué)報(bào)(自然科學(xué)版);2013年02期

7 丁湘陵;王志剛;;UML包與B結(jié)合的形式化建模研究[J];懷化學(xué)院學(xué)報(bào);2010年11期

8 李月星;李曉娟;關(guān)永;王瑞;張杰;魏洪興;;SpaceWire協(xié)議的形式化建模與概率分析[J];小型微型計(jì)算機(jī)系統(tǒng);2013年09期

9 郝莉莉;楊惠珍;謝攀;;CPN在FCM形式化建模與驗(yàn)證中的應(yīng)用[J];計(jì)算機(jī)仿真;2011年06期

10 沈嘯;陳邦興;唐晨;;基于Event-B的一種聯(lián)鎖邏輯的形式化建模研究[J];信息技術(shù);2013年02期

中國重要會議論文全文數(shù)據(jù)庫 前1條

1 蔡遠(yuǎn)利;于振華;王瑞峰;;多Agent系統(tǒng)形式化建模方法學(xué)[A];'2006系統(tǒng)仿真技術(shù)及其應(yīng)用學(xué)術(shù)交流會論文集[C];2006年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前1條

1 胡曉輝;智能分布監(jiān)控系統(tǒng)軟件形式化建模和設(shè)計(jì)研究[D];西北工業(yè)大學(xué);2007年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 夏倩倩;協(xié)同應(yīng)用流程并行交互的形式化建模研究[D];內(nèi)蒙古大學(xué);2012年

2 肖知屹;列車安全距離控制形式化建模與驗(yàn)證[D];蘭州交通大學(xué);2014年

3 熊錫嬌;列車自動防護(hù)系統(tǒng)的形式化建模與驗(yàn)證方法研究[D];華東師范大學(xué);2012年

4 李丹;λ噬菌體生活周期的形式化建模與分析[D];上海交通大學(xué);2007年

5 劉密霞;基于策略的信息安全模型及形式化建模的研究[D];蘭州理工大學(xué);2004年

6 周佳銘;基于PVS對SCADE開發(fā)軌交控制系統(tǒng)的形式化建模與驗(yàn)證[D];華東師范大學(xué);2011年

7 濮陽;生物過程的形式化建模及仿真[D];上海交通大學(xué);2007年

8 楊蒙;HMIPv6協(xié)議形式化建模及測試?yán)煞椒ㄑ芯縖D];內(nèi)蒙古大學(xué);2010年

9 韓福榮;基于時(shí)間有色Petri網(wǎng)的聯(lián)鎖軟件的形式化建模與分析[D];同濟(jì)大學(xué);2007年

10 嚴(yán)海星;OAuth協(xié)議的形式化建模與驗(yàn)證[D];華東師范大學(xué);2015年

，

本文編號：1101594