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]
References
[1]
S. Gritzalis, D. Spinellis, and P. Georgiadis, “Security protocols over open networks and distributed systems: formal methods for their analysis, design, and verification,” Computer Communications, vol. 22, no. 8, pp. 697–709, 1999.
[2]
R. Kailar, “Accountability in electronic commerce protocols,” IEEE Transactions on Software Engineering, vol. 22, no. 5, pp. 313–328, 1996.
[3]
L. Botao and L. Junzhou, “On timeliness of a fair non-repudiation protocol,” in Proceedings of the 3rd International Conference on Information Security (InfoSecu '04), pp. 99–106, Shanghai, China, November 2004.
[4]
Y. Xu and X. Xie, “Analysis of electronic commerce protocols based on extended rubin logic,” in Proceedings of the 9th International Conference for Young Computer Scientists (ICYCS '08), pp. 2079–2084, Hunan, China, November 2008.
[5]
W. Jamroga, S. Mauw, and M. Melissen, “Fairness in non-repudiation protocols,” in Proceedings of the 7th International workshop on security and trust management, pp. 122–139, Copenhagen, Denmark, June 2011.
[6]
S. Kremer and J. F. Raskin, “A game-based verification of non-repudiation and fair exchange protocols,” in CONCUR, 2001—Concurrency Theory, pp. 551–565, Springer, Berlin, Heidelberg, 2001.
[7]
R. Lanotte, A. Maggiolo-Schettini, and A. Troina, “Automatic analysis of a non-repudiation protocol,” Electronic Notes in Theoretical Computer Science, vol. 112, pp. 113–129, 2005.
[8]
Y. Guo, C. Lin, and H. Yin, “Formal proof of the IDOP-SP protocol based on the Petri Net,” in Proceedings of the IEEE International Conference on Networking, Architecture, and Storage (IEEE NAS '08), pp. 161–162, Chongqing, June 2008.
[9]
L. Chen and X. Li, “Cryptographic protocol logic for analyzing a variety of security properties and its formal semantics,” International Journal of Advancements in Computing Technology, vol. 4, no. 9, pp. 283–293, 2012.
[10]
J. Dreier, P. Lafourcade, and Y. Lakhnech, “Formal verification of e-Auction protocols,” in Proceedings of the 2nd International Conference on Principles of Security and Trust, pp. 247–266, Rome, Italy, 2013.
[11]
H. Zhang, “Analysis on authentication secrecy of non-repudiation protocols,” in Proceedings of the International Conference on Electrical and Electronics Engineering, pp. 705–711, Wuhan, China, 2011.
[12]
G. Draper-Gil, J. Zhou, J. L. Ferrer-Gomila, and M. F. Hinarejos, “An optimistic fair exchange protocol with active intermediaries,” International Journal of Information Security, vol. 12, no. 4, pp. 299–318, 2013.
[13]
S. Kremer and O. A. Markowitch, “Multi-party non-repudiation protocol,” in Proceedings of the 15th International Conference on Information Security, pp. 271–280, Beijing, China, 2000.
[14]
J. Zhou, J. Onieva, and J. Lopez, “Optimized multi-party certified email protocols,” Information Management and Computer Security, vol. 13, no. 5, pp. 350–366, 2005.
[15]
F. J. T. Fabrega, J. C. Herzog, and J. D. Guttman, “Strand spaces: Why is a security protocol correct,” in Proceedings of the IEEE Symposium on Security and Privacy, pp. 160–171, Oakland, Calif, USA, 1998.
[16]
K. Kim, S. Park, and J. Baek, “Improving fairness and privacy of Zhou-Gollmanns fair non-repudiation protocol,” in Proceedings of the International Workshops on Parallel Processing, pp. 140–145, IEEE Computer Society Press, 1999.
[17]
J. Zhou and D. Gollmann, “Fair non-repudiation protocol,” in Proceedings of the 17th IEEE Symposium on Security and Privacy, pp. 55–61, May 1996.
