Scyther-Semantics and verification of Security Protocol 翻譯 (第二章 2.2.2----2.3)

2.2.2  事件順序

協議中的每一個角色對應於事件列表，換句話說， 在屬於角色 R 的協議事件集上施加結構，總的排序表示爲 $ \prec $ , 如此任何角色 R∈Role 和 $\varepsilon 1$ ,$\varepsilon 2$ ∈ RoleEvent,這樣 Role($\varepsilon 1$)=R 和 role($\varepsilon 2$)=R 咱們有 這樣的表達：$ \varepsilon 1 \prec \varepsilon 2\vee \varepsilon 1=\varepsilon 2\vee \varepsilon 1\succ R\varepsilon 2$  咱們認爲一個抽象安全協議P 視爲通訊順序過程的集合。每個順序組件由特定的角色承載。通訊由裝飾事件的標籤管理，由於標籤直接決定了通訊的關係  ↝。

定義2.10 （通訊關係）： 全部的  $\imath $∈Label  ， m1, m2 ∈ Role ×Role ×RoleTerm , 通訊關係 ↝ 表示爲 ：

$\varepsilon 1$ ↝ $\varepsilon 2\Leftrightarrow \exists \imath $  m1,m2:$\varepsilon 1=send \imath (m1) \Lambda \varepsilon 2=read \imath (m2)$ . 該關係規定了發送協議事件和協議接受事件如何對應，

例子： 2.1.1 （事件角色和 通訊關係）： 比方說 NS 協議， 角色順序  $\prec$ i 和 $\prec$ r 是角色 i 和 r ，分別以下表示：

通訊關係 ↝ 給出以下表示：

2.2.3 靜態要求

 在以前的章節中我麼解釋了抽象的協議規範語法。適當的協議規範必須知足許多良好的形式要求，並非任何發送、聲明、讀取事件序列被認爲是安全的協議，比方說，咱們要求代理必須可以構建他發出的術語條款，若是他不知道祕鑰則不能檢查加密術語的內容。

良好的角色： 對於每個角色，我麼要求他符合基本的某些標準，這些範圍至關的明顯，例如：角色定義中的每一個事件都具備相同的角色執行它（被稱爲該事件的參與者），關於消息的更加微小的要求。對於消息，咱們要求發着的消息實際上能夠有發送者構造，若是消息在發送角色中，則知足此要求。對於變量咱們要求首先出如今一個讀取事件中， 在該事件中被實力化，而後才能出如今發送事件中。

對於讀取事件，狀況要複雜的多，從上面的列子中能夠看出，咱們描述協議 Needham-Schroeder 初始角色，讀取事件對傳入的消息施加結構，以這種模式的形式，若是接受者的知識知足某些要求，那麼他只能將消息與這種預期的模式相匹配。

咱們介紹一種預測形式  WF （Well- Formed） 表示角色定義知足這些一致性要求，使用輔助預測 RD （Readable）和一個推論知識關係$ \vdash $ : RoleKnow × RoleTerm

角色能夠組成和分解術語對，若是代理知道加密祕鑰則能夠加密術語，若是代理知道解密祕鑰則一樣能夠解密加密的術語。

定義 2.12 （知識推理操做）

 使用 M 做爲角色知識集，知識推理關係$ \vdash $ : RoleKnow × RoleTerm  定義概括以下： 針對所欲的角色術語  rt 、 rt1 、 rt2 、k

列子 2.13   （推理和加密）

  從一個包含 {/m/}k術語的術語集，不包含$k^{-1}$  不可以推斷出 m 或者 k ,i ,e

給定術語表達式 {/m/}k  和 $k^{-1}$  ，咱們可以推斷 m , 若是 k 是非對稱祕鑰（這就是說 k 不等於$k^{-1}$ ），給定{/m/}k  和 $k^{-1}$  不可能推斷 k

例子 2.14 （推論和子項）：給定兩個術語 m1 和 m2 關係是 {m1}$\vdash $m2 ,一般並非這種 m2$ \sqsubseteq $ m1 ,給出一個反例： m1 =( rt1,  rt2) 和 m2=(rt2, rt1) 當 rt1不等於 rt2的時候。反過來也沒有。例如 由於給定術語 k  和 m 以及 ，咱們有  k $\sqsubseteq $ {/m/}k 還有

