《OAuth2.0協議安全形式化分析-》----論文摘抄整理

---恢復內容開始---

本篇論文發表在計算機工程與設計，感受寫的仍是頗有水準的。實驗部分交代的比較清楚
本篇論文的創新點： 使用Scyther工具 主要是在 DY模型下面 形式化分析了 OAuth2.0協議的安全性。
首先 OAuth2.0協議定義了四種角色分別是： 資源擁有者、資源服務器、客戶端、受權服務器、
原文指出，根據應用環境的不一樣，OAuth2.0協議定義了四種受權模式： 受權碼模式、簡化模式、客戶端模式、密碼模式。
其次本篇論文知識討論了OAuth2.0的中的受權碼模型，

本論文中做者將認證服務器和資源服務器做爲同一個服務器（方便實驗操做） 。給出了順序圖，形象的展現受權碼模式下各個參數信息的傳遞狀況：

角色中須要定義的是本角色中使用的數據類型，（變量和常量的聲明-------本做者在原文中沒有說明）：從圖中能夠看到 User角色中包括5個事件，

我下面將協議關於受權碼模式的 形式化描述過程 從新寫了一遍

根據做者的解釋以下：在用戶角色描述 User ：------
User ：------ 第一行爲User角色定義，程序在實例化的時候會根據 U角色實例化 User運行實例，角色中首先須要定義的是本角色中使用到的數據類型，就是變量和常量。User 角色中主要包括5個事件，第3行使用用戶和客戶端的共享祕鑰由用戶（user）向客戶端（client）發送數據req ，第4行表示表示使用共享祕鑰加密接受從客戶端到用戶的消息，第5行表示使用共享祕鑰加密客戶端（user）向服務器（server）發送受權碼請求，並向服務器出示必要的參數信息如：已註冊的重定向 uri 、狀態碼等。 第6行表示接受服務器端的受權碼響應，第7行表示受權碼重定向客戶端。
接下來討論安全屬性的問題：

Scyther 定義一對屬性  （Running ,Commit）用來表示謝意雙方對傳輸數據的承認，若是角色 I 承認角色 R的數據  （隨機數 ni  和 nr），則在角色 I 的定義末尾插入語句 Claim （I，Commit， R ，ni, nr）;一樣在 R中send 事件以前插入語句  claim（R，Running，ni ,nr）<p>---恢復內容結束---</p>本篇論文發表在計算機工程與設計，感受寫的仍是頗有水準的。實驗部分交代的比較清楚
本篇論文的創新點：  使用Scyther工具 主要是在  DY模型下面  形式化分析了 OAuth2.0協議的安全性。
  首先 OAuth2.0協議定義了四種角色分別是：    資源擁有者、資源服務器、客戶端、受權服務器、
  原文指出，根據應用環境的不一樣，OAuth2.0協議定義了四種受權模式： 受權碼模式、簡化模式、客戶端模式、密碼模式。
   其次本篇論文知識討論了OAuth2.0的中的受權碼模型，

本論文中做者將認證服務器和資源服務器做爲同一個服務器（方便實驗操做） 。給出了順序圖，形象的展現受權碼模式下各個參數信息的傳遞狀況：

角色中須要定義的是本角色中使用的數據類型，（變量和常量的聲明-------本做者在原文中沒有說明）：從圖中能夠看到 User角色中包括5個事件，

我下面將協議關於受權碼模式的 形式化描述過程 從新寫了一遍

根據做者的解釋以下：在用戶角色描述 User ：------
User ：------ 第一行爲User角色定義，程序在實例化的時候會根據 U角色實例化 User運行實例，角色中首先須要定義的是本角色中使用到的數據類型，就是變量和常量。User 角色中主要包括5個事件，第3行使用用戶和客戶端的共享祕鑰由用戶（user）向客戶端（client）發送數據req ，第4行表示表示使用共享祕鑰加密接受從客戶端到用戶的消息，第5行表示使用共享祕鑰加密客戶端（user）向服務器（server）發送受權碼請求，並向服務器出示必要的參數信息如：已註冊的重定向 uri 、狀態碼等。 第6行表示接受服務器端的受權碼響應，第7行表示受權碼重定向客戶端。
接下來討論安全屬性的問題：

Scyther 定義一對屬性  （Running ,Commit）用來表示謝意雙方對傳輸數據的承認，若是角色 I 承認角色 R的數據  （隨機數 ni  和 nr），則在角色 I 的定義末尾插入語句 Claim （I，Commit， R ，ni, nr）;一樣在 R中send 事件以前插入語句  claim（R，Running，ni ,nr）
 如今對實驗結果解釋：
 經過實驗分析獲得實驗結果，Scyther自己採用的是黑盒的驗證思想，各個角色從本身的角度考慮觀察問題，是否可以知足安全目標和安全屬性，若是安全屬性不知足則可能存在攻擊路徑，（實驗輸出攻擊路徑圖），分別從三個角色出發分析攻擊：‘
 首先是  User 端角色觀察到的攻擊圖。

對上面的如作解釋:-------- 只有User端認爲本身是和攻擊者進行通訊的，User端認爲通訊三方分別是： 角色U 爲本身 ，角色C 爲 Eve（攻擊者），角色S爲 Server；
客戶端 Client 端認爲通訊三方 ：----角色 U爲 Uer ，角色 C 爲本身， 角色 S爲 Server
Server 端認爲 ，角色 U 爲 User， 角色 C 爲 Client， 角色 S爲本身 ，
攻擊者能夠破壞用戶的DNS服務，將信息重定向到惡意的客戶端，而後將信息修改沒發送給正常的客戶端和服務器，一單得到受權碼，能夠將受權碼發送給正常客戶端只是監聽用戶和客戶端的通訊，或者攻擊者能夠將信息修改將受權碼發送給惡意的客戶端，那麼惡意的客戶端就能夠得到用戶的受保護的資源實現資源的竊取。
其次是 Client 端角色觀察攻擊路徑圖以下：

解釋以下： 只有客戶端認爲本身是和攻擊者通訊的，
User端認爲通訊三方爲：角色 U爲本身 ，角色C爲 Client ，角色 S爲 Server
Client端認爲通訊三方 ： 角色U爲 User，同時可能存在另外一個User進程 Eve（攻擊者），角色C爲本身 ，角色S爲 Server
Server 端認爲： 角色U爲User ，角色C爲Client ，角色S爲本身 ，此項攻擊爲中間人攻擊，首先攻擊者監聽到用戶向Client端發送受權碼信息，若是這個通訊信道未受到保護戶，攻擊者將原有的信息截獲、原有的通道阻塞，保證受權碼的有效性，以後攻擊者以User的身份發起另外一個會話，使用監聽到的受權碼嘻嘻獲取資源。
Server端觀察到的攻擊路徑以下：

解釋以下： 只有Server端認爲本身是和攻擊者進行通訊的，
User端認爲通訊三方爲 ：角色 U爲本身 ，角色C爲Client ，角色 S爲Server
Client端認爲通訊三方爲： 角色U爲 User ，角色C爲本身 ，角色S爲Server，
Sever端認爲：角色U爲Eve（攻擊者），角色C爲Client ，角色S爲本身 ， 首先監聽者User發送到Server的受權碼請求消息，而後對信息進行修改，轉發給Server，Server作出受權碼響應，將受權碼轉發給攻擊者Eve。

’