系統能力

我們的系統是藉由加密訊息之間的相似性找出所有可能產生一加密訊息的 方式，而這是因為我們在建立 rules 時是以發送者的觀點出發，所以有些表面上 是不相似的加密訊息實際上是相似的(如第 4.2 節中 Woo And Lam security protocol 的分析)，所以當我們詢問一個加密訊息時，只要有符合我們加密訊息格 式的 rules 都會被詢問，且當 rule 和 rule 之間有依賴性時，我們用 available predicates 來表示，而 available predicates 會先看看是否有一個 public 的訊息可以 符合目前要求的訊息，也就是說，我們是否可以用一個已知的訊息取代，如果沒 有的話，available predicates 就會問是否有一個 rule 可以符合目前要求的訊息，

這時，available predicates 並沒有問特定某一個 rule，換句話說，如果有兩個 rules 都和目前要求的訊息相似，available predicates 就會問這兩個 rules 是否可以符合 目前要求的訊息，而這就是我們所提到的訊息相似性。我們系統的能力如下：如 果在一個安全規約的正常前提假設下，此安全規約存在一個相似訊息攻擊方式，

我們的系統就可以找出此攻擊方式。我們證明在我們的系統下，這樣一個攻擊中

所有攻擊者沒辦法自行產生的加密訊息 M 都可以正確地被找出來，也就是說，

當我們詢問每一個加密訊息M 時，系統就會回答 true 且攻擊方式中產生此加密 的路徑(步驟)也可以正確地找出來，注意，產生加密訊息 M 的路徑也許有很多(因 為訊息的相似性)，但攻擊方式中產生加密訊息 M 的路徑為其中之一，我們利用

矛盾法證明，如果有一個加密訊息 M 為攻擊者沒辦法自行產生的加密訊息，且

產生的加密訊息M 的路徑為 P，當我們詢問是否可偽造加密訊息 M 時，系統回 答false 或回答 true 但沒有一個路徑為 P，因此我們證明系統可以推導出路徑 P，

所以系統會回答true 且有一路徑為 P。

令加密訊息集合F為攻擊方式中攻擊者無法自行產生的加密訊息，假設有 一個加密訊息M _∈F，加密訊息M是由路徑P = M1->M2->…->Mn->M的步 驟中得到的(Mi ∈F for 2 ≤ i ≤ n，M1必為未加密訊息或攻擊者可以自行產 生的，這是因為在正常的假設下，攻擊者不知道任何安全金鑰除了他自己 擁有的以外)；我們用反推的方式推導出路徑P，首先因為加密訊息M的格 式是符合規約中某一個加密訊息的格式(相似性)，而系統也對每一個加密 訊息建立一個rule，所以有一個rule可以產生加密訊息M，這是因為加密訊 息M是攻擊者在攻擊中所傳送的訊息，因此加密訊息M必符合規約中的某 一個加密訊息格式，所以有一個rule存在是可以產生加密訊息M，接著我 們知道在路徑P中的Mn->M表示必需得到加密訊息Mn才能得到加密訊息 M，也就是說，產生加密訊息M時需要加密訊息Mn(訊息之間的依賴性)，

而我們知道系統中也有一個rule可以產生加密訊息Mn(因為加密訊息Mn的 格式也必符合規約中某一個加密訊息的格式)且系統用available predicates 來表示訊息之間的依賴性(詢問是否有一個public的訊息或有一個rule可以 符合目前的要求)，所以在某一個可以產生加密訊息M的rule中的available predicates就能問到一個產生加密訊息Mn的rule，同理，產生加密訊息Mn的 rule中的available predicates就能問到產生加密訊息Mn-1的rule，當在推導到 M2時，因為M1->M2，所以系統中也會有存在一個rule可以產生加密訊息 M2，且我們知道M1為未加密訊息，表示某一個可以產生加密訊息M2 的rule 也沒有依賴任何其它的rules，所以說，當在詢問是否可得到加密訊息M 時，系統會找到某一個產生加密訊息M的rule，然後一個產生加密訊息M n

的rule，接著一個產生加密訊息M n-1的rule，就這樣一直找下去，最後找 到某一個產生加密訊息M2的rule，且此rule就會結束(不依賴其它的rules)，

因此系統就回答true且尋找的路徑和P一樣，這和我們的假設相反，證明 我們的系統可以正確地找出每一個攻擊中所有攻擊者沒辦法自行產生的 加密訊息。

以圖2.2 的 Neumann Stubblebine security protocol 為例，其攻擊方式為：

(i1) (A)Z->B: A, Na

(i2) B->(S)Z: B, { A, Na, Tb }Kbs, Nb (i4) (A)Z->B: { A, Na, Tb }Kbs, { Nb }Na

從攻擊方式中，我們知到攻擊者無法自行產生的加密訊息為{A, Na, Tb}Kbs (在 第(i4)步驟)，而產生此加密訊息的路徑為 “A, Na”->{A, Na, Tb}Kbs ((i1)->(i2))，

因此當我們詢問{A, Na, Tb}Kbs 時，系統必需回答 true 且有一路徑為“A, Na”->{A, Na, Tb}Kbs，下面為上一節中對 Neumann Stubblebine security protocol 所建立的 假設集合和四個rules(小寫為 constant，大寫為變數)：

key(a, kas) key(s, kas) key(b, kbs) key(s, kbs) generate(a, na) generate(b, nb) generate(b, tb) generate(s, kab) public(a) public(na) public(b) public(nb)

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

2) maybeforged({B,Na,Kab,Tb}Kas) :- public(B), available({A,Na,Tb}Kbs), generate(S, Kab), key(S, Kas), key(S, Kbs), key(B, Kbs), key(A, Kas).

3) maybeforged({A,Kab,Tb}Kbs) :- available({A,Na,Tb}Kbs)), generate(S, Kab), key(S, Kbs).

4) maybeforged({Nb}Kab)) :- key(A, Kas), generate(A, Na), public(Nb), available({B,Na,Kab,Tb}Kas)

從rule 1)中，系統可以正確地推導如下：

1) maybeforged({a, na, tb}kbs) :- public(a), public(na), key(B, kbs), generate(B, tb).

我們知道變數B 可為參與者 b，所以這個 rule 是成立的，且這個 rule 是在第二個 communication action 時建立的，也就是說它的路徑為“A, Na”->{A, Na, Tb}Kbs，

如同攻擊方式中的(i1)和(i2)，因系統就正確地回答 true 且找出路徑。在第 4.2 節 和附錄一中有其它規約的分析，從這些分析中，可以再次看出我們系統的能力。