Rule 的建立

在說明如何建立加密訊息的 rules 前，我們有一個很自然的假設：每一位參 與者和伺服器都會老老實實地根據安全規約中的communication actions 去執行，

以觀察三的結果來說，每一位參與者和伺服器都會根據自己的子規約所規定的收 發順序去執行，所以說，每一位參與者和伺服器在一個run 中，如果收到符合規 約中所期望的訊息，就會往下一步執行，送出相對應的訊息，然後再次等待收到 下一個符合規約中所期望的訊息出現，就這樣接收和傳送，一步一步地完成自己 的子規約，最後依據交換訊息中變數的值結束。在這個假設之下，對每一個加密

訊息 X 內的元素處理，以發送者的觀點去推導個別元素的來源，最後列出元素

之間的隱含關係和元素與來源之間的隱含關係 (這些隱含關係是用 basic facts 的 key 和 generate 表示)，然後我們就得到一個 rule (如圖 2.3 的表示方式) 說明產生 此加密訊息X 所需要的訊息為何以及其訊息之間必需有何關連。

maybeforged(X) :- C1, C2 … , Cn (for 1 ≤ i ≤ n, Ci 為一個 basic fact 或 available predicate) 圖2.3 The format of a rule

在我們的系統裡，我們用圖2.3 的方式來表示一個 rule，其說明為：當 C1, C2,…,Cn 都符合時，攻擊者就可以得到加密訊息 X；如果加密訊息 X 會依賴另 一個加密訊息Y，我們就以 available(Y)來表示，因為 Y 可能是任何人都可獲得 或是可藉由另一個rule 得到，因此 available predicates 為下(此 W 為變數)：

available(W) :- public(W).

available(W) :- maybeforged(W).

以前一節的(r3)為例，在我們的系統裡，就以下面方式來表示：

maybeforged({A, Na, Tb}Kbs) :- public(A), public(Na), generate(B, Tb), key(B, Kbs). (r4)

我們用下面的五個 Procedures 來建立加密訊息的 rules，這五個 Procedures 分別為COLLECT，CONTAIN，DERIVE，PRINTRULE 和 MAIN，在介紹每一 個Procedure 功能為何前，我們定義 BF 為 basic facts 的假設集合，且所有出現在 Procedures 中的邏輯關係(and 和 or)為 Short-circuit Boolean Expression。

首先，COLLECT Procedure 有三個輸入欄位，第一個為要收集元素的訊息 M，第二個為要存放元素的集合 Q，而最後為安全金鑰的集合 KQ。這個 Procedure 的功能為收集一個未加密或加密訊息M 中的元素到元素集合 Q 且依據金鑰集合 KQ 決定是否可收集加密訊息 M 內的元素或把整個加密訊息 M 當作一個元素，

如果加密訊息 M 中有加密訊息，其一樣依據金鑰集合 KQ 決定是否繼續收集此 加密訊息內的元素或把它當成一個元素收集。圖2.4 為 COLLECT Procedure，下 面我們說明圖2.4 的正確性：

如果訊息M 為一個未加密訊息，訊息 M 就會在第四行時被加入元素集合 Q 裡，然後結束，回傳元素集合 Q，而元素集合 Q 也只有訊息 M 一個元 素，所以是正確的；反之，如果訊息M 是一個用金鑰 K 加密的訊息，但 如果金鑰K 不在金鑰集合 KQ 裡，訊息 M 就會被視為一個單一的元素，

一樣在第四行時被加入元素集合 Q 裡，然後結束，所以一個加密訊息的

金鑰不在金鑰集合KQ 裡，此加密訊息內的元素就不會被收集；可是，如 果金鑰K 在金鑰集合 KQ 裡，我們就再次利用 COLLECT Procedure 收集 每一個在訊息M 裡的元素 Y，如果元素 Y 是一個用 K’加密的訊息且 K’

在集合金鑰KQ 裡，我們就又一次呼叫 COLLECT Procedure 收集每一個

在 Y 裡的元素，因為每一個元素最後一定是一個未加密訊息或是一個加

密訊息，但加密金鑰不存在金鑰集合KQ 裡，因此第三行並不會產生無限 遞迴且會正確地依據集合 KQ 來收集每一個元素，所以 COLLECT Procedure 就能正確地依據金鑰集合 K 收集每一個在訊息 M 中的元素到元 素集合Q 中。

下列為一個範例：

COLLECT({A, {B, {C, {D}Kas}Kcs}Kbs}Kas, Q, {Kas, Kbs}) 其輸出的Q 為：

