Scyther tools 協議形式化分析幫助文檔翻譯

一、Scyther軟件做者網站的整理

   Scyther工具的網站主頁：https://people.cispa.io/cas.cremers/index.html

  首先 對Scyther軟件的資料進行整理，做者的不少關於Scyther的資料都是公開在本身的官網上的。

  協議使用角色序列做爲參數，而後在體內進行定義：

 

三、對稱角色協議：

  一些對手妥協模型規則，像SKR、LKR （aftercorrect），依靠合做關係。對這種協議在角色和算法上都對稱，（像HMQV），這不是適當的合做關係，使用正確的合做關係，協議須要使用說明做爲一個對稱協議，指導Scyther使用適當的合做。

四、全局聲明

在不少應用中使用全局常量，這包括字符串常量，標籤、或者協議的定義。他們的建模和使用方法以下：

5.7 Miscellaneous 混雜的

5.7.1 Macro  宏定義

  使用宏定義是容許的，是對特殊術語的縮寫，其語法的使用方法以下：

   macro MyShortCut= LargeTerm ;

 像下面這樣的，協議包含了複雜的消息或者重複的元素，宏定義能夠簡化協議的描述（規範）

   

注意的是 宏定義有全局性，能夠處理同層語法層面 ，者容許協議消息的全局縮寫

  

   5.7.2 導入文件

  在一個協議描述中可能導入其餘文件  ，使用  include  導入相關的協議描述文件

   5.7.3 one-role-pre-agent

      操做語義容許代理執行任何角色，甚至是不一樣的角色在同步。這種建模使用在最糟糕的場景中，敵手能夠有不少種利用。可是在具體的設置中代理只執行一個角色，列如服務器和客戶端集不相交，或者RFID標籤和Reads 標籤不相交，在這種狀況下，咱們不考慮領代理能夠執行多個角色的攻擊，能夠經過下面的方式建模

   option "--one-role-per-agent";  //容許代理在多個角色中。   這將引發Scyther 忽略 多個

5.8 輸入語言BNF語法的介紹

     下面給出了所有的輸入語言BNF語法的介紹： 在嚴格的語法定義中，不存在的像這樣的聲稱的術語 (Niagree  或者   Nisynch ),也沒有像以前使用預約義的了預約義的類型 像 Agent ,取而代之的是他們在Scyther工具自身定義常量。  

第六章 創建安全模型  Modeling security  protocols

6.1 Introduction

      使用 Scyther軟件對安全協議進行形式化的安全分析以前必須掌握 基本的符號模型。這些模型在 參考文獻中有有詳細的說明。

      粗略的說，符號分析側重於如下幾個方面：

      邏輯消息組件和協議預期的功能（公共祕鑰和每次生成的或者不變的）

      消息結構（配對，加密、簽名、哈希加密）

     消息流 （順序、涉及到的參加的角色）

6.2 舉例   Needham-Schroeder public key

        正以下面的例子  ， 我麼使用的協議模型 ,

  SCyther使用基於角色描述的協議，最後添加對協議的安全要求，假設沒有這種要求，Scyther不知道檢查什麼項目內容，

   在這咱們會檢查生成和接受的變量的安全性，將會檢查費內射性協議和協議的同步性。

    像上面這樣就完成了發起者的在協議中定義。在這個簡單協議中，響應者角色和發起者角色很是的相似。事實上，僅僅存在一點差異。以下：

    關鍵詞  fresh 和 var 交換了位置，在發起者角色中 ni 是被 I建立，是一個新的生成的值，可是對 響應者 R 角色來書  ni  是一個接受到的值，是一個變量。發送事假和接受事件的聲明也交換位置，聲明使用惟一的標籤，因此在接受事件R中已經改變，在執行聲明的角色是由 I  轉換成 R 。

下面是完整的  Needham-Schroeder protocol 形式化的SPDL描述語言

/*
* Needham-Schroeder protocol
*/
// The protocol description
protocol ns3(I,R)
{
role I
{
fresh ni: Nonce;
var nr: Nonce;
send_1(I,R, {I,ni}pk(R) );
recv_2(R,I, {ni,nr}pk(I) );
claim(I,Running,R,ni,nr);
send_3(I,R, {nr}pk(R) );
claim_i1(I,Secret,ni);
claim_i2(I,Secret,nr);        ////**從左面的安全聲明中能夠看出，claim 能夠在在發送事件和接受事件的聲明中出現
claim_i3(I,Alive);              ///也能夠在事件聲明以後，claim能夠是多個。聲稱安全的
claim_i4(I,Weakagree);
claim_i5(I,Commit,R,ni,nr);
claim_i6(I,Niagree);
claim_i7(I,Nisynch);
}

role R
{
var ni: Nonce;
fresh nr: Nonce;
recv_1(I,R, {I,ni}pk(R) );

claim(R,Running,I,ni,nr);
send_2(R,I, {ni,nr}pk(I) );
recv_3(I,R, {nr}pk(R) );
claim_r1(R,Secret,ni);
claim_r2(R,Secret,nr);
claim_r3(R,Alive);
claim_r4(R,Weakagree);
claim_r5(R,Commit,I,ni,nr);
claim_r6(R,Niagree);
claim_r7(R,Nisynch);
}
} 

