Scyther-Semantics and verification of Security Protocol

 1 、本書前一節主要是介做者本身的平生經歷（讀完感受做者是個神童），目標明確做者13歲代碼已經寫的很溜了。本身也開了網絡公司，可是後面又專一於本身的計算機基礎理論，修了哲學的博士學位（不得不說不少專業的交叉真的能夠創造新的起點），可是任何領域的開闢都是來自本身任勞任怨的決心和堅韌不拔的毅力。

   原本以前一直是在看滲透測試的方面資料，可是後面加上實習的事，論文View「」被「」選擇成工業網絡協議的形式化分析，沒有人指導該怎麼去作，迷茫應該往哪一個方向上分析，先是對EtherNet/IP 協議ODVA發佈的規範文檔的閱讀，（剛開始看的的時候感受看不到頭，沒有本身指望的相關資料或者越看越複雜）就好像一棵藤，本身獨自摸索着向前，每個枝節會有新的問題或者概念蹦出，而後在返回去找相關的資料。（這種狀況像是疊羅漢），可是這中間我感受本身走了不少彎路（磕磕碰碰），由於急切的想要找到指望的，切中要點的idea ，這樣我就不少時候半途而廢（太摧殘），就像漫畫上一我的挖井，挖到通常看不到但願就放棄另尋錨點挖。有個以前尋求幫助的博士說「你四處詢問的所須要的東西每每就在你眼前」因此真的要靜下心來，堅持下去。就是以爲本身在計算機方面的能力真的有待提升，因此尷尬的近況就是真的懼怕本身作不出來，如今還有論文方面還存在兩個困難。

        一是EtherNet/IP協議中應用層CIP協議中使用的安全傳輸機制TLS協議和DTLS協議自身的問題（TLS1.3版本已經更新，可是ODVA中的支持的芯片將來3-6年才能更新支持），若是對EtherNet/IP協議形式化分析，拿現有的TLS1.2做爲分析，仍是使用TLS1.3,1.3的版本在協議內容上存在較大的改變。可是若是使用TLS1.3作形式化分析，自己CIP中的全部密碼套件不支持，在回溯到EtherNet/IP 協議的自身安全的時候就會沒法進行下去。考慮到此因此對CIP協議分析的採用目前使用的TLS1.2版本，分析完以後對其中的漏洞和安全問題以及攻擊路徑作整理回溯到CIP安全，在回溯到EtherNet/IP協議的安全，這裏加上比較TLS1.2和TLS1.3存在的差別，（後面擴展視時間而定）。

      二是Scyther 形式化分析工具的手冊和語義分析的資料書目前仍是沒有看懂，Scyther user manual 已經看完，可是因爲裏面的內容是基於Scyther-Semantics and verification of Security Protocol 的，因此必須先吃透這本書的內容。

     如今第一個問題具體部署完成，預計週末完成比較和分析的梳理。如今對第二個問題進行分篇章的整理。

二、Scyther-Semantics and verification of Security Protocol（整理）

     內容：

  第一節：Dolev-Yao模型 （假設基礎， 要分析的密碼算法是完美的，消息是抽象的術語，網絡徹底可由入侵者控制）

   安全模型的術語定義： 首先安全協議區分了不少行爲，每一個這樣的協議行爲成爲角色，

   協議規範描述了協議中的每一個角色的行爲，將協議規範視爲語義的參數，定義抽象的語法制定安全協議，將安全協議中的角色指定爲一系列的事件，挑戰響應機制（一般成爲Nonce 隨機數）或者會話祕鑰，在整個協議中有重要的做用，按照協議提出一個抽象的語法和靜態要求，代理模型：代理執行協議的角色，能夠並行執行屢次，是封閉的假設（誠實的代理不會對外泄露分類消息），代理模型描述瞭如何解釋角色的運行，代理按照順序執行角色的描述，等待讀取時間，

通訊模型：通訊模型描述了消息之間的關係代理商的交換，咱們選擇異步模型通信。使用緩衝區（暫）

威脅模型： 參見 Dolev-Yao

