中文摘要：

　为了描述非否认协议中的各种不确定因素，在Kailar逻辑系统中引入了表示缺省信息的否定词，以及相应的推理机制。提出了安全协议验证的新方法，主要特点是：可以直接对协议的动态运行过程进行推理；推理具有非单调性；避免过多的理想化假设；可以分析含有多个子协议的非否认协议，以及协议的可追究性和公平性。文中以一种基于离线TTP方式的非否认协议为例，验证了该协议在运行一次时具有可追究性，但多次运行时存在攻击。

英文摘要：

For the description of the nondeterministic factors in the non-repudiation protocols, the Kailar logic system extended with the default negation and the corresponding reasoning mechanism is introduced. The extended system can be used to verify security protocols and it has several main characteristics. Firstly, the method can reason not only for the results but also for the dynamic procedure of the protocol run. Secondly, the reasoning is nonmonotonic. Thirdly, the ideal assumptions of the protocols can be reduced. Fourthly, the accountability and fairness of the security protocols with some sub-protocols can be analyzed. As an example, a non-repudiation protocol with offiine TTP was verified. The protocol has accountability during one protocol run and gets the attack in the repeated runs.