摘  要： 综合Kailar逻辑和SVO逻辑两种协议分析方法的优点，借助SVO逻辑的思想对Kailar逻辑进行了改进，使其更好地应用于不可否认协议的可追究性分析和设计。同时，将改进后的Kailar逻辑应用在类NG协议的分析中，分析结果证明了该协议可追究方面的安全性质。
关键词： 逻辑系统；Kailar逻辑；SVO逻辑；安全协议

　协议的安全性分析在安全协议的设计中起着重要的作用，Kailar逻辑的提出主要是针对电子商务协议的可追究性，但它不能分析签名的密文，对协议的证明不严格。SVO逻辑也可用于电子商务协议的形式化分析，它集成了BAN、GNY、AT等逻辑的优点，具有很好的扩展能力。本文针对Kailar逻辑的不足，借助SVO逻辑的分析思想对Kailar逻辑进行了改进和完善，使得新的Kailar逻辑能分析签名密文，严格推证协议是否具有不可否认性。
1 Kailar逻辑的基本架构
　Kailar逻辑的基本架构包含基本语句、分析假设和推理原则，限于篇幅，本文只对涉及的语句、推理原则进行说明，其他的不一一列举。

　

　图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（KB Authenticates B）；
　假设2：B Can prove（KA Authenticates A）；
　假设3：Shared（A，KAT，TTP）；
　假设4：Shared（B，KBT，TTP）；
　假设5：A Believe TTP；
　假设6：B Believe TTP。
　（2）说明协议目标
　G1：A Believe（B Received m）；
　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 Says C）（规则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（Kx Signedwith 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 of 1996 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.