Kailar逻辑的改进及应用*

翁艳琴 ，石曙东 ，解颜铭

（1.湖北师范学院 数学与统计学院，湖北 黄石 435000；2.湖北师范学院 计算机科学与技术学院，湖北 黄石 435000）

协议的安全性分析在安全协议的设计中起着重要的作用，Kailar逻辑的提出主要是针对电子商务协议的可追究性，但它不能分析签名的密文，对协议的证明不严格。SVO逻辑也可用于电子商务协议的形式化分析，它集成了BAN、GNY、AT等逻辑的优点，具有很好的扩展能力。本文针对Kailar逻辑的不足，借助SVO逻辑的分析思想对Kailar逻辑进行了改进和完善，使得新的Kailar逻辑能分析签名密文，严格推证协议是否具有不可否认性。

1 Kailar逻辑的基本架构

Kailar逻辑的基本架构包含基本语句、分析假设和推理原则，限于篇幅，本文只对涉及的语句、推理原则进行说明，其他的不一一列举。

（1）基本语句A，B，C……为参与协议的主体，通常用P指代。TTP专指可信的第三方。m为一个主体给另一个主体发送的原子消息。C为原子消息外的消息。Ki为主体i的公开密钥。Ki-1为与Ki对应的秘密私钥。x，y……为命题。

（2）基本推理原则为以下3个：

2 可追究原则的改进

本文假定发送者为A，接收者为B，可信第三方为TTP，其他符号含义同上。在Kailar逻辑中，只是涉及了接收方对发送方的主体签名的追究性，没有涉及发送方对接收方的签名的追究性，同时对第三方TTP对参与协议的其他方的追究性也没有明确的推理规则。本文借助SVO逻辑的思想，对Kailar逻辑进行了完善，改进后的推理原则如下：

（1）发送方的签名追究性

（2）接收方的签名追究性两方间：

三方间：

3 应用Kailar逻辑进行协议分析

不可否认协议（类NG协议）的交互过程如图1所示。

图1 类NG协议交互图

图1中的符号含义为：A、B为协议参与双方，TTP为可信第三方。L为协议轮标志。Na、Nb为新的随机数。SA、SB为 A、B 的私钥。 SAT、SBT分别为 A、T间共享密钥，B、T间共享密钥。Kx为 A产生的消息密钥。C=（m）Kx-1，m为发送的消息原语。此协议中A发送给B一个由Kx加密的消息C后通过第三方TTP传递Kx给B。此协议具有实现A、B、TTP间的消息可追究性的性质。

（1）协议的前提和假设

假设 1：A Can prove（KBAuthenticates B）；

假设 2：B Can prove（KAAuthenticates A）；

假设 3：Shared（A，KAT，TTP）；

假设 4：Shared（B，KBT，TTP）；

假设 5：A Believe TTP；

假设 6：B Believe TTP。

（2）说明协议目标

G2：B Believe（A Sent m）；

G3：TTP Believe（A Sent m）；

G4：TTP Believe （B Received m）。

（3）运用规则和公理进行推证协议理想化描述为：

（M1）B Received（（B，L，Na，C）Signedwith KA-1）

（M2）A Received（（A，L，Na+1，C）Signedwith KB-1）

（M3）TTP Received（（Kx，C）Signedwith KAT）

（M4）TTP Received（C Signedwith KBT）

（M5）B Received（（Kx，Nb）Signedwith KBT）

（M6）TTP Received（（Kx，Nb+1）Signedwith KBT）

（4）协议分析

①由协议描述（M2）知 A Received（C Signedwith KB-1）（规则 P14）。结合假设 1可得结论 1：A Can prove（B SaysC）（规则 P4）。 由原则 P1和 P2可 得 结论 2：A Can prove（B Sent C）。 再结合已知 A Sent（Na∧C）和A Received（Na’∧C），根据原则 P10 可得结论 3：A Can prove（B Received C）。其中，C=（m）Kx-1，即有结论 4：A Can prove（B Received m Sighned with Kx-1）。

