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

王婷婷+趙松澤

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

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

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

1 引言（Introduction）

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

OAuth在“客戶端”與“服務提供商”之間，設置了一個授權層（authorization layer）?！翱蛻舳恕辈荒苤苯拥卿洝胺仗峁┥獭?，只能登錄授權層，以此將用戶與客戶端區分開來。“客戶端”登錄授權層所用的令牌（token），與用戶的密碼不同。用戶可以在登錄的時候，指定授權層令牌的權限范圍和有效期。“客戶端”登錄授權層以后，“服務提供商”根據令牌的權限范圍和有效期，向“客戶端”開放用戶儲存的資料。

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

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

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

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