电子商务协议可追究性的Ｋａｉｌａｒ分析与改进

　　摘要：可追究性是电子商务安全性的基本要求之一，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