7.2.1  指定安全屬性

     爲了說明安全屬性，角色 I 在術語上和角色 R 一致，變量  ni  和  nr ,想下面這樣的插入聲明：

      在角色 I 的結尾，插入一個聲明 claim （I  ，Commit ，R，ni , nr）

      參考的例子能夠 看 ns3.Spdl  整個代碼在  Scyther工具中的描述。正規的輸出能夠看參考文獻4

8.使用  Scyther的 GUI 環境 或者  命令輸出

    Scyher  工具可使用兩種主要的方式，一種是基於圖形的使用GUI ，第二種是使用基於命令的接口，對於大多數用戶來講使用第一種是最佳的選擇，在這節當中咱們詳細的說明使用GUI做爲輸出。

  8.1 輸出結果

    以下面所示，驗證 Needham -Schroeder公鑰協議輸出結果。解釋以下：在 ns3 協議中全部的初始化角色，I 是正確的對一個無界限的運行，不幸的是。全部聲稱響應的角色都是假的，Scyther工具報告發現的至少一個錯誤對四個聲明中的。咱們能夠顯示這些錯誤，在結果輸出的窗口中，Scyther工具爲每一個聲明顯示單獨的一行，每一行又分紅幾列，第一列顯示聲明發生的協議，第二列顯示的是角色，第三列知名協議和標籤，第四例顯示聲明的類型和參數，

8.2  狀態空間綁定

    在驗證過程當中，Scyther工具探索全部可能協議行爲的證據樹，在墓中成都上，默認設置是綁定樹的大小，確保驗證程序的終止，然而，重要的是即便證實書的大小是綁定限制的，可是能夠實現無界限的驗證，在大多數狀況下，驗證程序在達到界限以前返回驗證結果，然而，若是驗證進程到達界限，將會在窗口中顯示以下結果：  NO attacks within bounds   ，這種清空能夠解釋爲Scyther工具沒有發現任何攻擊，由於到達界限，沒有 探索完整個樹，極可能任然存在協議的攻擊。

  默認的界限最大運行次數，或者協議的例子能夠經過主界面的設置改變，若是設置最大運行次數是5 ，這時候Scyther 報告在界限中沒有發現攻擊，這就意味着在涉及運行次數爲5 或者更小的時候沒有攻擊，可是當運行次數爲6或者更多的時候將會 存在攻擊。對於某些協議來講增長運行的次數可能會出現更加完整的結果，可是對於某些協議來講，任然是攻擊次數不會增長的。 注意的是驗證次數的增長必然會致使驗證時間的消耗越大。若是計算機CPU和內存不夠使用會死機。

8.3 攻擊圖輸出

     輸出圖的基本元素是箭頭和幾種方框，圖中的箭頭表示排序約束（是因爲協議角色事件的前綴封閉性引發的，或者取決於入侵者的知識），方框表示運行的建立和運行通訊事件和聲明事件。

8.3.1 運行 （Runs）

   每個垂直軸表明一個運行（協議角色的實例），如此在這個攻擊中咱們能夠看到兩個運行，麼一個運行的開始都是從一個菱形，這表示建立一個運行，並提供有關運行的信息，

  

 對於攻擊左側的運行咱們有以下的信息：（運行 Run 1 ）

能夠看到每個運行都會分配一個運行的標識符，能夠是任意的數字，爲了表示區別不一樣的運行，次運行執行協議中的R 角色，由一個代理名爲 Agent1 的代理執行，認爲正在和代理 Agent2 進行通訊，可是值得注意的是，雖然運行 2 （Run 2）由 Agent2 代理執行，可是這個代理並不認爲他正和Agent1 進行通訊。下面是運行2 的信息 （Run 2）

在運行的右側咱們看到這個運行表明角色的一個實例，從第二行裏能夠看出哪一個代理正在執行，和正在進行通訊的代理，在上圖單位例子中，運行被代理角色 Agent2 代理執行，認爲響應者是不受信任的角色代理 Eve ,