例子 2.15 （推論和函數）給定術語 f(rt) 且 f ∈Func , 沒有適用的進一步推理規則，如此推斷 rt 是不可能的，在這方面，咱們框架中的函數充當散列函數。咱們能夠放心的安全建模祕鑰 （列如：k(rt1,rt2),sk(rt1)） 做爲散列函數在相同的地方。正如咱們後面將看到的，代理名稱最初被代理和入侵者所知。建模 ， 所以不會增長任何相關方的可推斷條款。

（在模型中，應用推理運算符的全部集合都包括 rt1  、 rt2）

預測 RD： P（RoleTerm）× RoleTerm  表示哪些角色術語能夠用做具備特定知識集的代理讀取事件的消息模式。變量總會在讀取模型中出現，其餘任何術語只能以讀取模式發生，若是能夠從代理的知識中推斷出來（由從任何先前讀取事件中得到的初始知識組成），只有這樣才能將它與傳入的消息進行比較。

爲了可以讀取整對，咱們必須讀取每一個成分，同時經過從其餘組件推斷出的知識擴展知識，若是可從知識推斷出加密消息，或者若是能夠在解密以後推斷出加密消息，則能夠讀取加密消息。

定義 2.16 （可讀預測）：M 是 一個角色知識集，rt 是一個角色術語， 用做下面的額模式。

 特殊的，若是看到這種狀況， rt $\equiv $(rt1 , rt2)  可以讀取這樣的消息能夠對應於首次從 rt2  提取一些祕鑰，該祕鑰能夠用於解密 rt1 。反之也成立。

咱們有這樣新的預測結構， WF：Role × RoleSpec ,表示角色形式很好, 此預測第一個參數始終是事件發生角色，它用於表示執行事件的角色（例如：發送事件的發送者）應該與發生的角色相匹配，從發送和聲明事件知識中必須能夠推斷出術語。而讀取事件中的發生術語不準根據上述定義可讀。此外，代理應該只能讀取指向他的信息，而且只能發送給標記正確標籤的消息。若是一個術語在一個聲明事件中做爲i參數，沒有這樣的要求，由於這取決於聲明事件中參數的功能，在後續的章節中將會看到。

定義 2.17 （好的構造性）： R是一個 角色，M 做爲一個角色知識集，讓咱們列出角色事件列表：

對於協議規範 P： Role $\mapsto$RoelSpec 咱們要求全部的角色都是關於最初的知識良好的形式。表示爲 $\forall R\epsilon $dom(P): WF (R,P(R)) , 咱們使用 dom(f) 表示  f 的部分功能。

例子 2.18 （角色描述的正確性）： 首先考慮下面不正確的角色描述：

 角色描述 wrong1 格式錯誤，由於在讀取時發送變量 V。根據定義 2.6 初始角色知識集不包含變量，在 WF預測形式中，變量將會只會成爲角色知識的一部分（參數 M）在他們已經讀取後。在隨後的事件中 這些變量能夠從 m 中推斷出來，所以能夠做爲發送消息的一部分。

例子 2.19 （正確的角色描述） ：考慮下面錯誤的角色描述：

     

咱們看到在 wrong2 中的讀事件 包含一個 子術語 {/ V/}k2  ,目的是經過此讀取初始化 V。 然而 k2 是對稱祕鑰， k2 不是角色知識，經過此讀沒法肯定V的值。所以角色描述格式不正確，正確的角色描述以下：

2.3 協議執行描述

   在上面的章節中咱們已經成了協議形式化的描述概念，是協議如何表現的靜態描述，當這樣的協議描述執行的時候，動態方面介紹，涉及到代理模型的各個方面以及域分析的執行模型，這就須要引入一些協議描述級別上沒有出現的新概念。特別的咱們將模擬的動態行爲建模爲標記過分系統。

 2.3.1 運行

   協議規範描述了一組角色，這些角色充當系統中實際代理能夠執行的操做藍圖，執行協議時，每一個角色能夠執行屢次運行，多是並行執行，也可由多個代理執行。咱們稱之爲一個單 （運行）多是部分的，執行一個角色描述爲一個運行，從實施角度來看，一個運行 相似於一個線程，在咱們的模型中，有同一個代理執行的運行時獨立的，不存在共享任何變量問題。

執行角色會將角色描述轉換成爲運行，這被稱爲是實例化，爲了實例化一個角色，咱們必須將角色名稱綁定到實際代理的名稱上，咱們必須使每一個實例化的本地常量都是惟一的。此外，咱們必須考慮到值與變量的綁定也是運行本地的。所以，在運行中出現的術語集不一樣於角色描述中出現的術語集。

