第四章 系統測試和安全規約分析
4.2 系統測試
在這節中，我們以Neumann Stubblebine，Woo And Lam 和 Andrew Secure RPC 三個Security Protocols 為實驗範例 (在附錄一中例出其它範例)，為了方便解說，
我們在分析時，會直接找出弱點。首先，我們先看Neumann Stubblebine Security Protocol，圖 3.3 為此安全規約的輸入格式，經過程式轉換後，下列為輸出的內 容：
maybeforged([[A,NA,TB],KBS], RR, LL) :- key(B, KBS), generate(B, TB), (var(A) -> same(A, '_0'); public(A)), (var(NA) -> same(NA, '_1'); public(NA)), \+same(B, A),
\+member([[A,NA,TB],KBS], RR), same([[B, 2-2], [[A,NA,TB],KBS]| RR], LL).
maybeforged([[B,NA,KAB,TB],KAS], RR, LL) :- same(S,s), key(A, KAS), key(B, KBS), key(S, KAS), key(S, KBS), generate(S, KAB), public(B),
\+member([[B,NA,KAB,TB],KAS], RR), available([[A,NA,TB],KBS], [[S,3-1], [[B,NA,KAB,TB],KAS]|RR], LL), \+same(S, A), \+same(S, B).
maybeforged([[A,KAB,TB],KBS], RR, LL) :- same(S,s), key(S, KBS), generate(S, KAB), \+member([[A,KAB,TB],KBS], RR), available([[A,NA,TB],KBS], [[S,3-2], [[A,KAB,TB],KBS]|RR], LL), \+same(S, A).
maybeforged([[NB],KAB], RR, LL) :- key(A, KAS), generate(A, NA), public(NB),
\+member([[NB],KAB], RR), available([[B,NA,KAB,TB],KAS], [[A,4-2], [[NB],KAB]|RR], LL), \+same(A, B).
available(Y, RR, LL) :- current_predicate(public/1), public(Y),same([[public, Y]|RR], LL).
available(Y, RR, LL) :- maybeforged(Y, RR, LL).
forge(A, B):- available(A, [], B).
same(X, X).
key(s,kas).
key(a,kas).
key(s,kbs).
key(b,kbs).
generate(a,na).
generate(b,nb).
generate(b,tb).
generate(s,kab).
public(a).
public(na).
public(b).
public(nb).
public(nb).
在Prolog 的環境中，我們用 Prolog 內建的指令 consult 將轉換出來的檔案載入，
用法如下：
?- consult(‘filename.pl’).
假如我們要攻擊 B 時，我們就必需傳送 B 在安全規約所有接收到的訊息，其為 第一個和第四個communication actions，在第一個 communication action 中的所有 訊息都是未加密訊息，所以我們可以很容易偽造，但在第四個 communication action 中的所有訊息都為加密訊息，因此我們就必需想辦法偽造，注意在第四個 communication action 中的第二個加密訊息為{Nb}Kab，其 Nb 為公開的，而 Kab 是從第四個communication action 中的第一個加密訊息中得到的，因此我們用上 一節中所提出的第二種分析方法，詢問 A 在最後一步送出的加密訊息，如下：
?- forge([[a,K,tb],kbs],L).
其有一結果為：
K = '_1'
L = [[b,2-2],[[a,'_1',tb],kbs]]
從結果中，我們發現變數K 可以為任意值，且此加密訊息可從 B 在第二 communication action 中的第二個加密訊息得到，因此攻擊方式如下：
(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
接下來我們分析Woo And Lam Security Protocol，其輸入內容為下：
ASSUMPTION:
key(S,Kas).
key(A,Kas).
key(S,Kbs).
key(B,Kbs).
generate(B,Nb).
PROTOCOL:
A->B: A B->A: B, Nb
A->B: { A, B, Nb }Kas
B->S: { A, B, { A, B, Nb }Kas }Kbs S->B: { A, B, Nb }Kbs
經過程式轉換後的輸出為：
maybeforged([[A,B,NB],KAS], RR, LL) :- key(A, KAS), (var(B) -> same(B, '_0');
public(B)), (var(NB) -> same(NB, '_1'); public(NB)), \+same(A, B),
\+member([[A,B,NB],KAS], RR), same([[A, 3-1], [[A,B,NB],KAS]| RR], LL).
maybeforged([[A,B,LABEL_0],KBS], RR, LL) :- key(B, KBS), (var(A) -> same(A, '_0'); public(A)), (var(LABEL_0) -> same(LABEL_0, '_1'); public(LABEL_0)),
\+same(B, A), \+member([[A,B,LABEL_0],KBS], RR), same([[B, 4-1], [[A,B,LABEL_0],KBS]| RR], LL).
maybeforged([[A,B,NB],KBS], RR, LL) :- same(S,s), key(A, KAS), key(B, KBS), key(S, KAS), key(S, KBS), \+member([[A,B,NB],KBS], RR),
available([[A,B,[[A,B,NB],KAS]],KBS], [[S,5-1], [[A,B,NB],KBS]|RR], LL),
\+same(S, B), \+same(S, A).
available(Y, RR, LL) :- current_predicate(public/1), public(Y),same([[public, Y]|RR], LL).
available(Y, RR, LL) :- maybeforged(Y, RR, LL).
forge(A, B):- available(A, [], B).
same(X, X).
key(s,kas).
key(a,kas).
key(s,kbs).
key(b,kbs).
generate(b,nb).
public(b).
public(nb).
public(a).
載入 Prolog 的環境後，假如我們要攻擊 B，如上例一樣，必需傳送給 B 在安全 規約所有接收的訊息，B 在安全規約的第一個，第三個和第五個 communication actions 分別收到 A，M 和{A, B, Nb}Kbs，注意，第三個 communication action 收 到的訊息是一個用 Kas 加密的訊息，所以對 B 而言，它只是一個看不懂且不需 要了解的加密訊息 (如之前所說的，分析時，必需以個別參與者的觀點看待一個 安全規約)，所以我們只要能偽造{A, B, Nb}Kbs，我們就可以用 A 的身分去欺騙 B，因此我們詢問 {A, B, Nb}Kbs：
?- forge([[a,b,nb],kbs], PATH).
其有一結果如下：
PAHT = [[b,4-1],[[a,b,nb],kbs]]
我們可以從B 的第四個 communication action 中得到此加密訊息，其攻擊方式為 下：
(i1) (A)Z->B: A (i2) B->(A)Z: B, Nb (i3) (A)Z->B: Nb
(i4) B->(S)Z: { A, B, Nb }Kbs (i5) (S)Z->B: { A, B, Nb }Kbs
最後我們分析Andrew Secure RPC Security Protocol，其輸入內容為下：
ASSUMPTION:
key(A, Kab).
key(B, Kab).
generate(B, Kab1).
generate(A, Na).
generate(B, Nb).
generate(B, Nb1).
PROTOCOL:
A->B: A, { Na }Kab B->A: { Na, Nb }Kab A->B: { Nb }Kab
B->A: { Kab1, Nb1 }Kab
轉換後的輸出如下：
maybeforged([[NA,NB],KAB], RR, LL) :- key(B, KAB), generate(B, NB),
\+member([[NA,NB],KAB], RR), available([[NA],KAB], [[B,2-1], [[NA,NB],KAB]|RR], LL).
maybeforged([[NB],KAB], RR, LL) :- key(A, KAB), generate(A, NA),
\+member([[NB],KAB], RR), available([[NA,NB],KAB], [[A,3-1], [[NB],KAB]|RR], LL).
maybeforged([[KAB1,NB1],KAB], RR, LL) :- key(B, KAB), generate(B, KAB1), generate(B, NB1), \+member([[KAB1,NB1],KAB], RR), available([[NB],KAB], [[B,4-1], [[KAB1,NB1],KAB]|RR], LL).
available(Y, RR, LL) :- current_predicate(public/1), public(Y),same([[public, Y]|RR], LL).
available(Y, RR, LL) :- maybeforged(Y, RR, LL).
forge(A, B):- available(A, [], B).
same(X, X).
key(a,kab).
key(b,kab).
generate(b,kab1).
generate(a,na).
generate(b,nb).
generate(b,nb1).
public([[na],kab]).
public(a).
從這個安全規約中，我們可看出此安全規約是利用之前所建立的安全金鑰(Kab) 建立一把新的金鑰(Kab1)，我們用上一節中所提出的第二種分析方法詢問一下：
?- forge([[K,nb1],kab],PATH).
其有一結果如下：
K = na
PATH = [[public,[[na],kab]],[b,2-1],[[na,nb1],kab]]
從結果中我們知道，如果我們得到一個訊息{Na}Kab，然後送給 B，B 就在第二 個 communication action 中 產 生 {Na ,Nb1}Kab ， 因 此 我 們 就 可 以 在 第 四 個 communication action 時把此加密訊息傳送給 A，使 A 誤以為 Na 為新產生的安全 金鑰，或許有人會質疑，在規約中，B 在第二個和第四個 communication actions 分別產生Nb 和 Nb1，而此二個 Nonce 是不一樣的，但是上述的攻擊方式是用同 一個Nonce Nb1，注意到，在規約中，第四個 communication action 所產生的 Nb1 對A 是沒有意義的，因為 A 是第一次收到 Nb1，所以並沒有那樣的問題存在，
其攻擊方式如下：
(i1) A->B: A, { Na }Kab (i2) B->A: { Na, Nb }Kab (i3) A->B: { Nb }Kab
(i4) B->(A)Z: { Kab1, Nb1 }Kab (i4) (B)Z->A: { Na, Nb }Kab
上面的攻擊方式對攻擊者而言，似乎沒有利益，但是上面的run 執行完時，B 認 為所建立新的安全金鑰為Kab1，但 A 認為是 Na，因此雙方的認知不同。