【摘要】：OAuth 2.0協(xié)議是一種開放授權(quán)協(xié)議,主要用于解決用戶賬號(hào)關(guān)聯(lián)與資源共享問題。但是,其弱安全性導(dǎo)致各網(wǎng)絡(luò)公司海量用戶信息泄露,且OAuth 2.0傳輸數(shù)據(jù)采用的https通道效率低下,成為黑客攻擊對(duì)象。提出采用http通道傳輸OAuth 2.0協(xié)議數(shù)據(jù),基于Promale語言及Dolev-Yao攻擊者模型對(duì)OAuth 2.0協(xié)議建模,運(yùn)用SPIN進(jìn)行模型檢測(cè)。形式化分析結(jié)果表明,采用公鑰加密體系對(duì)OAuth 2.0協(xié)議進(jìn)行加密不安全。上述建模方法對(duì)類似的授權(quán)協(xié)議形式化分析有重要借鑒意義。
[Abstract]:OAuth 2.0 protocol is an open authorization protocol, which is mainly used to solve the problem of user account association and resource sharing. However, its weak security results in massive information leakage of users in various network companies, and the https channel used in OAuth 2.0 data transmission is inefficient, so it becomes the target of hacker attack. In this paper, http channel is used to transmit OAuth 2.0 protocol data. Based on Promale language and Dolev-Yao attacker model, OAuth 2.0 protocol is modeled, and SPIN is used for model checking. The results of formal analysis show that using public key encryption system to encrypt OAuth 2.0 protocol is not secure. The above modeling methods can be used for reference for formal analysis of similar authorization protocols.
【作者單位】： 華東交通大學(xué)軟件學(xué)院;
【基金】：國家自然科學(xué)基金資助項(xiàng)目(61163005) 計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室開放課題資助項(xiàng)目(KFKT2012B18) 江西省自然科學(xué)基金資助項(xiàng)目(20132BAB201033) 江西省高校科技落地計(jì)劃項(xiàng)目(KJLD13038) 江西省對(duì)外科技合作技術(shù)資助項(xiàng)目(20151BDH80005) 華東交通大學(xué)研究生創(chuàng)新計(jì)劃資助項(xiàng)目(YC2014-X007)
【分類號(hào)】：TP393.08

【參考文獻(xiàn)】

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

1 楊元原;馬文平;劉維博;;模型檢測(cè)中可變攻擊者模型的構(gòu)造[J];北京郵電大學(xué)學(xué)報(bào);2011年02期

2 李興鋒;張新常;楊美紅;閻保平;;基于SPIN的模塊化模型檢測(cè)方法研究[J];電子與信息學(xué)報(bào);2011年04期

3 XIAO Meihua;MA Chenglin;DENG Chunyan;ZHU Ke;;A Novel Approach to Automatic Security Protocol Analysis Based on Authentication Event Logic[J];Chinese Journal of Electronics;2015年01期

4 胡良文;馬金晶;孫博;;基于Spin的SysML活動(dòng)圖驗(yàn)證框架[J];計(jì)算機(jī)科學(xué)與探索;2014年07期

5 余鵬;魏歐;韓蘭勝;牛耘;;模型檢測(cè)網(wǎng)絡(luò)傳播干預(yù)策略[J];計(jì)算機(jī)科學(xué)與探索;2014年08期

【共引文獻(xiàn)】

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

1 高洪博;李清寶;王煒;朱瑜;;基于敏感位置識(shí)別的狀態(tài)化簡技術(shù)研究[J];電子與信息學(xué)報(bào);2013年03期

2 錢成;燕雪峰;周勇;徐海生;;基于狀態(tài)約簡的順序圖和狀態(tài)圖一致性檢測(cè)[J];計(jì)算機(jī)應(yīng)用研究;2014年05期

3 賀志宏;曾慶凱;;基于SPIN的LTL屬性分解方法研究[J];計(jì)算機(jī)應(yīng)用與軟件;2014年07期

4 肖美華;程道雷;胡磊;;基于Spin/Promela的Woo-Lam協(xié)議安全性質(zhì)高效驗(yàn)證[J];計(jì)算機(jī)與數(shù)字工程;2014年10期

5 肖美華;朱科;馬成林;;基于SPIN的Andrew Secure RPC協(xié)議并行攻擊模型檢測(cè)[J];計(jì)算機(jī)科學(xué);2015年07期

6 顧名宇;;數(shù)理邏輯的程序可靠性驗(yàn)證[J];山東農(nóng)業(yè)大學(xué)學(xué)報(bào)(自然科學(xué)版);2015年04期

7 王曦;徐中偉;;基于啟發(fā)式NDFS的模型檢測(cè)新算法[J];小型微型計(jì)算機(jī)系統(tǒng);2012年08期

