Fair Non-repudiation Protocol Analysis Method

A fair non-repudiation protocol can prevent the correspondents from denial about the occurrence or non-occurrence of a corresponding event or action, and then ensures the fairness of the communication. So it's the base of electronic commerce protocol. Because of the importance of fair non-repudiation protocol, analysis to its security properties was a hot field in information security field during the past ten years. Currently, some formal methods have been successfully applied to the analysis of fair non-repudiation protocol. These methods are in three categories: methods base on logic reasoning; methods base on modeling and state exploration; methods of theorem proving techniques based on the Dolev-Yao model. Generally, these methods can analyze one or multiple properties of a fair non-repudiation, but heretofore, none of these methods can analyze non-repudiation, fairness and timeliness at the same time. On account of the subtle relationship between security properties of security protocol, Separate analysis to these properties is unscientific. Inside a fair non-repudiation protocol, non-repudiation, fairness and timeliness are correlative and will disturb each other in some cases. Neglect of analyzing any of these properties will probably make the analysis work skimble-skamble.Aiming at the problem mentioned above, this thesis presented a method that can analyze these three properties of non-repudiation protocol after studying these three properties'essence and summarizing the current analysis methods.The main results are as follows:1. Studied non-repudiation, fairness and timeliness'essence and summarized the principium, application, advantage and disadvantage of current fair non-repudiation protocol analysis methods.2. Presented a formal method based on provable logic that can analyze non-repudiation, fairness and timeliness. New method creates a time limit ability set for each correspondent, and follows a way that"cut off one correspondent, let others go"to analyze protocol. At the same time, it assumes that there is an attacker who also has an ability set. These make sense to examining non-repudiation, fairness and timeliness of a protocol. After introducing new method, this thesis analyzed some typical fair non-protocols using the new method and found some known and unknown flaws.3. Validated purchase phase protocol which is a sub protocol of SET protocol using new method, Analyzed non-repudiation, fairness and timeliness successfully.