程道雷，肖美華，劉欣倩，梅映天，李 偉

（華東交通大學軟件學院，江西 南昌330013）

1 引言

OAuth（Open Authorization）［1］作為一種授權(quán)標準，用戶無需將用戶名和密碼等信息提交給第三方應(yīng)用，便能在第三方應(yīng)用中獲取其存儲于其它平臺的私密資源，該標準主要用于解決賬號關(guān)聯(lián)與資源共享問題。OAuth 2.0是OAuth協(xié)議的最新版本，不兼容OAuth 1.0，但降低了OAuth協(xié)議的編碼復雜度，且為各平臺的相關(guān)應(yīng)用提供了對應(yīng)的認證方式。近年來，OAuth 2.0協(xié)議的安全性漏洞引發(fā)了許多互聯(lián)網(wǎng)安全問題，包括CSDN、facebook、亞馬遜、新浪微博在內(nèi)的眾多著名網(wǎng)站遭受黑客攻擊。因此，OAuth 2.0協(xié)議形式化分析與驗證具有重要社會價值。

Pai S等［2］運用Alloy框架對OAuth 2.0進行形式化分析；Sun San－Tsai［3］通過利用基于OAuth 2.0的單點登錄系統(tǒng)的實例表明OAuth 2.0雖然內(nèi)容簡單，但不安全；陳偉等［4］運用“數(shù)字簽名技術(shù)”對OAuth 2.0進行改進，并基于Blanchet演算對其進行安全性分析；王煥孝等［5］運用協(xié)議分析工具SATMC，得出OAuth 2.0協(xié)議在失去https通道保護下的危險狀態(tài)。由于OAuth 2.0協(xié)議當前依賴https 通道傳輸相關(guān)數(shù)據(jù)，而https 要運行SSL（Secure Sockets Layer）對傳輸數(shù)據(jù)加密，降低了https傳輸效率。根據(jù)相關(guān)調(diào)查研究，在北上廣深以外的中國廣大城市，有20%～25% 的用戶都會遇到https連接困難，排查發(fā)現(xiàn)問題和接入點無關(guān)，信號和網(wǎng)絡(luò)不穩(wěn)定導致https 請求很難完成，導致一旦遭遇ARP（Address Resolution Protocol）攻擊或中間人攻擊，用戶信息將遭竊取或破壞。本文提出使OAuth 2.0脫離https通道，通過“http＋消息加密”的方式傳輸數(shù)據(jù)，并將公鑰密鑰體系運用到該協(xié)議上，使用模型檢測技術(shù)對協(xié)議進行安全性驗證。

形式化方法主要包括模型檢測（Model Checking）［6］與 定 理 證 明［7］兩 個 分 支。SPIN（Simple Promela INterpreter）［8，9］是 一 種 著 名 的 協(xié) 議 模 型檢測驗 證 工 具。Maggi P 等［10］以Ndddam－Schroeder協(xié)議為實例，基于Dolev－Yao攻擊模型［11］的思想，提出一種用于安全協(xié)議模型檢測的建模方法。本文對該方法進行擴展，運用到包含多主體的授權(quán)協(xié)議的模型檢測上。

由于OAuth 2.0 是一個嶄新的授權(quán)協(xié)議，可供參考的運用形式化方法對該協(xié)議安全性驗證研究成果仍然不足，本文探索使用模型檢測技術(shù)對OAuth 2.0協(xié)議進行形式化分析與驗證。首先，將OAuth 2.0協(xié)議進行簡化，并用形式化方法對其進行描述，再運用公鑰加密體系對協(xié)議進行加密，在對OAuth 2.0協(xié)議進行建模后，驗證該協(xié)議是否能安全用在消息傳輸中，模型檢測實驗發(fā)現(xiàn)了中間人攻擊序列圖，因此得出公鑰加密體系不能夠保證OAuth 2.0協(xié)議安全的方法。

本文結(jié)構(gòu)安排如下：第2 節(jié)對OAuth 2.0 協(xié)議進行簡化及形式化表示，并運用公鑰密碼體系對協(xié)議加密；第3節(jié)闡述了OAuth 2.0 協(xié)議建模過程；第4節(jié)運用SPIN 對OAuth 2.0協(xié)議進行驗證與分析；第5節(jié)為結(jié)束語。

2 OAuth 2.0協(xié)議及形式化表示