相關(guān)博士學(xué)位論文 前3條

1 包力;Web服務(wù)組合形式化建模與驗(yàn)證研究[D];大連海事大學(xué);2009年

2 林英;多核軟件形式化建模、驗(yàn)證及性能評(píng)價(jià)方法研究[D];云南大學(xué);2013年

3 高洪博;指令誘發(fā)型硬件木馬檢測(cè)技術(shù)研究[D];解放軍信息工程大學(xué);2013年

相關(guān)碩士學(xué)位論文 前10條

1 程瑩;網(wǎng)絡(luò)安全協(xié)議的模型檢測(cè)分析及驗(yàn)證系統(tǒng)[D];南昌大學(xué);2010年

2 呂審;NuSMV模型檢測(cè)的研究及應(yīng)用[D];武漢理工大學(xué);2011年

3 李靜;網(wǎng)絡(luò)安全認(rèn)證協(xié)議自動(dòng)分析系統(tǒng)[D];南昌大學(xué);2007年

4 王兵;電子商務(wù)協(xié)議的形式化分析[D];南昌大學(xué);2007年

5 魏小勇;符號(hào)模型檢測(cè)的研究[D];西安理工大學(xué);2008年

6 劉俏威;SPIN模型檢測(cè)的形式化分析機(jī)理研究及應(yīng)用[D];南昌大學(xué);2008年

7 熊昊;模型檢測(cè)形式化分析中若干關(guān)鍵問題研究[D];南昌大學(xué);2008年

8 王勝;基于SystemC的時(shí)態(tài)邏輯屬性驗(yàn)證方法研究[D];北京化工大學(xué);2009年

9 舒良春;基于SPIN/Promela的UML模型驗(yàn)證工具設(shè)計(jì)與實(shí)現(xiàn)[D];南昌大學(xué);2009年

10 安鑫;面向一類基于輪數(shù)的分布式算法的狀態(tài)空間分析與模型檢測(cè)[D];山東大學(xué);2010年

【二級(jí)參考文獻(xiàn)】

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

1 邱慧敏;楊義先;鈕心忻;;無線傳感器網(wǎng)絡(luò)中廣播通信的安全協(xié)議設(shè)計(jì)[J];北京郵電大學(xué)學(xué)報(bào);2006年05期

2 杜杰;江國華;;基于模型檢測(cè)的UML狀態(tài)圖和順序圖一致性檢測(cè)[J];電子科技;2012年02期

3 高曉星;李曉霞;薛冰;;基于UML和SPIN的軟件安全模型驗(yàn)證[J];長沙大學(xué)學(xué)報(bào);2013年05期

4 顏志軍,孫寶文,王天梅;基于UML的業(yè)務(wù)流程模型分析方法研究[J];計(jì)算機(jī)工程與應(yīng)用;2004年29期

5 周春燕;李緒蓉;周良;;UML活動(dòng)圖模型正確性診斷方法[J];計(jì)算機(jī)工程;2011年14期

6 吳翔虎;曲明成;李建中;王志超;;活動(dòng)圖并發(fā)語義代碼自動(dòng)生成算法設(shè)計(jì)[J];哈爾濱工業(yè)大學(xué)學(xué)報(bào);2012年09期

7 王松鋒;熊選東;付建丹;張亮忠;;基于Petri網(wǎng)的SysML活動(dòng)圖的分析與驗(yàn)證[J];計(jì)算機(jī)科學(xué);2012年09期

8 劉軍霞;熊選東;王松鋒;;基于隨機(jī)Petri網(wǎng)的SysML狀態(tài)機(jī)圖的驗(yàn)證[J];計(jì)算機(jī)應(yīng)用與軟件;2013年06期

9 張?bào)?崔哲;張宇淵;;UML和Petri網(wǎng)的建模驗(yàn)證方法[J];火力與指揮控制;2013年10期

10 魏歐;袁泳;蔡昕燁;黃志球;徐丙鳳1;;循環(huán)對(duì)稱化簡及在三值模型上的擴(kuò)展[J];軟件學(xué)報(bào);2011年06期

相關(guān)博士學(xué)位論文 前1條

1 韓蘭勝;計(jì)算機(jī)病毒的傳播模型及其求源問題研究[D];華中科技大學(xué);2006年

相關(guān)碩士學(xué)位論文 前3條

1 單卓為;基于SPIN的UML模型驗(yàn)證技術(shù)的研究[D];西北大學(xué);2008年

2 薛克;基于SPIN的UML活動(dòng)圖驗(yàn)證[D];華東師范大學(xué);2008年

3 張冠女;基于rCOS的SysML形式化研究[D];內(nèi)蒙古大學(xué);2008年

，

本文編號(hào)：2350299