由协议描述 （M6）知 TTP Received（（Kx）Signedwith KBT）（规则 P14）， 而由假设 4， 基于原则 P6有结论 5：TTP Can prove（B Says Kx），根据原则 P1 和 P2 有结论6：TTP Can prove（A Sent Kx）。 由结论 6 结合已知 TTP Sent（Nb∧Kx）和 TTP Received（Nb’∧Kx），运 用 原 则 10可得出结论 7：TTP Can prove（B Received Kx），结合假设 5和结论 7，运用原则 P6可得结论 8：A Can prove（B Received Kx）。结合结论 4，应用原则 P8可推出结论 9：A Can prove（B Received m），进而应用原则P13可得结论 10：A Believe（B Received m），此结论即为要达成的协议目标G1。

②由协议描述 （M1）基于规则 P14知 B Received（C Signedwith KA-1），而由假设 2，运用原则 P4可得结论 11：B Can prove（A says C），进一步运用原则 P1 和P2 可得结论12：B Can prove （A Sent C）， 而 C=（m）Kx-1，即有结论 13：B Can prove（A Sent m Sighned with Kx-1）。

由 描 述 （M3）知 TTP Received（KxSignedwith KAT），结合假设 3和规 则 P4有结论 14：TTP Can prove（A Says Kx），进一步结合假设 6，应用规则 P5有结论 15：B Can prove（A Says Kx）。 而结论 11 为 B Can prove（A says C），即 B Can prove （A Says m Sighned with Kx-1），应用原则 P9可得结论 16：B Can prove（A Says m）。进一步根据原则 P1和 P2有结论 17：B Can prove（A Sent m）， 再根据原则 P12可得结论 18：B Believe（A Sent m）。该结论即为要达成的协议目标G2。

③基本推理规则 P14，由协议描述 （M3）知 TTP Received（C Signedwith KAT），结合假设 3和规则 P7有结论 19：TTP Can prove（A Says C）， 而已有结论 14为TTP Can prove（A Says Kx），已 知 C=（m）Kx-1，故 由 P9可得结论 20：TTP Can prove（A Says m），进一步应用P1和 P2原则有结论 21：TTP Can prove （A Sent m），再基于原则 P12可得结论 22：TTP Believe（A Sent m）。结论22即为要达成的目标G3。

④由协议描述（M4）、假设 4、结论 19和原则 P11可得结论 23：TTP Can prove（B Received C），结合已知C=（m）Kx-1和结论 7， 基于原则 P8可得结论 24：TTP Can prove（B Received m），进一步基于基本推理原则P13 得出结论 25：TTP Believe（B Received m），结论 25即为要达成的目标G4。

由上述分析可知，该协议的4个目标都可满足，协议的各方的信任都可以建立，具有不可否认的性质，协议具有追究性。

基于推理结构性方法体系通常由一些命题和推理公理组成，命题表示了主体对消息的信仰或知识，运用推理公理可以从已知的知识和信仰推导出新的知识和信仰。其中，Kailar逻辑和SVO逻辑是最重要的两种方法，各具优点和不足。针对Kailar逻辑的不足，本文借助SVO逻辑的思想对其进行了改进和完善，使得它能更好地应用于协议的不可否认性和可追究性的分析。将扩展了的Kailar逻辑应用于类NG协议的可追究性的分析，证明了该协议可追究方面的安全性质。该协议分析方法简单、语义明确，为电子商务类协议的分析提供了强有力的工具。但是还有一些需要改进的地方，例如如何应用它来分析协议的公平性，如何引入恰当的初始化假设等。

[1]范红，冯登国.安全协议形式化分析的研究现状与有关问题[J].网络安全技术与应用，2001（8）：12-15.

[2]KAILAR R. Accountabitity in electronic commerce protocols[J].IEEE Transactions on Software Engineering，1996，22（5）：313-328.

[3]ZHEN J，GOLLMANN D.A fair non-repudiation protocol[J].IEEE Computer Society Symposium on Research in Security and Privacy，1996.

[4]范红，冯登国.安全协议理论与方法[M].北京：科学出版社，2003.

[5]ZHOU J，GOLLMAN D.A fair non-repudiation protocol[C].Proceeding of1996 IEEE Symposium on Security and Privacy， 1996：55-61.

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

[7]卿斯汉，常晓林，章江.安全电子商务协议 iKP I的设计和实现[C].信息和通信安全——CC ICS’99：第一届中国信息和通信安全学术会议，2000.230-239.

[8]ISO/IEC 1388822，Information technology security techniques non-repudiation part2： mechanisms using symmetrical techniques[S].International Organization for Standardization，1998.