OAuth是一種第三方授權(quán)協(xié)議。首先，客戶端發(fā)送Authorization Request（授權(quán)申請），向Resource Owner（資源擁有者）申請Access Grant（訪問授權(quán)）；然后，使用Access Grant和Client Credentials（身份證書）與Authorization Server（授權(quán)服務(wù)器）交換Access Token（訪問令牌，包含持續(xù)時間、作用范圍等信息），最后客戶端提交Access Token至Resource Owner（資源擁有者）獲取受保護資源。具體過程如圖1所示。

Figure 1 Flow of the abstract protocol圖1 抽象協(xié)議流程

根據(jù)圖1所示的協(xié)議流程，將OAuth 2.0 協(xié)議進行形式化表示，獲得如下協(xié)議：

（1）Client→Resource Owner：Authorization Request；

（2）Resource Owner→Client：Access Grant；

（3）Client→Authorization Server：Access Grant，Client Credentials；

（4）Authorization Server→Client：Access Token；

（5）Client→Resource Server：Access Token；

（6）Resource Server→Client：Protected Resource。

如果將以上協(xié)議中未加密的消息直接通過http通道傳輸數(shù)據(jù)，所有的信息都將被攻擊者輕而易舉截獲。因此，將OAuth 2.0 協(xié)議簡化，并用公鑰加密體系對消息進行加密，得到如下OAuth 2.0協(xié)議：

（1）C→RO：｛A＿r｝PKRO；

（2）RO→C：｛A＿g｝PKC；

（3）C→AS：｛A＿g，C＿c｝PKAS；

（4）AS→C：｛A＿t｝PKC；

（5）C→RS：｛A＿t｝PKRS；

（6）RS→C：｛P＿r｝PKC。

其中，PKC表示以C的公鑰加密，任意經(jīng)C的公鑰加密的消息，只有C才能通過其私鑰解開，其它主體類似。本文將運用模型檢測技術(shù)對以上協(xié)議進行驗證分析。

3 OAuth 2.0 協(xié)議建模

將OAuth 2.0 協(xié)議建模分為誠實主體建模和攻擊者建模兩個部分，其中，攻擊者建模以Dolev－Yao攻擊者模型為指導理論。

3.1 誠實主體建模

OAuth 2.0 協(xié)議的誠實主體包括Client、Resource Owner、Authorization Server 和Resource Server。結(jié)合Promela語言性質(zhì)，我們分別為四個誠實主體定義各自的進程，依次命名為proctypePC（）、proctypePRO（）、proctypePAS（）和proctypePRS（）。由于誠實主體進程的定義方法非常類似，本文將以proctypePC（）的定義過程為例進行闡述。

本文所研究的內(nèi)容為檢測協(xié)議本身存在的漏洞，因此首先需要對模型做出如下幾點假設(shè)：

（1）公鑰加密算法本身沒有漏洞；

（2）只有對應(yīng)的密鑰才能解密加密消息；

（3）攻擊者可以是任何主體。

由于攻擊者建模遵循Dolev－Yao攻擊模型，因此誠實主體發(fā)送的所有消息都將被攻擊者截獲，而誠實主體所接收的消息，也全部由攻擊者根據(jù)已有的知識組合生成或者直接轉(zhuǎn)發(fā)截獲的消息。依據(jù)該思想，建模過程需要借助Promela語言中的通道（chan）這一數(shù)據(jù)結(jié)構(gòu)。將協(xié)議中傳輸?shù)南⒏鶕?jù)數(shù)據(jù)項的數(shù)目進行分類，同一類的消息使用同一個通道進行傳輸，因此，OAuth 2.0數(shù)據(jù)傳輸模擬需要兩個參數(shù)不同的通道，將其進行如下定義：

chanca＝［0］of｛mtype，mtype，mtype｝

chancb＝［0］of ｛mtype，mtype，mtype，mtype｝

