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