{“A”, “B”, “{C, {D}Kas}Kcs” }

COLLECT (M, Q, KQ)

圖2.4 COLLECT procedure

接著我們介紹CONTAIN Procedure，CONTAIN Procedure 有四個輸入，分別 為訊息X，訊息 M，和二個安全金鑰的集合 KQ1 和 KQ2。CONTAIN Procedure 的功能為判斷訊息M 是否為訊息 X 或著訊息 M 是否有包含訊息 X，如果回傳 true 傳值為true 時，KQ2 = TotalKQ – KQ1。圖 2.5 為 COTAIN Procedure，下面我們 說明其正確性：

在第一行時，我們宣告二個空集合，分別為TQ1 和 TQ2，接著在第二行 時，我們設定一個flag 為 false，這個 flag 決定 CONTAIN Procedure 回傳 時的值為true 或 false，在第三行中，如果訊息 M 等於訊息 X，我們就設

KQ1 和 KQ2 會正確地存放相對應的安全金鑰。

下列為一範例：

CONTAIN({a}Kbs, {b, {a}Kbs, {{c}Kcs}Kbs}Kas, KQ1 ← Ø, KQ2 ← Ø) 其輸出的為true，KQ1 為{Kas}，KQ2 為{Kbs, Kcs}。

CONTAIN(X, M, KQ1, KQ2) 1 TQ1← Ø , TQ2 ← Ø;

15 return flag;

圖2.5 CONTAIN procedure

下面我們介紹第三個Procedure，DERIVE Procedure 有五個輸入，分別為訊 息X，訊息陣列 SM，元素集合 Q，條件集合 P 和字串 S。S 為訊息 X 的發送者， 中的元素為一個安全規約中以S 為接收者的 communication action，所以一個訊 息陣列SM 中的元素可以有多個訊息存在。如果 DERIVE Procedure 回傳 true 的 話，表示訊息X 出現在某一個 SM 的元素中(communication action, SM[I] for some I)，元素集合 Q 就會收集每一個包含或等於訊息 X 的訊息 M 中的每一個元素，

其包括S 知道在訊息 M 中的金鑰；另外，如果回傳 true 且訊息 M 為未加密訊息 (等於訊息 X)，加入 public(M)到條件集合 P，說明 M 是一個未加密訊息；反之 如果是加密訊息(包含訊息 X)，加入 available(M)到條件集合 P，說明 M 是一個 加密訊息。圖2.6 為 DERIVE Procedure，下面我們說明其正確性：

在第一行中，我們先設 flag 為 false，然後，在從第二行到第二十五行迴 Procedure 中知道到訊息 M 包含訊息 X 的話，也就是 CONTAIN Procedure 回傳 true，那我們就設先 flag 為 true，因為金鑰集合 KQ1 含有從加密訊

最後收集加密訊息M 中的元素。注意，我們是以 communication action 為 處理單位，也就是說，在訊息陣列 SM 的元素 SM[I]中，如果有一訊息 Y(未加密訊息)等於訊息 X 或訊息 Y(加密訊息)包含訊息 X，我們就不處 理下一個陣列SM 的元素 SM[I-1]，但在元素 SM[I]中的其它訊息 Y’還是

會被處理，因為其它訊息Y’也有可能等於或包含訊息 X(訊息 X 可能不只 依賴訊息Y，或許也有依賴在同一個 communication action 中的訊息 Y’)。

如果以 S 為觀點出發且訊息 X 無法從訊息陣列 SM 中找到，DERIVE Procedure 能正確回答 false；反之如果以 S 為觀點出發且在一個 SM[I]中 有找到訊息X，那元素集合 Q 和條件集合 P 就會存放相關的元素和條件。

26 return false;

圖2.6 DERIVE procedure

PRINTRULE Procedure 有四個輸入，分別為訊息 X，元素集合 Q，條件集合

如果其中任何一個條件符合我們就加入相對應的條件generate(S, I)，key(S, I)或 key(I, J)到條件集合 P，注意，在第四行的 Continue 會直接跳到第一 PRINTRULE Procedure 的要求。

PRINTRULE(X, Q, P, S)

10 print "maybeforged (X) :- ";

11 for each V _∈ P 12 do print V;

圖2.7 PRINTRULE procedure