咱們假設存在一個集合 RID 來表示運行表示符， 並設置一個代理集合表示 代理，運行術語和角色術語定義是相似的，不一樣之處在於抽象角色由具體代理替換，經過使用運行標識符擴展局部常量使其成爲惟一的。運行術語集好包括由入侵者生成的基本的集合 IntruderConst ,這個集合只會在2.4.2 章節中使用，  之後會再詳細的介紹。

定義 2.20  （運行術語）而且變量由具體值實例化，

 

定義 2.21  （實例功能）：  對於每個運行，  存在兩個兩個相關的角色術語和運行術語，一個角色術語轉換成一個運行術語，

經過應用實例化：

 實例化的第一個組件肯定常量擴展的運行標識符，第二個組件肯定代理的角色實例化。第三個決定了變量的估值。

咱們延伸 逆 function$^{-1}$ 到運行術語集中，角色功能： RoleTerm $\rightarrow $P(Role)和  vars: RoelTerm$\rightarrow $P(Var) 肯定術語中出現的角色和變量，咱們以明顯的方式將這些功能擴展到RoleSpec。

咱們常常提取第一個組件，運行標識符來自實例化。咱們將使用符號 runidof(inst) 表示運行標識符來自實例化 inst

定義 2.22 （實例化術語）

咱們有 inst∈Inst  是一個實例，而 inst=（θ，ρ，σ） ，使 f ∈ Func 和 rt 、rt1....... rtn 做爲角色術語，像這樣 roles(rt) $\subseteq$dom(ρ)  和 vars(rt)$\subseteq$dom(σ), 咱們定義實例：<inst>:

RoleTerm $\rightarrow $RunTerm 以下：

 

例子 2.23 （實例化術語） 咱們改定兩個實例化，可能在執行協議的時候發生：

定義 2.24 （運行） 一個運行是事件角色的實例化，定義爲 Run=Inst ×RoleEvent$^{x}$

       咱們將會在後面看到，每個系統的運行，將會有一個肯定的標識符，由於經過角色描述已經實現了靜態定義， 咱們能夠在運行規範中省略他。

考慮到系統由一些代理執行的許多運行組成，運行之間的通訊是異步的。爲了方便模擬不一樣入侵者的行爲，咱們將通訊經過兩個緩衝。咱們有一個輸出緩存來自發送運行，還有有個輸入緩存來自接受運行。（關於這種）入侵者可以決定消息從輸出緩存到輸入緩存。輸出緩存和輸入緩存均可以存儲消息，消息包括髮送者、接受者。一個運行的術語表達式：  MSG=Agent ×  Agent ×  RunTerm 。  緩衝區是這樣消息的多重集合 ： Buffer=M(MSG) ,爲了不標記混亂，我麼使用MSG 當 MSG∈ RunTerm ，避免在RunTerm 上重定義已經存在的操做

完整的網絡模型還包括入侵者元素，目前尚未討論過，特別的，在過分系統中定義狀態概念，咱們須要介紹一組術語從 P（RunTerm），在第2.4 節中提到過動入侵的概念。

定義 2.25 （網絡狀態）： 在一個安全協議中，代理執行角色的網絡狀態定義以下：

               State=P（RunTerm）× Buffer × Buffer × P (Run)     這樣狀態中包含攻擊者知識，內容有輸出緩存，輸入緩存，（並且剩餘的）任然要被執行。

指定在讀取事件中，若是匹配肯定的模式，來自緩衝區的消息會被代理接受，我麼引入一種預測模型 Match 表示消息與變量的某些實例化模型匹配。這個預測的定義知識系統的一個參數，咱們將會給出一個直接的匹配實例。

例如，咱們爲每一個變量定義一組容許值得運行術語，我麼介紹一種輔助函數類型 ： Var -----P(RunTerm )   :定義做爲變量有效值的運行術語集。咱們能夠給出三個定義類型的列子，會致使讀取事件的語義有稍微的不一樣。

例子 2.26 （模型匹配： 武缺陷類型）： 在大多數狀況下，咱們假設運行術語集被劃分紅有限的 S一、 S二、 ..... Sn ，這能夠表明代理角色，隨機變量、代理名稱、會話祕鑰、加密、元組。這種類型匹配模型咱們有下面的要求，

    若是變量的類型是  Nonce  ，僅僅匹配運行術語的 Nonce

定義 2.27 （簡單類型匹配：基礎類型缺陷）：