第二章 安全規約分析系統設計
2.1 安全規約的觀察
在目前的TCP/IP 架構下,一個封包的 source IP 是說明這個封包的來源,當 這個封包在網路上傳送時,任何經過的伺服器都有能力更改source IP 的欄位,
並且任何一個人都可以發送一個不屬於自己source IP 的封包給任何人,也就是 說,一個封包的source IP 並沒有任何保護的機制,因此對於接收到封包的人而 言,就不能完全依賴source IP 的欄位去認定封包的來源,而在安全規約的描述 中,並無這樣的考慮,但是在分析時,我們就必需以真實環境的特性去驗證規約 的安全性。一個安全規約的描述通常如圖2.2,圖 2.2 是 Neumann 和 Stubblebine 在[14]所提出的一個安全規約,他們用簡潔地方式說明一下這個安全規約如何運 作和一些事前的必要條件,很多提出安全規約的人也是用相同的方式,但實際上 這樣的描述方式是不足夠的。下文中我們可以看到為什麼那樣的敘述方式是有問 題的,並提出四個觀察。
如我們所知,在電腦網路的世界和真實的世界是不一樣的,當程式設計師在 撰寫一個安全規約的程式時,他所需要的資訊不只是每一個步驟的作法,還需要 更仔細的說明,例如訊息之間的關係,以圖2.2 為例,圖中的描述如下,當 A 和 B 要建立一個安全通訊管道時,A 送出他的 Identity 和一個 Nonce,當 B 收到這
樣一個訊息時,他根據規約中的規定送出相對應的訊息給一台信任的伺服器S,
當每個步驟都正確執行完時,A 就認定 B 是他一開始所想要建立連線的人,並
且雙方共有一把安全金鑰,對 B 而言,他也有相同的認知。不過,實際上,這
樣的一個規約只有說明在那一步時要傳送什麼訊息的行為,而收到訊息時和送出 相對應訊息之前所必需完成的動作有什麼,這樣的動作並未很明確地表現在規約 裡,甚至收到訊息和之前收到的訊息是否有需要檢驗的動作也沒有詳盡的說明,
例如說,時間郵戳的檢查,當B 在第四步時所收到的加密訊息中的時間郵戳 Tb,
是否要和在第二步時所產生的時間郵戳一致?如果 B 忽略了這個檢查的重要 性,下列情況將會發生 (S 是一台信任的伺服器,Z 是攻擊者)。
(i1) A->B: A, Na
(i2) B->S: B, {A, Na, Tb}Kbs, Nb
(i3) S->(A)Z: {B,Na,Kab,Tb}Kas , {A,Kab,Tb}Kbs, Nb #Z intercepts this message (ii1) (A)Z->B: A, Na #Z pretends A (ii2) B->S: B, {A, Na, Tb’}Kbs, Nb’
(ii3) S->(A)Z: {B,Na,Kab’,Tb’}Kas , {A,Kab’,Tb’}Kbs, Nb’ #Z intercepts this message
(i3) (S)Z->A: {B,Na,Kab’,Tb’}Kas , {A,Kab’,Tb’}Kbs, Nb (i4) A->B: {A,Kab’,Tb’}Kbs, {Nb}Kab’
這樣的攻擊方法似乎並沒有違反當初Neumann 和 Stubblebine 設計此安全規約的 目的,雙方彼此認證,也建立了一把安全金鑰,然而,雙方所建立的安全金鑰是 Kab’,但伺服器在建立這把安全金鑰時,是要給 B 和攻擊者 Z 之間的安全通訊 使用,如今成為A 和 B 共有的一把金鑰,或許有人會爭議說,這樣的攻擊方式 對攻擊者Z 也沒有利益,而且 A 和 B 也建立了一把安全金鑰,但仔細想想,這 個攻擊方式的確違反了設計者所期望一個成功的run 所必需的條件,所以對一位 程式設計師而言,這樣未在規約中呈現的隱喻行為必需被明朗化,對一個安全規 約分析師也是如此。
觀察一:一個安全規約隱含著未被明確說明的行為。
一個安全規約只規範如何完成認證的行為和訊息中所要的資訊,因此在規約 中的符號相當於電腦程式中的變數一樣。如圖2.2 中, A,B,Na,Tb,Nb 和 Kab 都是變數,簡單地分析一下Na 和 Nb,Na 是 A 送出的 Challenge,而 Nb 是 B 送 出的Challenge,個別只對產生他們的 A 和 B 有意義,因此 Na 和 Nb 並無任何的 相關性存在,也就是說,Na 和 Nb 可以為相同的值,但並不是每一個在規約中 的符號都可以為任意值,首先,A 和 B 可以是任何人,但不可以是同一個人,
理由是非常直覺的,A 不會相信攻擊者聲稱自已是 A 而要和 A 認證,可是在範
例中,S 是必需要和 A 與 B 個別有一把安全金鑰,如 Kas 和 Kbs,並且 Kas 只 有S 和 A 共有,Kbs 只有 S 和 B 知道,因此 S 必需是一個被 A 和 B 所信任的伺 服器。如果 Na 和 Kab 碰巧為相同值時,那下面列的情況也就有可能發生,而 Kab 就可以從第一個訊息中得到了。
A->B: A, NK
B->S: B, {A, NK, Tb}Kbs, Nb
S->A: {B, NK, NK, Tb}Kas , {A, NK,Tb}Kbs, Nb A->B: {A, NK, Tb}Kbs, {Nb}NK
觀察二:一個安全規約只規範如何完成認證的行為和訊息中所要的資訊,訊息中 的符號相當於電腦程式中的變數。
如我們之前所提到的,在電腦網路裡,一個訊息的傳送者並不一定就是訊息 的發送者,根據這個認知,一個安全規約所描述的只是一連串訊息的收發動作,
如圖2.2 中,對 A 所描述的行為如下,當 A 要和 B 建立安全連線時,A 送出他 的Identity 和一個 Nonce,然後等待接收訊息,這個訊息必需合乎規約的規範,
等他收到一個所期望的訊息後,他便送出相對應的訊息,然後完成建立連線,此 連線的資料是依據交換訊息中變數的值而定,所以在範例中,對一個發起建立連 線者,如A,所要執行的步驟如下:
步驟一:送出自己的Identity, A 和一個 Nonce, Na
步驟二:收到 {對方的 Identity, Na, K, T}Kas ,M 和 N (K, T, M, N 為變數) 步驟三:送出M 和{N}K
在步驟二中,因為發起建立連線者A,並不知道對方和伺服器的安全金鑰 Kbs,
所以對他而言,第二個訊息{A,Kab,Tb}Kbs 只是一個變數 M,而第三個訊息是 B 產生的Nonce,所以也是一個變數 N,因此一個安全規約是以概觀的角度來描述 一連串交換訊息的動作,但這樣的概觀方式和個別參與者對訊息接受和發送的觀 點是有所不同的,所以當在分析一個安全規約或程式設計時,安全規約的概觀會 困惑分析師和程式設計師,然而以個別參與者的觀點去分析和設計將更容易看出
個別參與者的行為。
觀察三:一個安全規約是由數個子規約所構成的,每個子規約代表個別參與者和 伺服器的行為。
我們引用在[15]所說的一段話:
“The spy is allowed to perform any of these actions at any time, subject only to the limitation that the messages it introduces must be feasible to produce from its current state of knowledge (initial and what it has learned since) under the rules of the cryptographic systems in use.”
這段話所描述的內容是非常直覺的,一個攻擊者在任何時間都能竊聽和中斷參與 者之間或參與者和伺服器之間的連線,修改或偽造訊息,但其修改或偽造訊息必 須合乎攻擊者能力範圍內;相對地,如果以觀察三的觀點切入,任何參與者所產 生的訊息也是根據他現有的資訊產生出來的,換句話說,任何參與者在一個安全 規約中所產生的訊息不管是加密或未加密都是有依據的,在分析一個安全規約 時,我們重視的是加密訊息,原因非常明顯,一個攻擊者可以很容易地偽造一個 未加密的訊息,但就不一定能偽造一個加密的訊息。
觀察四:每一個加密訊息都有一個因果關係。
在下一節中,我們將利用四個觀察結果設計出一個安全規約分析系統,此系 統將會把一個安全規約轉換成 Prolog 的語言,因此我們就可以藉由電腦高速處 理的能力來發現安全規約中的弱點。