黃寄洪，甘金明

（梧州學(xué)院 計算機科學(xué)系，廣西 梧州 543002）

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

然而，要設(shè)計一個沒有漏洞的安全協(xié)議實屬不易。目前，協(xié)議中的漏洞大多是通過形式化方法發(fā)現(xiàn)的。而在各種協(xié)議的形式化分析方法中，值得注意的是串空間（Strand Space）模型，它具有簡潔明了的特點，主要依靠一定的因果關(guān)系將協(xié)議執(zhí)行過程表示為圖結(jié)構(gòu)，并建立了在網(wǎng)絡(luò)通信中可能傳輸?shù)男畔⒌拇鷶?shù)，在認證協(xié)議和密鑰分配協(xié)議的研究中，有著較大的影響。

1 相關(guān)工作

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

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

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

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

2 符號與假設(shè)

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

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

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

3 串空間

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

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

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

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

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

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

圖1：輸出認證測試

圖2：輸入認證測試

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

4 SECT協(xié)議目標

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

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

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

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

5 兩方子協(xié)議

圖3：P，Q兩方子協(xié)議

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

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

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

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

6 三方協(xié)議

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

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

對三方協(xié)議，要求遵循如下原則：

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

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

（3）如果一個參與者收到不是發(fā)給自己的信息，則轉(zhuǎn)發(fā)給下一個參與者。

（4）

圖4 SECT協(xié)議流程圖

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

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

7 小結(jié)

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

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

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

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

［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.