安全電子商務交易協議的設計及其形式化分析

黃寄洪，甘金明

（梧州學院 計算機科學系，廣西 梧州 543002）

所謂安全協議，是在協議中應用加密解密的手段隱藏或獲取信息，達到認證以及消息正確發送的目的。運用安全協議，人們可以解決一系列的安全問題，如：對信息源和目標的認證、信息的完整性、時效性等。因此，安全協議是通訊和網絡安全體系、分布式系統和電子商務的關鍵組成部分，是安全系統的主要保障手段和工具。

然而，要設計一個沒有漏洞的安全協議實屬不易。目前，協議中的漏洞大多是通過形式化方法發現的。而在各種協議的形式化分析方法中，值得注意的是串空間（Strand Space）模型，它具有簡潔明了的特點，主要依靠一定的因果關系將協議執行過程表示為圖結構，并建立了在網絡通信中可能傳輸的信息的代數，在認證協議和密鑰分配協議的研究中，有著較大的影響。

1 相關工作

大量的安全協議設計似乎是依賴于設計者的技巧和獨創性。其中最著名的是Abadi和Needham[4]。他們提出了一系列關于怎樣使密碼協議正確的方法以及如何使密碼協議準確完成其安全目標。但是他們的理論不能系統化，也不能基于某種使協議目標正確的理論。

Butty'an等人[6]基于類BAN邏輯設計了一個協議設計方法，但這種方法很難從他們所給的例子中抽象出來。

Song[5]基于串空間理論設計了一種邏輯，再以此為模型得到一個協議自動檢測算法－Athena。這種算法在一定條件下能處理狀態空間爆炸的問題，而且可以用于協議的生成。可是這種方法還不能利用子協議的獨立性去分解協議的設計過程，然后再把那些安全的小協議合成為完整的大協議。

我們設計的SECT協議是為了在三方協議交互中，使任意兩方享有某些信息的機密性保護，并提供相互認證功能。同時，SECT還能提供有效的非否認證明。

2 符號與假設

參與者有三個不同的角色，類似于顧客，商店和銀行，我們將分別表示為C，M，B。當然，即使是同一個參與者在不同的協議中可擔任不同的角色。比如：當一家商店向另一家商店訂貨時，就分別作為C和M；而一家銀行向商店購物時，就會作為C。我們將用P，Q泛指協議中任意兩個參與者。

在三者之間，有一些信息是共享的，比如：三者的標識符和C向M提交的購物金額。但還有一些信息只限于兩方知道，第三方不知道的，比如：C向M所購買的商品就與B無關；另外C的信用卡號最好不要讓M知道；而M與B之間的交易手續費用屬于商業機密，不應該讓C知道。參與者P發送給Q的機密信息記為MsgP,Q；而P的所有可以共享的信息記為PubP。

信息t被P的密鑰KP加密記為tP。把hash函數h作用于信息t所得的值記為h（t）。而所有能夠證明攻擊者所不能得到的密鑰稱為安全密鑰，記為Safe。

3 串空間

下面介紹串空間模型的一些基本概念。

定義3.1 串空間（strand space）[1]是一個二元組（∑，tr）。其中∑是一個串（strand）的集合，這里的串可以用來表示任何序列。在協議分析中我們用它表示協議參與者或攻擊者的行為序列。如果參與者是誠實的，就叫作正規串；如果參與者是不誠實的，就叫入侵者串。tr是一個映射，表示為：

這里A表示一個集合，（＋A）*表示由A中元素組成的有限序列。我們稱這樣的一個映射為跡映射，映射的像稱作原像的跡（trace）。

定義3.2 對于一個串空間∑，定義節點為n＝，s屬于∑，i是一個整數并滿足 1≤i≤length（tr（s））。如果一個節點屬于一個正規串，則稱之為正規節點。定義term（n）=（tr（s））i。

定義3.3 輸出測試（outgoing test）令發出的加密包{…a…}K中包含一個唯一生成值a，其中K-1∈Safe，如果接收回一個不同的加密包{… a…}K1，則這個包首先是由一個正規的參與者生成的。圖1表示了[3]命題19的簡化形式。

定義3.4 輸入測試（incoming test）[2]如果接收到一個加密包{… a…}K，其中K∈Safe，并且a從來沒有以這樣的加密形式發送過，則這個包首先是由一個正規的參與者加密的。圖2表示了[3]命題20的簡化形式。

圖1：輸出認證測試

圖2：輸入認證測試

定義 3.5 主動測試（unsolicited test）[2]：如果接收到term={|h|}K，并且密鑰K∈Safe，則{|h|}K產生于某個正規的串。

4 SECT協議目標

（1）機密性：所有的加密交互信息保持機密性，發給另一方的信息不能給第三方解密。

（2）一類認證：參與者P能收到來源于Q的關于接收到P發送給Q的信息的證明。