最後，我們介紹主要的 MAIN Procedure，其輸入有二個欄位，一個存放一 個安全規約的communication action 陣列 CA 和一個存放 basic facts 的假設集合 BF。MAIN Procedure 將會對所有規約中的每一個加密訊息建立一個 rule，除了 出現在第一個communication action 中的加密訊息(圖 2.8 為 MAIN Procedure)。而 我們定義何謂一個正確的 rule，一個正確的 rule 為當所需要滿足的條件都成立 時，此rule 就會產生相對應的訊息(如圖 2.3 的 X)，然而如何建立一個正確的 rule 就是我們要討論的問題，首先，我們想一想，在一個安全規約中，第一個 communication action 的發送者在一個規約開始前，他並沒有事先收到任何訊息，

因此任何第一個communication action 中的訊息是發送者依據自己擁有的資訊產 生的，所以沒有任何人可以主動地要求第一個communication action 的發送者開 始執行一個 run，也就是說，如果有一個加密訊息出現在第一個 communication action 中，其加密訊息並不依賴外界的影響，所以在 MAIN Procedure 中的第四 行和第五行，我們把出現在第一個communication action 中的訊息以 public 的方 式加到假設集合 BF 中，接下來想想第二個 communication action，如果第二個 communication action 的發送者是第一個 communication action 的接收者的話，那 表示第二個communication action 中的訊息產生是因為收到第一個 communication action 的訊息且收到的訊息是合乎規約的規範，如圖 2.2 中的參與者 B 在第二個 communication action 中的加密訊息{A, Na, Tb}Kbs，其中 A 和 Na 是依據第一個 communication action 中的 A 和 Na，所以說，如果我們在第一個 communication action 中傳送 C 和{A, Na}Kcs 給參與者 B 的話，而參與者 B 就會在第二個 communication action 送出 C，{C, {A, Na}Kcs, Tb}Kbs 和 Nb，其中 Tb 和 Nb 為 參與者B 自己產生的，所以說，除了第一個 communication action 的訊息外的加 密訊息都有一個相對應的rule 存在(注意，我們只討論只有一個 initiator 的安全規 約，不討論multiple initiators)，所以在 MAIN Procedure 中的第六行到第二十三

行中，我們對每一個在陣列CA 的元素做處理，因為我們需要記錄每一位參與者

之前所收到的訊息，所以我們有一個陣列Message 來存放每一位參與者所收到的 訊息，如Message[B]表示 B 到目前為止所有收到的訊息，而 Message[B][1]表示 B 第一次收到的訊息，反之，Message[B][length[Message[B]]]表示 B 最近收到的 訊息，注意，此訊息是表示一個communication action 中的所有訊息，如在 MAIN Procedure 中的第三行和第十行。如我們之前所提的，一個 rule 並非只適用於特 定的參與者，所以說，我們要使它一般化，如上例中{A, Na, Tb}Kbs 的 rule，我

們要說明 key(B, Kbs)的關係是必需存在的，才能使它適用於任何參與者，所以 當要建立這個 rule 時，元素 A，Na，Tb 和 Kbs 就會被加入元素集合 Q 裡，而 public(A)和 public(Na)加入條件集合 P 裡，最後，從元素集合 Q 中找出隱含關係 (如 generate(B, Tb), key(B, Kbs))，將他們加入條件集合 P 裡，然後列出所如圖 2.3 的rule。從第十一行到第二十三行中，我們針對每一個在 CA[I]中的訊息 X 處理，

以發送者S 的觀點出發，也就是依據假設集合 BF 中對發送者 S 的 key 和 generate

假設為基礎，如果訊息 X 為一個未加密訊息，在第十三行的判斷就不成立，因

此就直接跳到第二十三行執行，把未加密訊息 X 以 public 的方式加入到假設集 合BF(注意第二十三行中，如果訊息 X 是加密訊息，表示發送者 S 是轉送之前收 到的訊息，因此不處理)，如果訊息 X 是一個以金鑰 K 加密的訊息且 key(S, K) 存在假設集合BF 中或可以從發送者 S 之前收到的訊息 Message[S]中找到，我們 就知道訊息X 是發送者 S 產生的，注意，如果 key(S, K)存在假設集合 BF 中，

我們就不會檢查是否可以從發送者 S 之前收到的訊息 Message[S]中找金鑰 K(Short-circuit Boolean Expression)；反之如果 key(S, K)不存在假設集合 BF 中，

我們才需要檢查是否可以從發送者S 之前收到的訊息 Message[S]中找到金鑰 K，

如果這兩個條件沒有一個成立的話，表示加密訊息 X 不是由發送者 S 產生的，

而是S 轉送出來的，所以就跳到第二十三行；相反，如果其中只要有一個成立，

而是S 轉送出來的，所以就跳到第二十三行；相反，如果其中只要有一個成立，