密碼 原語： 密碼原語是理想化的數學結構，例如加密，在對加密原語的處理中，使用了所謂黑盒測試，只是知道密碼算法的相關屬性，只考慮非對稱和對稱算法，而且假設要分析的協議使完美的。

 本章使用NS協議（Needham-Scroeder）,使用消息序列圖（MSC）來講明安全協議的攻擊：   首先 發起者 i  擁有公鑰pk(r)和私鑰sk(i) ,同時接受者也一樣擁有公鑰pk(i)和私鑰sk(r) ,發起者向接受者發送個個隨機變量 ni 同時加上本身的身份 i ，使用 公鑰 pk(r)進行加密，接受者 r 接收到消息以後向發送者發送一個隨機變量 nr 加上以前的隨機變量 ni 使用本身的公鑰 pk(i)進行加密。接受者收到消息以後，解密出nr 發送給 接受者，並使用本身的公鑰進pk(r)行加密,這樣發送者和接受者都聲稱本身有安全認證的屬性 ni-synch 的擁有者。

   

 角色術語： 定義基本的角色術語

    Var : 表示用於存儲接受消息的變量     、    Const  :表示角色的每一個實例化新生成的常量，被認爲是局部常量。  、  Role ：定義角色   、   Func :表示函數的名字

   咱們將角色術語集定義爲基本術語套，使用構造函數進行擴展以進行配對和加密，而且假設配對是右關聯的。

  

  當咱們想要使用個函數的 f 的時候，其定義域是 X，能夠這樣標記  ：------->  {f(x)| x ∈X}

這裏咱們定義一個術語的逆 使用函數：

         咱們規定 — ^-1是本身的逆， （rt ^-1）^-1=rt  

   在整片論文中咱們假設公鑰pk 和私鑰映射到非對稱祕鑰的元素函數中，咱們使用pk 表示i代理的公鑰，使用sk表示代理的私鑰

    （補充數學量詞   ∀R∈Role ：pk(R)^-1=sk(R)^sk(R)-1=pk(R) 表示 對任意的R 屬於 Role均成立右面的等式。）

例子： 咱們創建角色R的私鑰模型 sk(R)和對應公鑰的逆 pk(R),使用公鑰模型加密消息 m 表示模型爲  ： {/m/}pk(R) ,  對消息進行簽名，並非直接使用祕鑰進行加密，而是被稱爲：消息摘要」加密，

爲了使私鑰正確的簽名消息 m 模型，咱們須要一個函數  h , 簽署消息 m 以後的的術語是  （m, {/h(m)/}sk(R)）

定義：描述角色，（協議是由角色組成的，而角色又是由角色事件組成的）。

    咱們定義一組事件集，RoleEvent 使用兩個新的組，標籤 Labe 和安全聲稱 Claims

  

      上面的事件集解釋以下： 事件 表示發送的消息 rt  綁定到代理 R上 ，打算用於綁定代理 R' ,一樣的 指明消息  rt 被代理 R ’ 綁定，顯然是由代理 R發送過來的，事假聲明表達，執行此事件時 R 指望安全目標  c 與可選參數  rt 保持一致。聲稱事件僅僅表示涉及本地代理R 並非其餘任何人的指望的代理。標籤標記事件來消除協議規範中相同事件的相似避免發生歧義，第二層含義是表達發送事件和接受事件的之間的關係，

      定義次運算符：  定義子術語，其中包括用於加密的祕鑰，注意術語形如 f(rt)的術語沒有子句，由於被認爲是非組合型術語。除了發送和接受術語以外，角色規範還定義了執行角色的初始知識，也是一組術語。

    定義以下：

   定義 角色知識： 咱們定義角色知識，將角色知識集RoleKnow定義爲不包含變量做爲子項的全部角色術語的集合。

       做爲結果，咱們有這樣的表達式 由於角色事件徹底描述角色的行爲。    沒有必要聲明局部常量和變量，協議的執行不須要角色知識，這裏引入角色知識有兩個緣由，首先他容許靜態角色的一致性測試，在給定初始知識集的狀況下查看角色是否能夠執行，第二，他將使咱們可以系統的推導出文章末尾的初始入侵者。

   定義角色規範： 角色規範包含一系列的事件，一些事初步知識，所以咱們定義了角色規範集合 像  ： RoleSpec=RoleKnow×RoleEvent*

 咱們寫成[ε1,ε2]指定 兩個事件列表，ε1和ε2 ，咱們寫 [ε1,ε2]^.[ε3] 去指定兩個列表的級聯，  常常在書寫單個事假的時候咱們會省略括號直接寫成,ε1^.ε2 表示 [ε1,ε2]。

  咱們書寫  A B指定一個局部函數，他將A的元素映射到元素B上，  

 定義2.8  一個協議規範角色行爲經過設置協議的部分功能，如此咱們有這樣的表達式  ： Protocol=RoleRoleSpec 

    咱們使用 MR^P(R)做爲協議規範 P中角色 R的初始知識簡寫。在不少狀況下咱們省略 參數 P 在協議上下文很清楚的狀況之下。符號  MR是M的縮寫，以後咱們將用做表示知識，R 用做表示角色。

      角色事件在協議中的描述必須是惟一的，能夠經過標籤事件進行強制執行，者容許咱們定義一個角色函數:   RoleEvent ------> Role ,鑑於角色事件，角色函數也是事件中的一個。咱們將協議做爲一個隱式的參數，當協議上下文清楚的時候。

