運用SPIN對開放授權(quán)協(xié)議OAuth 2.0的分析與驗證
[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é)基金資助項目(61163005) 計算機軟件新技術(shù)國家重點實驗室開放課題資助項目(KFKT2012B18) 江西省自然科學(xué)基金資助項目(20132BAB201033) 江西省高?萍悸涞赜媱濏椖(KJLD13038) 江西省對外科技合作技術(shù)資助項目(20151BDH80005) 華東交通大學(xué)研究生創(chuàng)新計劃資助項目(YC2014-X007)
【分類號】:TP393.08
【參考文獻(xiàn)】
相關(guān)期刊論文 前5條
1 楊元原;馬文平;劉維博;;模型檢測中可變攻擊者模型的構(gòu)造[J];北京郵電大學(xué)學(xué)報;2011年02期
2 李興鋒;張新常;楊美紅;閻保平;;基于SPIN的模塊化模型檢測方法研究[J];電子與信息學(xué)報;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活動圖驗證框架[J];計算機科學(xué)與探索;2014年07期
5 余鵬;魏歐;韓蘭勝;牛耘;;模型檢測網(wǎng)絡(luò)傳播干預(yù)策略[J];計算機科學(xué)與探索;2014年08期
【共引文獻(xiàn)】
相關(guān)期刊論文 前7條
1 高洪博;李清寶;王煒;朱瑜;;基于敏感位置識別的狀態(tài)化簡技術(shù)研究[J];電子與信息學(xué)報;2013年03期
2 錢成;燕雪峰;周勇;徐海生;;基于狀態(tài)約簡的順序圖和狀態(tài)圖一致性檢測[J];計算機應(yīng)用研究;2014年05期
3 賀志宏;曾慶凱;;基于SPIN的LTL屬性分解方法研究[J];計算機應(yīng)用與軟件;2014年07期
4 肖美華;程道雷;胡磊;;基于Spin/Promela的Woo-Lam協(xié)議安全性質(zhì)高效驗證[J];計算機與數(shù)字工程;2014年10期
5 肖美華;朱科;馬成林;;基于SPIN的Andrew Secure RPC協(xié)議并行攻擊模型檢測[J];計算機科學(xué);2015年07期
6 顧名宇;;數(shù)理邏輯的程序可靠性驗證[J];山東農(nóng)業(yè)大學(xué)學(xué)報(自然科學(xué)版);2015年04期
7 王曦;徐中偉;;基于啟發(fā)式NDFS的模型檢測新算法[J];小型微型計算機系統(tǒng);2012年08期
相關(guān)博士學(xué)位論文 前3條
1 包力;Web服務(wù)組合形式化建模與驗證研究[D];大連海事大學(xué);2009年
2 林英;多核軟件形式化建模、驗證及性能評價方法研究[D];云南大學(xué);2013年
3 高洪博;指令誘發(fā)型硬件木馬檢測技術(shù)研究[D];解放軍信息工程大學(xué);2013年
相關(guān)碩士學(xué)位論文 前10條
1 程瑩;網(wǎng)絡(luò)安全協(xié)議的模型檢測分析及驗證系統(tǒng)[D];南昌大學(xué);2010年
2 呂審;NuSMV模型檢測的研究及應(yīng)用[D];武漢理工大學(xué);2011年
3 李靜;網(wǎng)絡(luò)安全認(rèn)證協(xié)議自動分析系統(tǒng)[D];南昌大學(xué);2007年
4 王兵;電子商務(wù)協(xié)議的形式化分析[D];南昌大學(xué);2007年
5 魏小勇;符號模型檢測的研究[D];西安理工大學(xué);2008年
6 劉俏威;SPIN模型檢測的形式化分析機理研究及應(yīng)用[D];南昌大學(xué);2008年
7 熊昊;模型檢測形式化分析中若干關(guān)鍵問題研究[D];南昌大學(xué);2008年
8 王勝;基于SystemC的時態(tài)邏輯屬性驗證方法研究[D];北京化工大學(xué);2009年
9 舒良春;基于SPIN/Promela的UML模型驗證工具設(shè)計與實現(xiàn)[D];南昌大學(xué);2009年
10 安鑫;面向一類基于輪數(shù)的分布式算法的狀態(tài)空間分析與模型檢測[D];山東大學(xué);2010年
【二級參考文獻(xiàn)】
相關(guān)期刊論文 前10條
1 邱慧敏;楊義先;鈕心忻;;無線傳感器網(wǎng)絡(luò)中廣播通信的安全協(xié)議設(shè)計[J];北京郵電大學(xué)學(xué)報;2006年05期
2 杜杰;江國華;;基于模型檢測的UML狀態(tài)圖和順序圖一致性檢測[J];電子科技;2012年02期
3 高曉星;李曉霞;薛冰;;基于UML和SPIN的軟件安全模型驗證[J];長沙大學(xué)學(xué)報;2013年05期
4 顏志軍,孫寶文,王天梅;基于UML的業(yè)務(wù)流程模型分析方法研究[J];計算機工程與應(yīng)用;2004年29期
5 周春燕;李緒蓉;周良;;UML活動圖模型正確性診斷方法[J];計算機工程;2011年14期
6 吳翔虎;曲明成;李建中;王志超;;活動圖并發(fā)語義代碼自動生成算法設(shè)計[J];哈爾濱工業(yè)大學(xué)學(xué)報;2012年09期
7 王松鋒;熊選東;付建丹;張亮忠;;基于Petri網(wǎng)的SysML活動圖的分析與驗證[J];計算機科學(xué);2012年09期
8 劉軍霞;熊選東;王松鋒;;基于隨機Petri網(wǎng)的SysML狀態(tài)機圖的驗證[J];計算機應(yīng)用與軟件;2013年06期
9 張筠;崔哲;張宇淵;;UML和Petri網(wǎng)的建模驗證方法[J];火力與指揮控制;2013年10期
10 魏歐;袁泳;蔡昕燁;黃志球;徐丙鳳1;;循環(huán)對稱化簡及在三值模型上的擴(kuò)展[J];軟件學(xué)報;2011年06期
相關(guān)博士學(xué)位論文 前1條
1 韓蘭勝;計算機病毒的傳播模型及其求源問題研究[D];華中科技大學(xué);2006年
相關(guān)碩士學(xué)位論文 前3條
1 單卓為;基于SPIN的UML模型驗證技術(shù)的研究[D];西北大學(xué);2008年
2 薛克;基于SPIN的UML活動圖驗證[D];華東師范大學(xué);2008年
3 張冠女;基于rCOS的SysML形式化研究[D];內(nèi)蒙古大學(xué);2008年
,本文編號:2350299
本文鏈接:http://www.sikaile.net/guanlilunwen/ydhl/2350299.html