Abstract: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 offline TTP was verified. The protocol has accountability during one protocol run and gets the attack in the repeated runs.