除此以外，運 行的頭部包含新生成的變量和常量信息，（例如 Run 1 中的是 nr#1） ,和有關局部變量實例化的信息。（Run1 使用隨機變量 ni#2 或者 run 2 實例化變量 ni ）         

 

 8.3.2 通訊事件 （Communication event）

  發送事件指明發送一個消息，在運行 2 中（Run 2 ）第一次發送發生在此次攻擊中是第一次發送事件，

每一次消息發送，攻擊者能夠高效的得到，在這種狀況下，由於攻擊者知道代理 Eve的公共祕鑰 sk (Eve)  他能夠解密消息和得到隨機變量的的實例化的值 ni#2

接受事件對應着事件的成功接受，在運行 Run 0 第一次接受事件發生在此次攻擊中是第一次接受到的事件，

着告訴咱們代理執行運行， Agent 1 接受一條信息顯然來自 Agent1 ，接受到的信息是 {Agent#0 ，ni#2}pk(Agent#1)  ,認爲與之通訊的消息 隨機變量 ni#2 被公鑰加密，

傳入箭頭並不表示直接發送消息，相反，它代表約束順序，只有在發生其餘事件以後才能收到此消息，在這個例子中，我麼能夠看到僅僅當 Run 2 發送初始化消息以後才能被接受，緣由是隨機變量的實例化 ni#2 （攻擊者不可以預測這個變量）如此必須等待 直到 Run 2 產生它。

在輸出圖中鏈接箭頭爲紅色並有標籤  「construct」 是由發送事件和接受事件不匹配引發的（沒有接受事件），咱們知道攻擊者只能在發送的消息以後構造要接受的消息，所以必須攻擊者使用本身發送的消息構造消息的接受狀況，其餘可能的狀況包括綠色和黃色的箭頭，黃色的箭頭表示一個消息發送，接受者以徹底相同的形式接受，然而，代理不一樣意任何消息的發送和任意消息的接受，這是由於重定向標籤「redirect」  由於攻擊者必須重定向消息，一個綠色的箭頭表示（不在上面的輸出圖中）收到的和發送的消息是一致的。表示兩個代理之間的正常的通訊關係。

要注意的是，接受事件沒有傳入箭頭表示接受的術語能夠經過攻擊者初始知識生成。列如一個角色閱讀到一個原文信息包括一個代理的名字，攻擊者能夠生成術語根據本身的初始知識。

8.3.3 聲明

第九章  使用Scyther 的命令行工具

 全部的Scyther GUI 工具提供的功能在 命令行工具下都是支持的，除此以外，命令行工具還具備GUI不具備的功能， 

    依靠不一樣的操做系統的平臺，Scyther 目錄包含下面的執行文件

•     Scyther/scyther-linux  
•     Scyther/scyther-w32
•     Scyther/scyther-mac

在下面咱們假設，我麼使用的Linux版本的操做系統，若是你使用的是不一樣的版本，在你的操做系統上替換 下面的Scyther-linux

得到某些命令行的選項的參數列表  使切換  --help  運行可執行文件  ：   Scyther-linux --help

如今分析 NeedHam-Schroeder 協議，生成一個  .dot文件 （輸入語言爲 Graphviz工具）爲攻擊使用 。使用命令：  Scyther-linux --dot-output --output=tls1-attacks.dot TLS_1.spdl

下面使用 Graphviz工具進行輸出結果文件 ：dot -Tpdf -O tls1-attacks.dot 可是執行發現出現dot文件執行錯誤。

根據錯誤提示調試以後，輸出的結果 ，發現輸出的結果並無使用 Graphviz 工具畫出工具圖（這部分緣由以後說明）

 

爲了獲得更加詳細的命令行的選項參數列表 可使用命令：  scysther -linux --expert --help

第十章 高級主題

 10.1  建模多個非對稱祕鑰對

      非對稱祕鑰一般被建模成兩個函數，其中一個函數將代理映射到其公鑰函數，另外一個函數將代理映射到其私鑰。在默認的狀況下沒喲個代理 x 均有一對祕鑰  公鑰/私鑰   (pk(x), sk(x))

建模其餘的非對稱祕鑰，首先定義兩個函數，例如用名字  pk2 表示公鑰函數    ，使用 sk2 表示私鑰函數  ：

   const pk2:   Function ;

   secret sk2: Function ;

咱們也能夠申明 表示非對稱密鑰對錶示方法以下：

 inversekeys (pk2 ,sk2);

若是按照上面的額定義，那麼若是一個術語加密使用 pk2(x)  只能使用 sk2(x)  進行解密。反之亦然。

10.2 近似等式理論

     Scyther工具底層操做語法目前只在語法上考慮對等，當兩個術語相等當且僅當語法上相等的時候，然而，存在幾種常見的加密結構，更加天然的使用肯定的等式。例如：

顯然 Scyther 工具不能爲這種等式理論提供直接的支持，可是存在一種直截了當的近似的方式，核心思想是替代平等術語建模，若是敵手掌握了等價類中的一個元素，咱們提供敵手全部的等價類中的術語。例如，等價類 {k(A,B),   k(B, A)} 咱們提供敵手同 k(A,B),學習 k(B,A) 的能力，反之亦然。 我麼能夠適當的引入幫助器來建模協議  （定義 經過  前綴 @）

 由於角色能夠被任何代理X或者Y 進行實例化，這包括全部的組合代理。上述能夠近似等到完善，一個明顯的實際相關的漏洞是敵手可學習加密的消息，可是不祕鑰，在這種狀況下，咱們任然想模擬等式：

{M}k(A,B)={M}k(B,A)  ，所以咱們調整咱們的幫助協議以下：

 

入股協議包含的非對稱祕鑰術語出如今其餘位置，列如嵌套加密或哈希中，咱們會添加更多的角色，可是在實際中並非常常有效果，咱們可使用輔助協議規則更加緊密的提升性能。經過利用更多協議類型的信息，若是協議傳輸兩種類型的加密消息：

{I , nI, nR }k(I, R)  和   {nI   }k(I, R)   這時候這樣修改輔助協議：

總的來講，手動檢查協議並提取全部的位置，其中來自等價類的術語做爲子項，對於這些位置中的每個，創建一個適當的角色在輔助協議中。這也用來建模，像 Diffe-Hellman 冪，對於冪咱們引入一個抽象的函數符號，列如 exp 和一個公共不變的 常量 g   ，咱們能夠介紹一個輔助協議角色：  exp（exp（g,X）,Y）=exp(exp(g,Y),X)

事實上這種近似類型的證實極其有效。從這一點上講 ，從現實世界上協議全部已知的攻擊均可以使用「real」相等理論來建模。當使用近似相等的時候在Scyther下。

須要注意的是雖然這種近似適用於保密和數據協議，他能夠致使基於消息的洗衣失敗（好比說同步），由於消息等價檢查是語法上的，這種檢查不能影響引入的輔助協議。

10.3 建模時間戳和全局計數器

     Scyther工具底層模型當前不提供代理程序之間共享的變量，每個運行開始都以 clean  slate ,獨立於先前執行的任何運行。換句話說，全局更新狀態不能直接建模。在下面的章節中咱們將提供適當的模型爲常見的問題。

10.3.1 建模全局時間計數器

 使用新生成的值對全局遞增的計數器進行建模，這樣確保每個運行使用不一樣的值，可是這種計數器是粗略的，計數器接受者不能檢查他是技術器先前的值仍是後繼的值。

10.3.2  使用隨機數建模時間戳

 至少存在兩種方式來建模時間戳，第一種模型適用於兩次運行接受給定時間戳值得機率很是接近的協議，當時間戳很高或兩次運行按照順序發生時，可能會發生時間上的延遲。在這種狀況下，能夠將時間戳建模成新生成的值，列如  ; nonces   ,爲了迎合敵手一般知道時間的實事（所以也能夠預測時間戳），咱們將一個發送事件添加到角色，該角色爲對手提供將使用的時間戳的值。咱們在發送 send 前置標籤 ！ T1 爲時間戳 T1 ：

10.3.3 使用變量建模時間戳

 當兩個運行能夠接受相同的時間戳值得時候，第二個模型更適用，這對於粗略的時間戳或一般以高並行性執行的角色（列如服務器角色）是常見的，在這種狀況下，能夠改成將時間戳加密爲由對手肯定的值，與以前的解決方案相比， 這是經過預先接事假完成的

 

10.4 多協議攻擊

     Scyther 工具可使用在多協議攻擊的檢測中，（密切相關的協議使交叉協議攻擊和選擇協議的攻擊）這些攻擊取決於不一樣子協議之間的相互做用，有時候，攻擊者可使用來自一個協議的消息或者消息組件來攻擊另外一個協議，

   最簡單的檢查多協攻擊的方法是結合兩個協議的形式化描述在一個文件中實現，建立一個新的 .spdl 文件 在Scyther 工具下進行檢測，

參考引文：