定義 2.9  下面的角色描述模擬了NeedHam-Schroeder 協議的發起者角色，沒有任何的安全要求。

 

 2.2.2 事件順序

      事件的每一個角色對應於事件列表，換句話說， 一個結構順序加到屬於角色R的協議事件中，這個總數的排序指定 ，如此 對於任何角色R∈Role 和 ε1，ε2 ∈RoleEvent ,這樣 role(ε1)=R 和role(ε2)=R 我麼有這樣的表達式 ： 我麼認爲有個抽象的安全協議 P做爲通訊序列結合，每個順序組件由特定的角色承擔。通訊由裝飾事件的標籤管理，標籤直接定義溝通（通訊）關係：

 定義2.10  通訊關聯

    對於全部的 ∈ Label  以及 m1 ,m2 ∈ Role ×Role ×RoleTerm ,通訊關係定義爲： 這個關係規範了發送事假和接受事件如何對應。

 Example 2.11  事假順序和通訊關係：  對於示例協議 NS  角色排序 和關於角色 i 和 r ,分別表示以下：

  

    通訊關係表示以下：

  

2.2.3 靜態要求

      在上一節中咱們已經解釋了協議規範的抽象的語法，適當的協議規範還應當知足不少無缺性的要求，並非任何有發送、接受、和聲明的事件被認爲是安全的協議，列如，咱們要求代理可以構建出他發送的條款，而且他不能檢查條款的內容和加密的祕鑰。

    良好的角色，  對於每個角色，咱們要求有本身肯定的標準，這些標註的範圍是至關明確的，列如，協議角色定義中的每一個時間都是具備執行它的相同的角色（事件參與者和執行者），對於消息，咱們要求發送者可以實際構造這些消息，對於變量應該首先出如今接受事件中，在實例化以前能夠出如今發送時間中。對於接受事件，從上的協議的列子中能夠看出， 在咱們描述Needham-Schroeder protocol

    咱們定義一個 預測 WF 表達一個角色定能夠的一致性要求，  使用輔助定義RD （可讀性）和一個推理知識的關係，

             角色能夠撰寫和分解術語對，若是代理指導加密祕鑰，則能夠加密術語，若是代理知道響應的解密祕鑰，則能夠解密加密的術語。

定義 2.12 推理運算法

     使用M做爲 一個角色知識集，  知識推理關係 概括以下： 全部的角色術語 rt ,rt1 ,rt2  ,k :

       

Example 2.13 推理和加密  從術語集 組成 術語 term{/m/}k ，可是不是  k ^-1 沒法推斷 是m 或者 k  i e

         給定 和 k ^-1 咱們可以推斷出 m , 若是 k 是非對稱祕鑰 （如此 k k ^-1 ），而且給定{/m/}k 和k ^-1   沒法推斷 K

   

Example 2,1,4 推斷和子句 

     給定術語  m1 和m2 以及 通常狀況之下，m2 不是 ，一個反例給出 m1=(rt1, rt2) 和 m2=(rt2 ,rt 1) 當 rt 1不等於rt2 ，反之則否則。好比，由於給定術語 k 和 m 以及 咱們有 k 可是

Example 2.1.5 推斷和函數