系統架構

在介紹我們提出的安全規約分析系統前，我們先定義在我們系統裡何謂一個 有弱點的安全規約，當一個攻擊者可以利用它欺騙它人時，或它可以產生或執行 不如設計者所預期的情況出現時，我們說這個安全規約是有弱點。

從上一節中的四個觀察中，我們推導如下：從觀察三中，我們可以將一個安 全規約以個別參與者和伺服器的觀點分為多個子規約，而個別的子規約描述相對

應的參與者或伺服器的一連串收發訊息動作，因此從觀察四中，我們就得知，任 何參與者或伺服器在發送任何加密訊息時，此加密訊息是依據他們原有的資訊和 之前收到訊息中的資訊，再從觀察一中，我們得知此關係是隱含的，未被明確地 表現在規約上，因此在分析時，我們就必需將它明確地列出 (這些隱含的關係是 以發送此加密訊息者的觀點為出發)，在我們的系統裡，我們稱這樣的關係為 rule，最後從觀察二中，我們知道當我們建立任何加密訊息和他們個別依據資訊 的關係時，此關係並不是對特定參與者才適用，也就是說，任何人只要在規約中 扮演這個角色，且所收到訊息之間的關係符合要求，那就會產生相對應的加密訊 息，所以我們用“rule”說明加密訊息和他們個別依據資訊的關係並不特定於任何 人，任何攻擊者都可以利用這些 rules 偽造相對應的加密訊息只要他們能符合 rules 的要求。以圖 2.2 的 B 為例，B 的收發行為如下：

步驟一：收到 A, Na

步驟二：送出 B, {A, Na, Tb}Kbs, Nb 步驟三：收到 {A,Kab,Tb}Kbs, {Nb}Kab

當B 在第步驟二送出{A, Na, Tb}Kbs 時，這個加密訊息中的 A 和 Na 是從步驟一 得到的，因此他們的關係如下（“:- ”表示依據）：

{A, Na, Tb}Kbs :- 收到 A 和 Na (r1)

但這樣的條件是不足夠的，因為在{A, Na, Tb}Kbs 中，Tb 是 B 所產生的 Timestamp，所以 B 必需產生一個 Timestamp：

{A, Na, Tb}Kbs :- 收到 A 和 Na，並且 Tb 是 B 產生的 Timestamp (r2)

上面的描述對加密訊息{A, Na, Tb}Kbs 和他依據資訊之關係只適用特定的參與 者B，因為 Kbs 和 B 之間的關係並未明確地顯示出來，因此正確的關係如下：

{A, Na, Tb}Kbs :- 收到 A 和 Na，並且 Tb 是 B 產生的 Timestamp, B 必須有金鑰 Kbs (r3)

上面的描述就是一個rule，它適用於任何參與者扮演 B 的角色。所以當攻擊者 Z 需要偽造一個訊息是用Kas 加密時，並且訊息內容只有三個欄位，第一個和第二 個欄位分別為 X 和 Y，第三個欄位可以為任意值，因此攻擊者 Z 就可以利用這 個rule 造出所要的訊息，如下：

(X)Z->A: X, Y

A->(S)Z: A, {X, Y, Ta}Kas, Na

我們所提出安全規約分析系統的架構主要有三個原素構成，此三個元件為 basic facts，rules 和 available predicates，首先，我們介紹何謂 basic facts，每一個 安全規約在被執行前，提出規約者都有一些前提必要的假設，然後以這些前提的 假設為基礎，用正式或非正式的方法證明他們所提出的規約是安全且正確，因此 我們在設計一個分析系統時，系統也要把這些前提的假設考慮進去，所以我們用 basic facts 來表示安全規約中的前提假設，表示的方式有三種：public(X)，key(A, K)和 generate(A, N)，注意在這裡 X，A，K 和 N 為變數。public(A)是說 A 是公 開的，大家都可以得到的，如每一位參與者的Identity 都是公開的，基本上，因 為電腦網路的特性，每一個在規約中的訊息都是公開的，而加密的訊息和未加密 的訊息只差別於知道加密金鑰的人才能知道加密訊息中的內容。第二個key(A, K) 是用來描述參與者和伺服器所知道的金鑰，例如參與者 A 和伺服器 S 事前有建 立一把安全金鑰Kas，在我們的系統裡，就以 key(A, Kas)和 key(S, Kas)來表示這 個前提假設。最後，generate(A, N)是用來表示當在執行一個安全規約時，每一位 參與者在這個run 中所要產生的東西，如圖 2.2 中，A 要產生一個 Nonce Na，B 要產生一個Nonce Nb 和一個 Timestamp Tb，而伺服器 S 要產生一把金鑰 Kab，

我們以下列的 generate 來表示這些要求：generate(A, Na)，generate(B, Nb)，

generate(B, Tb)和 generate(S, Kab)。對一個安全規約的前提假設，我們已經提出 轉換的方式，接下來我們將在下一節中說明如何運用因果關係將一個安全規約中 所描述的訊息交換機制轉換成系統的rules，而將以集合 BF 表示一個安全規約的 前提假設，在我們的系統裡，每一個在規約中的加密訊息都有一個相對應的 rule，每一個 rule 說明了如何產生相對應的加密訊息，當然有些 rules 會依賴其它 rules，如圖 2.2，在第三個 communication action 時，S 送出兩個加密訊息，這兩 個加密訊息的rule 都是依據上一步所收到加密訊息，在系統裡，這樣 rules 和 rules

之間的相依性我們就用 available predicates 來表示，下一節我們將對 available predicates 進一步說明。在這裡我們必要注意到一件事，如果一個安全規約規定 第一個communication action 有加密訊息，在我們的系統裡，對此加密訊息我們 並無建立任何相對應的 rule,因為我們是以一個攻擊者的角度去分析一個安全規

約的弱點，對攻擊者而言，這個加密訊息只有當發起建立連線者在執行一個run

時，才能得到的。