|
|
A New Verification Method for Non-repudiation Protocol |
Zhou Yong; Zhu Wu-jia |
College of Information Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China |
|
|
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.
|
Received: 29 March 2006
|
|
|
|
|
|
|
|