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