其中，協(xié)議中的消息（1）、（2）、（4）、（5）、（6）通過通道ca傳輸，消息（3）通過通道cb傳輸。值得注意的是ca和cb所定義的單位元素個數(shù)都比所需表示的消息元素多一項，這是因為通道中需要預留一個元素應(yīng)對會話過程中的優(yōu)化需要。具體原因如下：由于本文所要構(gòu)建的是一個并發(fā)系統(tǒng)，因此各進程之間的交叉運行所產(chǎn)生的狀態(tài)遷移量將非常龐大，甚至足以導致狀態(tài)爆炸［12～15］，為了減少狀態(tài)遷移的數(shù)量，在建模過程中，以ca為例，對通道作如下定義：發(fā)送語句ca！x1，x2，x3 中，x1 為消息接收者，x2是知識項，x3 是對x2 進行加密的公鑰。接收語句ca？eval（x1），x2，eval（x3）中，eval函數(shù)被用作判斷知識項是否與預期一致，從左到右依次判斷，如果某處不一致，直接拒絕接收該消息。但是，攻擊者需要截獲所有誠實主體發(fā)送的消息，因此不需要通過eval來判斷消息發(fā)送方，可直接定義為ca？＿，x1，x2。如此，可以減少大量無效消息。對Client的建模，具體如以下proctypePC（）的詳細代碼所示：

在PC進程中，self表 示 消 息 發(fā) 起 者，party1、party2、party3為消息接收者，g1和g2為泛型變量，用作表示主體C接收到的消息中的未知數(shù)據(jù)項。atomic為Promela語言中用來定義原子序列的語法規(guī)則，旨在減少進程交叉運行的次數(shù)，達到優(yōu)化系統(tǒng)的目的。init＿start＿C＿RO、init＿commit＿C＿RO、init＿start＿C＿AS、init＿commit＿C＿AS和init＿start＿C＿RS為模型程序中定義的宏，被用來更新記錄原子謂詞的變量的值，這些原子謂詞被用來表示協(xié)議性質(zhì)。如果主體C發(fā)起對主體RO的協(xié)議會話，表示主體C參與了主體RO運行的協(xié)議。如果主體C完成了與主體RO的會話，則表明主體C提交了與主體RO的會話。根據(jù)以上原理，模型的每一條性質(zhì)都需要用一個全局的Promela布爾變量表示，它們將在協(xié)議運行的特定階段為真。通過對協(xié)議的分析，定義了如下原子謂詞變量：

為了將模型中的所有性質(zhì)運用到SPIN 工具的仿真過程中，本文將協(xié)議性質(zhì)用LTL（線性時態(tài)邏輯）［16，17］刻畫如下：

［］（（［］！commitCRO）‖（！commitCRO∪startROC））

［］（（［］！startCAS）‖（！startCAS∪commitCRO））

［］（（［］！commitCAS）‖（！commitCAS∪startASC））

［］（（［］！startCRS）‖（！startCRS∪commitCAS））

［］（（［］！commitCRS）‖（！commitCRS∪startRSC））

根據(jù)相同的規(guī)則，類似地定義主體RO的進程PRO和主體AS的進程PAS以及主體RS的進程PRS。

除定義好誠實主體進程之外，還要對初始進程作如下定義：

主體C作為整個協(xié)議的發(fā)起者，在協(xié)議模型中，他有可能向任意主體發(fā)起協(xié)議，如主體RO和主體HACKER。

3.2 攻擊者建模

攻擊者建模中，攻擊者知識庫創(chuàng)建最為關(guān)鍵，其主要由兩部分知識項構(gòu)成：第一部分為攻擊者本身的初始知識庫；另一部分知識項學習方法如下：攻擊者每攔截到一條新消息后，便將學到的知識添加到知識庫中。其添加方式分為兩種：如截獲的消息未經(jīng)加密，則可直接獲取其所有知識項并添加入庫；如截獲的消息已加密或者部分加密，則未經(jīng)加密部分或者可以解密部分，直接或者解密后添加入庫，如無法解密，將整個密文部分存入知識庫中，以備需要時提取使用。

為簡化知識項表示，攻擊者知識項表示須遵循以下兩點原則：（1）不表示攻擊者不可能學會的知識項；（2）不表示誠實主體拒絕接受的消息（通過類型檢查的方式判斷）?；谝陨蟽牲c，可以計算出需要表示的攻擊者知識，如圖2所示，攻擊者潛在能學會的知識和攻擊者需要學會的知識的交集為攻擊者模型需要表示的知識。

Figure 2 Schematic of the attacker acquiring the knowledge which need to be indicated圖2 攻擊者模型中需要表示的知識項求解示意圖

