◆

摘要：可追究性是电子商务安全性的基本要求之一，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负责)。通常，隐含地假设以下推论成立：

　　

A Says(x，y) A Says x

　　

A Receives m Signer with K-1：表示A收到了用K-1签名的消息m。

　　

xy：表示x蕴涵y，即若x成立，则有y成立;

　　

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)协议的形式描述如下：

  

(1)A→B：h(m)，，

  

(2)B→A：

  

(3)B→TTP： ，

  

(4)TTP→B：

  

(5)TTP→A：

  

其中，h(m)是消息m的单向Hash函数值，依据协议保证非否认性的目标解释协议语句并提出初始化假设

  

A1：A，B CanProve ( Authenticates TTP)

  

A2：A，TTP CanProve (Authenticates B)

  

A3：B，TTP CanProve ( Authenticates A)

  

A4：A，B CanProve (TTP IsTrustedOn (TTP Says))

  

A5： (A Says m) (A sent m)

  

A6： (B Says h(m))  (B received h(m))

  

A7： (TTP Says (B，m))  (TTP Says m成功发送给B)

  

A8： (B Received h(m))∧(m成功发送给B)  (B received m)

　　

利用Kailar逻辑进行推理，可以证明该协议满足可追究性[2]。而事实并非如此，导致错误结论的原因在于初始化假设A8。除可信任第三方TTP外，每个主体都有可能是不诚实的， 假设A8将由非可信任的主体B的声明得到的结论(B Received h(m))未加验证地作为得出进一步的结论(B received m)的依据是不严格的。

 

四、Kailiar逻辑的改进

　　

为此，需要在初始状态假设中加入一个检测机制：如果一个主体不是可信任第三方，那么认为他所声明的陈述不总是与事实相符是合理的。因此，当将这些陈述或者将根据假设由这些陈述得到的结论作为得到其他结论的依据时，应验证其有效性。即将假设A8修改为

　　

A8’：(B Received h(m))∧(m成功发送给B)∧(}=h()) (B received m).

　　

假设8’中增加了依据}=h()来验证B签名的消息是否与A签名的消息的Hash函数值相等，从而形成对主体A和主体B所签名的消息的相互印证和制约，以保证由假设A8′中的依据得出进一步的结论(B received m)的有效性。

　　

根据假设8’还需要验证结论A CanProve （=，然而根据在协议CMP1(b)执行过程中，没有任何主体检查与的相等性，因此该协议不满足可追究性。

 

将上述改进应用于分析CMP1协议：

  

(1)A→B：h(m)，，

  

(2)B→TTP ：，，

  

(3)TTP→B：

  

(4)TTP→A： ，

　　

初始化假设与CMP1(b)协议分析中改进的初始状态假设完全相同，可以判断CMP1协议也不满足可追究性。这是由于在CMP1协议的实际运行中，当且仅当在TTP验证了B的签名消息h(m)与A的签名消息m的Hash函数值相等的条件下，TTP才会执行语句3和4。这是协议继续执行的前提，为此增添两个初始状态假设表示这个验证操作：

　　

A9： (TTP Says (m signedWith )) (= (h))

　　

A10： (TTP Says  (h(m) SignedWith ，(B，m)))(= (h))

　　

通过假设A9和A10， 表示TTP在协议执行期间对和h()的相等性进行验证，可以得到结论A CanProve (= (h))，从而可以证明该协议满足可追究性。

 

五、结束语

　　

用Kailar逻辑对电子商务协议可追究性的形式化分析过程中，需要在推理之前引入一些初始化假设，但这些初始化假设的引入是一个非形式化的过程，不恰当的引入初始化假设会导致协议的分析失败。本文通过对初始化时存在的问题的研究，提出改进，修正不适当的假设、补充新的假设，可以有效进行协议的可追究性分析。

 

作者单位：焦作大学

 

参考文献：

 

[1] Kailar R.Accountability in electronic commerce  protocols[J].IEEE Transactions on Software Engineering， 1996,（5）：313-328.

 

[2]周典萃，卿斯汉，周展飞. Kailar逻辑的缺陷[J].软件学报， 1999，10(12)：1238-1245.

 

[3] Deng， R.H.， Gong， L. Practical protocols for certified electronic mail[J].Journal of Network and Systems Management，1996，4(3)：279-297.

 

[4]郭云川，古天龙，董荣胜，蔡国永.逻辑缺陷的进一步讨论[J].计算机工程与应用，2003，17:77-79.

 

The Accountability Research on Karliar  Logic for the Analysis of Electronic Commerce Protocol

 

Liu Qinghua   Zhou Xiaoyan

 

Jiaozuo University

 

Abstract：The accountability is one of electronic commerce secure essential requirements, The Kailar logic is aims at the electronic business to be possible specially the investigation to carry on the analysis logic. However the Kailar logic also has the insufficiency， This article discussed the logical one kind of flaw initial state assumption not to be able to analyze all quarters to be possible correctly the investigation，Analyzed had this kind of flaw the reason，Proposed the improvement program.

 

Key Words： accountability； kailar logic； initial state assumption

 

 

责任编辑：紫藤