Rule 轉換

上一章節中，我們已經介紹我們的安全規約分析系統，其主要有三個部分：

basic facts，rules 和 available predicates，在這一節中，我們將說明如何把系統中 的三個元件轉成 Prolog 的格式。我們實作在第二章中如何建立每一個加密訊息 的rules，實作 MAIN，COTAIN，COLLECT，DERIVE 和 PRINTRULE Procedures

只是程式設計，因此我們不討論如何用 C，Java，或其它程式語言撰寫這四個

Procedures，但是我們重視的是在執行完這些 Procedures 後所產生的輸出：basic facts，rules 和 available predicates。首先是 basic facts，基本上，basic facts 已經 是合乎Prolog 的語法了，basic facts 是從使用者輸入得到的，且從上一節輸入格 式的規定中得知，basic facts 已經是 Prolog 的 facts，惟一需要修改的是把 basic facts 轉成小寫，這樣才符合Prolog 中 atom 的定義，從使用者的輸入中，我們已經有 一個facts 的資料庫。現在我們需要建立加密訊息的 rules，從第二章中我們知道 每一個加密訊息在輸入的安全規約中，經過PRINTRULE Procedure 就會產生相 對應的rule (第一個 communication action 除外)，但那樣的格式並不符合 Prolog 的語法，因為Prolog 中沒有“{”和“}”，所以我們必需將原來加密訊息的格式轉成 Prolog 中的 List Structure，如圖 3.5，用二層 List 來表示一個加密訊息，外層 List 的第一個欄位為另一個存放所有元素的List，第二個欄位則為加密的金鑰，如果 有一個加密訊息裡含有一個加密訊息，其表示方式為[[ [[elements, …, elements], key2] ], key1]，當加密訊息經過轉換 List 的格式後，其格式已經符合 Prolog 的要 求，但我們需要額外的修改，才能有效地找出一個安全規約的弱點，首先，如圖

3.6 中的 2)，偽造加密訊息{B,Na,Kab,Tb}Kas 需要加密訊息{A,Na,Tb}Kbs，但在 詢問偽造加密訊息{B,Na,Kab,Tb}Kas 時，如果 Prolog 回答 true 時，表示加密訊 息{B,Na,Kab,Tb}Kas 是可以被偽造的，但偽造時要經過其它的 rules (如在這個例 子中的{A,Na,Tb}Kbs)並沒有被顯示出來，因此我們需要建立一條 derivation path，所以修改 maybeforged(M)為 maybeforged(M,RR,LL)，其中 M 為加密訊息，

RR 為臨時的 derivation path，LL 為最後成功時的 derivation path，相對地，在每 一個maybeforged 中的 available 就必須負責建立臨時的 derivation path 的責任，

因此修改成available(N, [[S, CA-nth], M | RR], LL)，M 為 maybeforged 中的加密 訊息，N 為加密訊息 M 所依賴的加密訊息，S 為 M 的發送者，CA 為目前第幾 個communication action，nth 為目前 communication action 的第幾個訊息，如圖 3.6 中的 2)就修改成如下：

maybeforged([[B,NA,KAB,TB],KAS], RR, LL) :- key(S, Kas), key(S, Kbs),

public(B), generate(S, Kab), key(B, Kbs), key(A, Kas), available([[A,NA,TB],KBS], [[S,3-1], [[B,NA,KAB,TB],KAS]|RR], LL).

接著，因為 available 可能會用相同的 rule 去詢找所需要的加密訊息 N，為了避 免無限迴圈發生，我們在每一個available 的詢問前加入\+member(M, RR)，\+和 member 為 Prolog 內建的規則，\+為邏輯的 NOT，如果 Element 是 List 中的一個 元素，member(List, Element)為 true。修改後如下：

maybeforged([[B,NA,KAB,TB],KAS], RR, LL) :- key(S, Kas), key(S, Kbs), public(B), generate(S, Kab), key(B, Kbs), key(A, Kas),

\+member([[B,NA,KAB,TB],KAS], RR), available([[A,NA,TB],KBS], [[S,3-1], [[B,NA,KAB,TB],KAS]|RR], LL).

注意，上面這個rule 是由伺服器發送出來的加密訊息，因此此加密訊息只有伺服 器才能送出的，因此再次修改如下，其中same(X, Y)表示如果 Y 或 X 是一變數 而另一個為值，變數那個就會等於值，注意same(S,s)，S 為一變數代表此加密訊 息的發送者，而s 為值，表示伺服器。注意，因為 same 這個規則不是 Prolog 內 建，所以在輸出時，我們必需加“same(X,X).”到輸出的檔案裡。

maybeforged([[B,NA,KAB,TB],KAS], RR, LL) :- same(S,s), key(S, Kas), key(S, Kbs), public(B), generate(S, Kab), key(B, Kbs), key(A, Kas),

\+member([[B,NA,KAB,TB],KAS], RR), available([[A,NA,TB],KBS], [[S,3-1], [[B,NA,KAB,TB],KAS]|RR], LL).

最後我們修改public，如果一個 rule 中沒有 available，那表示此 rule 並沒有依賴 其它rules，接著如果此 rule 有 public，但 public 中的參數為一變數，表示此變數 可 以 為 任 意 值 ， 因 此 我 們 改 變 原 有 的 public(X) 為 (var(X) -> same(X, '_$');

public(X))，其中$為任意數值，var 為 Prolog 內建的規則，如果 X 為變數，var(X) 為true，此用意是使 public 的值不會因為詢問時所用的值使結果為特定的值，也 就是說，所以如果在詢問後的結果中看到“_”開頭的，表示其變數可為任意值 (如 2.2 中的範例)，因此圖 3.6 的 1)修改如下：

maybeforged([[A,NA,TB],KBS], RR, LL) :- key(B, KBS), (var(A) -> same(A, '_0');

public(A)), (var(NA) -> same(NA, '_1'); public(NA)), generate(B, TB),

\+member([[A,NA,TB],KBS], RR), same([[B, 2-2], [[A,NA,TB],KBS]| RR], LL).

因此從第二章PRINTRULE Procedure 得到的 rule，需要做下面四個修改動作：

修改一：修改maybeforged(M)和 available(N)分別為 maybeforged(M,RR,LL)和 available(N, [[S, CA-nth], M | RR], LL)，S 為訊息 M 的發送者，CA 為目 前第幾個communication action，nth 為目前 communication action 的第幾 個加密訊息。

修改二：在available(N, [[S, CA-nth], M | RR], LL)之前加入\+member(M, RR)。

修改三：如果訊息M 的發送者為伺服器，加入 same(S,s)到條件裡。注意，在我 們的實作中，我們以s 表示為何服器。

修改四：如果rule 中有 public 的條件但沒有 available，以(var(X) -> same(X, '_$');

public(X))取代原有的 public(X)，$為任意數值，並加入\+member(M, RR), same([[S, CA-nth], M| RR], LL).

最 後 ， 因 為 available 並 不 會 因 安 全 規 約 的 改 變 而 有 所 變 化 ， 但 為 了 配 合 maybeforged 的修改，因此必需由

available(W) :- public(W).

available(W) :- maybeforged(W).

修改成

available(Y, RR, LL) :- current_predicate(public/1), public(Y),same([[public, Y]|RR], LL).

available(Y, RR, LL) :- maybeforged(Y, RR, LL).