首先求解攻擊者可以學會的知識。因為攻擊者可以學會的知識，都是通過截獲誠實主體發(fā)送的消息并對其進行相應(yīng)處理所得，故可通過對誠實主體的發(fā)送消息語句進行分析，獲得所需知識。攻擊者 初 始 知 識 庫 為 ｛C，RO，AS，RS，H，gD，R，PKH，PKRO，PKRS，PKAS，PKC｝，變量g1～g5的取值范圍為｛C，RO，AS，RS，H，gD，PKH，PKRO，PKRS，PKAS，PKC｝，因此，可獲得如表1所示的攻擊者可學會的知識。

Table 1 Knowledge elements that the intruder can acquire表1 攻擊者可學會的知識

接下來需要求解的是攻擊者需學會的知識項。攻擊者需要學會的知識，就是組成攻擊者發(fā)送給誠實主體的消息的知識項。故可通過對誠實主體的接收消息語句進行分析，根據(jù)變量的不同取值，組合得到如表2所示的攻擊者需要學會的知識。

Table 2 Knowledge elements the intruder needs表2 攻擊者需要學會的知識項

由表1和表2的第2列求交集，可得到攻擊者模型中需要表示的知識項，具體如圖3所示。

Figure 3 Knowledge elements that need to be indicated in the attacker model圖3 攻擊者模型中需要表示的知識項

根據(jù)以上的研究基礎(chǔ)與理論，編寫攻擊者模型代碼，框架如下所示：

在Windows 7 64位系統(tǒng)、Cygwin 2.510.2.2以及SPIN 5.2.0構(gòu)建的環(huán)境下進行仿真實驗，發(fā)現(xiàn)了如圖4所示的OAuth 2.0協(xié)議的中間人攻擊序列。

Figure 4 Attack sequence diagram圖4 攻擊序列圖

4 實驗結(jié)果與分析

使用SPIN 工具，對上述模型進行驗證，獲得了如圖4所示的攻擊序列，并得到如下攻擊過程：

（1）C→HACKER： ｛A＿r｝PKHACKER；HACKER→RO：｛A＿r｝PKRO；

（2）RO→HACKER：｛A＿g｝PKC；HACKER→C：｛A＿g｝PKC；

（3）C→HACKER： ｛A＿g，C＿c｝PKAS；HACKER→AS：｛A＿g，C＿c｝PKAS；

（4）AS→HACKER：｛A＿t｝PKC；HACKER→C：｛A＿t｝PKC；

（5）C→HACKER： ｛A＿t｝PKHACKER；HACKER→RS：｛A＿t｝PKRS；

（6）RS→HACKER： ｛P＿r｝PKHACKER；HACKER→C：｛P＿r｝PKC。

協(xié)議運行的第（6）步，資源服務(wù)器將受保護資源加密發(fā)送出來后，被攻擊者截獲后利用自己的私鑰解密，從而竊取受保護資源，而C 并不知道自己接收到的消息實際是HACKER 轉(zhuǎn)發(fā)而來的。

5 結(jié)束語

OAuth 2.0協(xié)議關(guān)系到用戶賬號、密碼等個人隱私信息，與人們生活息息相關(guān)。本文提出使用http通道對OAuth 2.0協(xié)議數(shù)據(jù)進行傳輸，運用模型檢測技術(shù)，通過Promela語言以及SPIN 工具對經(jīng)公鑰體系加密的OAuth 2.0協(xié)議運行過程進行仿真，發(fā)現(xiàn)一條中間人攻擊路徑。仿真結(jié)果表明，利用公鑰加密體系對OAuth 2.0協(xié)議加密并不安全。下一步工作將嘗試利用私鑰體系對OAuth 2.0進行加密改進，并對其安全性進行驗證。

［1］ Hardt D.The OAuth 2.0authorization framework（draft－ietfoatuth－v2－31）［EB/OL］.［2012－08－01］.https：//tools.ietf.org/id/draft－ieft.org/id/draft－ietf－oauth－v2－31.html.

［2］ Pai S，Sharma Y，Kumar S，et al.Formal verification of OAuth 2.0using Alloy framework［C］∥Proc of 2011International Conference on Communication Systems and Network Technologies（CSNT），2011：655－659.

［3］ Sun San－Tsai.Simple but not secure：An empirical security analysis of OAuth2.0－based single sign－on systems［D］.Vancouver：University of British Columbia，2012.

［4］ Chen Wei，Yang Yi－tong，Niu Le－yuan.Improved OAuth2.0 protocol and analysis of its security［J］.Computer Systems＆Applications，2014，23（3）：25－30.（in Chinese）

