電子商務協議可追究性的Ｋａｉｌａｒ分析與改進

　　摘要：可追究性是電子商務安全性的基本要求之一，Kailar邏輯是專門針對電子商可追究性進行分析的邏輯。然而Kailar邏輯也存在不足。本文討論了邏輯的一種缺陷———初始化假設不當而致Kailar邏輯不能正確分析各方的可追究性，并分析了出現這種缺陷的原因，提出了改進方案。
　　關鍵詞： 可追究性；Kailar邏輯；初始化假設
　　中圖分類號：F062.5 文獻標識碼：A
　　
　　一、 引言
　　
　　電子商務協議是保證網絡正常商務活動的基礎。可追究性和公平性是協議中最重要的性質，可追究性要求任何交易方必須為自己的行為負責，即一條消息被發送或者接收后，應該通過一定的方式，保證信息的收方發方都有足夠的證據證明接收或發送操作已經發生，并且能夠確定發送方或接收方的身份，發送方或接收方都不能否認其發送或接收操作已經發生，非否認性在電子商務中具有特別重要的作用，缺乏非否認性則容易引起交易方之間的糾紛。
　　Kailar邏輯[1]是目前用于電子商務協議分析的最有效的形式化方法之一。 而在利用Kailar邏輯分析電子商務協議時，需要將協議形式化，但這個形式化的過程卻是非形式的，極易導致協議分析失敗[2]。本文以研究電子郵件協議及其修改協議[3]的可追究性為例，分析了Kailiar邏輯進行時易出現的兩個問題，給出解決方案。
　　
　　二、Kailar邏輯
　　
　　Kailar邏輯是Rajashekar Kailar提出的提出的一種對電子商務責任性（即非否認性）[4]進行形式化邏輯證明的方法，其基本概念是責任性。下面首先介紹Kailar邏輯的符號、語義及語法。
　　
　　1.基本符號
　　主體（principal）：參與協議的各方；A，B：交易主體;K是密鑰，其中Ka表示主體A的公鑰，Ka-1表示與Ka相對應的A的私鑰;m表示消息;TTP可信任的第3方(trusted third party，簡稱TTP) 。
　　Kailar邏輯中的邏輯公式如下：
　　A CanProve x：表示A可以向任何主體證明x是正確的，而不泄露任何其它秘密y(y≠x)給其它主體，我們將這種證明叫強證明：
　　A CanProve x to B：表示A可以向B證明x是正確的，而不泄露任何其它秘密y(y≠x)給其它主體，我們將這種證明叫弱證明;
　　A IsTrustedOn x：表示任何主體都相信A給出的x是可信的;
　　A IsTnxstedOn x by B：表示B認為A給出的x是可信的，或者說A可以向B證明A能對x負責;
　　Ka Authenticates A：密鑰Ka 能夠用于認證主體A的身份，即能夠將主體A與以密鑰Ka-1加密
　　x in m：表示x是m中的一個或幾個可被理解的域，它的含義是由協議設計者明確定義的。可被理解的域通常是明文或者主體擁有密鑰的加密域;
　　A say x：表示A說過x(因而A對x負責)。通常，隱含地假設以下推論成立：
　　
　　x∧y：表示x并y。
　　2. Kailar邏輯的基本規則：
　　有：連接規則K1;推理規則K2：信仰關系K3;簽名規則K4和信任規則K5。
　　3.Kailar邏輯的分析步驟
　　利用Kailar邏輯來分析協議共有4個步驟：（1）列舉協議要達到的目標;（2）對協議的語句進行解釋。使之轉化為邏輯公式。在這一步中，只對那些包含簽過名的明文消息并且和分析可追究性相關的語句進行解釋;（3）列舉分析協議時需要用到的初試假設;（4）對協議進行分析。
　　
　　三、 協議非否認性分析
　　
　　非否認性原則要求電子商務協議為參與協議的各個主體提出充分的證據以解決今后可能出現的糾紛。一般地協議的非否認性通過發方非否認性和收方非否認性來達到，發送方的不可否認（Non-repudiation of origin）即為消息的收方提供消息來源的證據以避免發送消息的一方否認曾經發送過消息m，該證據由發送方（有時與協議中的第三方一起）產生，接收方擁有；接收方的不可否認性（Non-repudiation of recipient）即為消息的發方提供收到消息的證據以避免收到消息的一方否認曾經收到消息m，該證據由接收方（有時與協議中的第三方一起）產生，發送方擁有。
　　認證電子郵件協議CMP1 (certified electronic mail) [4]可以為電子郵件的傳輸提供非否認服務的，它是弱可追究的；而CMP1（b）是不可追究的。
　　CMP1(b)協議的形式描述如下：
　　
　　利用Kailar邏輯進行推理，可以證明該協議滿足可追究性[2]。而事實并非如此，導致錯誤結論的原因在于初始化假設A8。除可信任第三方TTP外，每個主體都有可能是不誠實的， 假設A8將由非可信任的主體B的聲明得到的結論(B Received h(m))未加驗證地作為得出進一步的結論(B received m)的依據是不嚴格的。
　　
　　四、Kailiar邏輯的改進
　　
　　為此，需要在初始狀態假設中加入一個檢測機制：如果一個主體不是可信任第三方，那么認為他所聲明的陳述不總是與事實相符是合理的。因此，當將這些陳述或者將根據假設由這些陳述得到的結論作為得到其他結論的依據時，應驗證其有效性。即將假設A8修改為
　　
　　五、結束語
　　
　　用Kailar邏輯對電子商務協議可追究性的形式化分析過程中，需要在推理之前引入一些初始化假設，但這些初始化假設的引入是一個非形式化的過程，不恰當的引入初始化假設會導致協議的分析失敗。本文通過對初始化時存在的問題的研究，提出改進，修正不適當的假設、補充新的假設，可以有效進行協議的可追究性分析。
　　作者單位：焦作大學
　　
　　參考文獻：
　　[1] Kailar R.Accountability in electronic commerceprotocols[J].IEEE Transactions on Software Engineering， 1