王婷婷+趙松澤

摘 要：本文在OAuth2.0授權(quán)碼模型的基礎(chǔ)上做出改進(jìn)，采用HLPSL語(yǔ)言對(duì)授權(quán)碼模型進(jìn)行形式化建模，建立OAuth2.0協(xié)議授權(quán)碼模型形式化模型，找到授權(quán)碼模型出現(xiàn)安全漏洞的根本原因是客戶端憑證可以被攻擊者竊取。結(jié)合惰性無(wú)限狀態(tài)方法和惰性攻擊者優(yōu)化方法對(duì)形式化模型分析和驗(yàn)證。提出OAuth2.0安全授權(quán)碼模型，并分析和驗(yàn)證其在理論上無(wú)安全漏洞。通過的研究，本文可以提供一套安全的OAuth2.0授權(quán)協(xié)議模型，對(duì)目前安全要求高的開放平臺(tái)的授權(quán)是有指導(dǎo)意義的。

關(guān)鍵詞：OAuth2.0；安全；授權(quán)碼模型；形式化

中圖分類號(hào)：TP309 文獻(xiàn)標(biāo)識(shí)碼：A

1 引言（Introduction）

近些年來(lái)，隨著OAuth2.0協(xié)議的廣泛應(yīng)用，其安全性受到了人們的重點(diǎn)關(guān)注。2012至2014年期間，騰訊、新浪微博、Twitter、Facebook、Google等國(guó)內(nèi)外大量知名網(wǎng)站因使用OAuth授權(quán)的開放平臺(tái)而受到安全威脅，曾數(shù)次緊急公布修復(fù)方案。目前最主流的開放平臺(tái)授權(quán)協(xié)議OAuth的授權(quán)模型的安全性一直受到企業(yè)應(yīng)用者的關(guān)注，實(shí)質(zhì)上是保證不同角色在交互過程中提供安全可信任的服務(wù)。OAuth2.0授權(quán)碼模型是功能最完整、流程最嚴(yán)密的授權(quán)模式，也正因此授權(quán)碼模型被廣泛應(yīng)用，但是頻頻曝出安全漏洞問題。從20世紀(jì)80年代以來(lái)，國(guó)內(nèi)外出現(xiàn)了很多對(duì)安全協(xié)議進(jìn)行形式化分析的方法，根據(jù)方法的性質(zhì)不同，也出現(xiàn)很多不同的分類方法，本文根據(jù)形式化分析方法的表達(dá)能力分將其大致分為基于模型檢測(cè)的安全協(xié)議分析方法、基于模型檢測(cè)的安全協(xié)議分析方法和基于證明的安全協(xié)議分析方法。

OAuth在“客戶端”與“服務(wù)提供商”之間，設(shè)置了一個(gè)授權(quán)層（authorization layer）?！翱蛻舳恕辈荒苤苯拥卿洝胺?wù)提供商”，只能登錄授權(quán)層，以此將用戶與客戶端區(qū)分開來(lái)?！翱蛻舳恕钡卿浭跈?quán)層所用的令牌（token），與用戶的密碼不同。用戶可以在登錄的時(shí)候，指定授權(quán)層令牌的權(quán)限范圍和有效期。“客戶端”登錄授權(quán)層以后，“服務(wù)提供商”根據(jù)令牌的權(quán)限范圍和有效期，向“客戶端”開放用戶儲(chǔ)存的資料。

2 基于模型檢測(cè)的安全協(xié)議形式化分析方法研究（Research on formal analysis method of security protocol based on model detection）

基于模型檢測(cè)的安全協(xié)議分析和驗(yàn)證方法的基本思路是利用有限狀態(tài)機(jī)理論，通過定義狀態(tài)集合及狀態(tài)遷移函數(shù)為安全協(xié)議建立模型；通過窮盡搜索狀態(tài)空間來(lái)判斷一些特殊的狀態(tài)是否可達(dá)，或者是否可以生成一條特殊的狀態(tài)轉(zhuǎn)移路徑，并以此檢測(cè)該模型是否具備期望的安全性質(zhì)。通用的做法是把安全協(xié)議看成一個(gè)分布式系統(tǒng)，單個(gè)主體涉及的協(xié)議執(zhí)行部分稱為局部狀態(tài)，所有局部狀態(tài)構(gòu)成系統(tǒng)的全局狀態(tài)；協(xié)議執(zhí)行過程中，主體收發(fā)消息的動(dòng)作會(huì)引起局部狀態(tài)的改變，進(jìn)而也引起全局狀態(tài)的改變；在安全協(xié)議全局狀態(tài)上定義安全屬性或不變關(guān)系，則安全協(xié)議是否滿足安全目標(biāo)定價(jià)與系統(tǒng)可達(dá)的每個(gè)全局狀態(tài)上安全屬性或不變關(guān)系是否都能得到滿足。

安全協(xié)議的模型檢測(cè)分析方法取得了很大的成功，其優(yōu)點(diǎn)是自動(dòng)化程度高，可以借助自動(dòng)分析工具來(lái)完成分析過程而不需要用戶的參與，并且安全協(xié)議存在缺陷時(shí)能夠自動(dòng)生成相應(yīng)的攻擊實(shí)例。模型檢測(cè)方法是基于Dolev-Yao模型。

本文采用基于模型檢測(cè)的安全協(xié)議形式化分析驗(yàn)證方法，并使用OFMC形式化檢測(cè)工具，OFMC是AVISPA平臺(tái)的主要檢測(cè)工具，也被稱為On-the-Fly模型檢測(cè)器，基于惰性攻擊者思想，結(jié)合兩種分析驗(yàn)證方法來(lái)優(yōu)化和證明協(xié)議的正確性和完整性，第一種是使用惰性數(shù)據(jù)類型建立高效的無(wú)限狀態(tài)空間；第二種是將符號(hào)技術(shù)和惰性Dolev-Yao攻擊者模型最優(yōu)化相結(jié)合的方法。