［5］ Wang Huan－xiao，Gu Chun－xiang，Zheng Yong－h(huán)ui.Formal security analysis of OAuth 2.0authorization protocol［J］.Journal of Information Engineering University，2014，15（2）：141－147.（in Chinese）

［6］ Yu Peng，Wei Ou，Han Lan－sheng，et al.Model checking network transmission intervention policies［J］.Journal of Frontiers of Computer Science and Technology，2014，8（8）：906－918.（in Chinese）

［7］ Xiao M H，Ma C L，Deng C Y，et al.A novel approach to automatic security protocol analysis based on authentication event logic［J］.Chinese Journal of Electronics，2014，23（2）：235－241.

［8］ Holzmann G J.The model checker SPIN［J］.IEEE Transactions on Software Engineering，1997，23（5）：279－295.

［9］ Hu Liang－wen，Ma Jin－jing，Sun Bo.SPIN－based verification framework for SysML activity diagram［J］.Journal of Frontiers of Computer Science and Technology，2014，8（7）：836－847.（in Chinese）

［10］ Maggi P，Sisto R.Using SPIN to verify security properties of cryptographic protocols［C］∥Proc of the 9th International SPIN Workshop Grenoble，2002：187－204.

［11］ Dolev D，Yao A C.On the security of public key protocols［J］.IEEE Transactions on Information Theory，1983，29（2）：198－208.

［12］ Hou Gang，Zhou Kuan－jiu，Yong Jia－wei，et al.Survey of state explosion problem in model checking［J］.Computer Science，2013，40（z1）：77－85.（in Chinese）

［13］ Jamal B，Mohamed El－M，Hongyang Q，et al.Communicative commitments：Model checking and complexity analysis［J］.Knowledge－Based Systems，2012，35：21－34.

［14］ Yang Yuan－yuan，Ma Wen－ping，Liu Wei－bo.The construction of changeable intruder model in model checking［J］.Journal of Beijing University of Posts and Telecommunications，2011，34（2）：54－57.（in Chinese）

［15］ Li Xing－feng，Zhang Xin－chang，Yang Mei－h(huán)ong，et al.Study on modularized model checking method based on SPIN［J］.Journal of Electronics ＆Information Technology，2011，33（4）：902－907.（in Chinese）

［16］ Xiao Mei－h(huán)ua，Xue Jin－yun.Formal description of properties of concurrency system by temporal logic［J］.Journal of Naval University of Engineering，2004，16（5）：10－13.（in Chinese）

［17］ Salamah S，Ochoa O，Jacquez Y.Using pairwise testing to verify automatically－generated formal specifications［C］∥Proc of 2015IEEE 16th International Symposium on High Assurance Systems Engineering（HASE），2015：279－280.

附中文參考文獻：

［4］ 陳偉，楊伊彤，牛樂園.改進的OAuth2.0協(xié)議及其安全性分析［J］.計算機系統(tǒng)應(yīng)用，2014，23（3）：25－30.

［5］ 王煥孝，顧純祥，鄭永輝.開放授權(quán)協(xié)議OAuth2.0的安全性形式化分析［J］.信息工程大學報，2014，15（2）：141－147.

［6］ 余鵬，魏歐，韓蘭勝，等.模型檢測網(wǎng)絡(luò)傳播干預策略［J］.計算機科學與探索，2014，8（8）：906－918.

［9］ 胡良文，馬金晶，孫博.基于SPIN 的SysML 活動圖驗證框架［J］.計算機科學與探索，2014，8（7）：836－847.

［12］ 侯剛，周寬久，勇嘉偉，等.模型檢測中狀態(tài)爆炸問題研究綜述［J］.計算機科學，2013，40（z1）：77－85.

［14］ 楊元原，馬文平，劉維博.模型檢測中可變攻擊者模型的構(gòu)造［J］.北京郵電大學學報，2011，34（2）：54－57.

［15］ 李興鋒，張新常，楊美紅，等.基于SPIN 的模塊化模型檢測方法研究［J］.電子與信息學報，2011，33（4）：902－907.

［16］ 肖美華，薛錦云.時態(tài)邏輯形式化描述并發(fā)系統(tǒng)性質(zhì)［J］.海軍工程大學學報，2004，16（5）：10－13.