（3）非否認性：每個參與者P都能向第三方證明其一類認證。

（4）二類認證：參與者Q能收到一個證明，證明如果其接收到聲稱是由另一個參與者所發的信息，則這個信息確是由P在當前這輪協議運行中所發出的。

5 兩方子協議

圖3：P，Q兩方子協議

參與者 P 的數據就是兩個值：MsgP，Q和 PubP。這兩個值在傳輸過程中顯然應該用Q的密鑰加密，根據輸入認證測試，這個過程要把一次性隨機數NP，Q和{|MsgP，Q^PubP|}Q 一起傳輸。如果把 NP，Q也同時用Q的密鑰加密，則子協議的這一步也可同時作為輸出測試。當Q接收到P的信息后，返回的認證信息應該包含{… NP，Q…}Q。有時我們也需要返回包含MsgP，Q和PubP的信息，比如：當我們發出一個訂單，那返回信息中就希望看到對貨物的確認。所以Q返回的信息中包含{… NP，Q^t…}Q，其中 t包含 MsgP，Q和PubP的信息。在這里我們選擇了 h（MsgP，Q^PubP），考慮到以后P和Q都可是C，M或者B，這樣共有6種可能。為了將彼此區分開來，在協議每一步加入標識 ci，i從 1到 6。同時加上 F，S，T 作為子協議中各步的標識。

當P=C，Q=M時，在商務流程是這樣的：當商店收到訂單后，首先解密，檢查訂單是否正確，核實貨物和單價；然后送到財務部，財務部hash MsgP，Q和PubP；然后簽字，接著執行下一步。

為了完成二類認證目標，根據對Q的輸入認證測試，Q向P發送一次性隨機數NQ，P，因為P的簽名密鑰是安全的，當 Q 收到{|…^NP，Q^NQ，P^h（MsgP，Q^PubP)|}P后完成了一次輸入測試。

協議的正確性由輸入認證測試，輸出認證測試和主動測試得知所設計的子協議滿足上面所說的四個協議目標。

6 三方協議

定義6.1 強分離加密：n1是子協議∑1的節點，n2是子協議∑2的節點，如果{|h|}K?（n1）則{|h|}K（n2），稱∑1和∑2滿足強分離加密。

根據串空間理論，當子協議∑1和∑2滿足強分離加密時，∑1和∑2是獨立的，即∑1不論子協議∑2是否正在運行，都能實現其原定的安全目標。由圖3的數據結構能夠知道所設計的P，Q兩方子協議滿足強分離加密條件，所以當多個兩方子協議同時運行時，不影響各自的安全目標。

對三方協議，要求遵循如下原則：

（1）對C和M以及C和B的子協議，都將首先由C開始第一步。當M和B分別接收到C和M的信息時才開始執行子協議的下一步。

（2）每個參與者只處理每個子協議中的確是發給自己的本協議的信息。

（3）如果一個參與者收到不是發給自己的信息，則轉發給下一個參與者。

（4）

圖4 SECT協議流程圖

P，Q均表示為C，M，B其中之一；

SECT協議的四個安全目標的證明類似于雙方子協議。

7 小結

文章中，我們利用串空間理論構造了一個電子商務協議SECT，展示了怎樣利用協議的形式化分析工具來設計安全協議。協議的設計過程分為以下幾步：

（1）明確表示出協議將要完成的目標。把某些僅由其中一部分參與者完成的目標設計成子協議。

（2）對于每個目標，選擇一種認證方式來完成。驗證每個子協議是否實現了獨立的安全目標。再用分離加密保證協議的獨立性。

（3）把子協議組合成完整的大協議，最后檢驗其安全性。

［1］F.Javier Thayer F'abrega，Jonathan C.Herzog，and Joshua D.Guttman.Strand Spaces:Why is a security protocol corrSECT？In Proceedings of the 1998 IEEE Symposium on Security and Privacy， pages 160-171.IEEE Computer Press，1998.

［2］Guttman，J.D.and F.J.Thayer F'abrega，Authentication tests， in:Proceedings， 2000 IEEE Symposium on Security and Privacy，May 2000.

［3］Joshua D.Guttman and F.Javier Thayer F'abrega.Authentication tests and the structure of bundles.Theoretical Computer Science，2002.

［4］M.Abadi and R.Needham.Prudent engineering practice for cryptographic protocols.In Proceedings，1994 IEEE Symposium on Research in Security and Privacy，pages 122-136.IEEE，IEEE Computer Society Press，1994.

［5］D.X.Song.Athena:a new efficient automated checker for security protocol analysis.In Proceedings of the 12th IEEE Computer Security Foundations Workshop.IEEE Computer Society Press，June 1999.

［6］L.Butty'an，S.Staamann，and U.Wilhelm.A simple logic for authentication protocol design.In 11th IEEE Computer Security Foundations Workshop，pages 153-162，1998.