Research On Verification Technology For Non-Repudiation And Fairness Of Cryptographic Protocols

With the development of military information construction process, attacks from the internal entities become a serious threat to the information security. Non-repudiation and fairness properties mainly solve the attacks from the internal entities. Over the past decade, the development of formal methods for protocol analysis has mainly concentrated on the secrecy and authenticity properties. Formal analysis for non-repudiation and fairness properties is a new trend, which is still at the elementary stage.This paper studies the verification technology for non-repudiation and fairness, Based on first-order logic, we propose a new method special for non-repudiation and fairness, and realize the automatic verification for non-repudiation protocols successfully using our method.The main works and creations are as the following:1. Introduce the existing formal methods for non-repudiation and fairness, compare them, and point out the advantages and disadvantages of each method.2. Propose a set of syntax and semantics of first-order logic for non-repudiation and fairness.3. Propose a modeling method for non-repudiation based on first-order logic, modle the factors separately, and define the non-repudiation and fairness by first-order logic. This is the focus of the paper.4. Progress a manual analysis for ZG non-repudiation protocol using our first- order logic model, and a known attack is found. It proves the correctness, efficiency and advantages of our model.5. Design the automatic verification algorithms of non-repudiation and fairness based on the model, adding some necessary strategies to reduce the complexity of the algorithms, and avoid non-termination situations. This is the difficult part of the paper.6. Design and implement a prototype system called AVT-NR based on the model and verification algorithms. Simply introduce its architecture and the work flow, mainly discuss the realization details of each part, and verify the ZG non-repudiation protocol, ZG optimistic non-repudiation protocol, KM non-repudiation protocol and some other non-repudiation protocols successfully by this system, which further verifies the correctness and efficiency of our new method.