基于OAuth2.0協(xié)議的安全授權模型研究

王婷婷+趙松澤

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

關鍵詞：OAuth2.0；安全；授權碼模型；形式化

中圖分類號：TP309 文獻標識碼：A

1 引言（Introduction）

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

OAuth在“客戶端”與“服務提供商”之間，設置了一個授權層（authorization layer）?！翱蛻舳恕辈荒苤苯拥卿洝胺仗峁┥獭保荒艿卿浭跈鄬?，以此將用戶與客戶端區(qū)分開來?！翱蛻舳恕钡卿浭跈鄬铀玫牧钆疲╰oken），與用戶的密碼不同。用戶可以在登錄的時候，指定授權層令牌的權限范圍和有效期?！翱蛻舳恕钡卿浭跈鄬右院?，“服務提供商”根據(jù)令牌的權限范圍和有效期，向“客戶端”開放用戶儲存的資料。

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

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

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

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