翁艳琴 ，石曙东 ，解颜铭

（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）接收方的签名追究性两方间：

三方间：