%0 Journal Article
%T Fairness Analysis for Multiparty Nonrepudiation Protocols Based on Improved Strand Space
%A Lei Li
%A Licheng Wang
%A Jing Chen
%A Ruiming Wang
%A Zhihong Zhang
%J Discrete Dynamics in Nature and Society
%D 2014
%I Hindawi Publishing Corporation
%R 10.1155/2014/904717
%X Aimed at the problem of the fairness analysis for multiparty nonrepudiation protocols, a new formal analysis method based on improved strand space is presented. Based on the strand space theory, signature operation is added; the set of terms, the subterm relation and the set of penetrator traces are redefined and the assumption of free encryption is extended in the new method. The formal definition of fairness in multi-party non-repudiation protocols is given and the guideline to verify it based on improved strand space is presented. Finally, the fairness of multi-party non-repudiation protocols is verified with an example of Kremer-Markowitch protocol, which indicates that the new method is suitable for analyzing the fairness of multiparty nonrepudiation protocols. 1. Introduction As a crucial foundation of the realization of electronic commerce, nonrepudiation protocols provide the nonrepudiation services for the interbehavior between the network entities. Generally speaking, some security properties of the nonrepudiation protocols should be equipped with such as nonrepudiation, fairness, and timeliness, among which the fairness acts as the most important one. The nonrepudiation protocols are usually the ones being of one sender and multireceptors. Formal methods, theory, and supporting tools paly an important role in the design, analysis, and verification of the security-related and cryptographic protocols [1]. There are numbers of approaches for analyzing the security protocol; however, it turns out to be that each one is subjected to its own limitations since it can only analyze a certain class of protocols or security properties. During the period of designing the security protocols, it is required to guarantee the security properties of security protocol as much as possible by applying multikinds of formal analysis methods. Currently, the formal analysis methods based on nonrepudiation protocols can be divided into two classes.(1)Belief logic method: in [2], Kailar firstly extended the BAN logic and applied it to the analysis of fairness of the nonrepudiation protocols; the authors in [3, 4] analyzed the fairness and timeliness of the nonrepudiation protocols by using belief logic, respectively. In [5, 6], the authors introduced the alternating-time temporal logic analyzing the fairness of the nonrepudiation protocols. However, the formal analysis based on the belief logic method only works under a lot of assumptions.(2)State space method: the automatic analysis method with a protocol checker adopted in [7] and Petri net method proposed in [8]
%U http://www.hindawi.com/journals/ddns/2014/904717/