×

Formal analysis of fairness for optimistic multiparty contract signing protocol. (English) Zbl 1442.94041

Summary: Optimistic multiparty contract signing (OMPCS) protocols are proposed for exchanging multiparty digital signatures in a contract. Compared with general two-party exchanging protocols, such protocols are more complicated, because the number of protocol messages and states increases considerably when signatories increase. Moreover, fairness property in such protocols requires protection from each signatory rather than from an external hostile agent. It thus presents a challenge for formal verification. In our analysis, we employ and combine the strength of extended modeling language CSP\(\#\) and linear temporal logic (LTL) to verify the fairness of OMPCS protocols. Furthermore, for solving or mitigating the state space explosion problem, we set a state reduction algorithm which can decrease the redundant states properly and reduce the time and space complexity greatly. Finally, this paper illustrates the feasibility of our approach by analyzing the GM and CKS protocols, and several fairness flaws have been found in certain computation times.

MSC:

94A60 Cryptography
68M12 Network protocols

Software:

PAT
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Asokan, N.; Schunter, M.; Waidner, M., Optimistic protocols for fair exchange, Proceedings of the 4th ACM Conference on Computer and Communications Security
[2] Even, S.; Yacobi, Y., Relations among public key signatures systems, 175 (1980), Haifa, Israel: Technion, Haifa, Israel
[3] Mauw, S.; Radomirović, S.; Dashti, M. T., Minimal message complexity of asynchronous multi-party contract signing, Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF ’09), IEEE Computer Society Press · doi:10.1109/CSF.2009.15
[4] Mukhamedov, A.; Ryan, M. D., Resolve-impossibility for a contract-signing protocol, Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW ’06) · doi:10.1109/CSFW.2006.27
[5] Asokan, N., Fairness in electronic commerce [Ph.D. thesis] (1998), University of Waterloo
[6] Chadha, R.; Kremer, S.; Scedrov, A., Formal analysis of multi-party contract signing, Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW ’04), IEEE Computer Society Press
[7] Zhang, Y.; Zhang, C.; Pang, J.; Mauw, S., Game-based verification of contract signing protocols with minimal messages, Innovations in Systems and Software Engineering, 8, 2, 111-124 (2012) · doi:10.1007/s11334-012-0180-9
[8] Mukhamedov, A.; Ryan, M. D., Fair multi-party contract signing using private contract signatures, Information and Computation, 206, 2-4, 272-290 (2008) · Zbl 1148.68326 · doi:10.1016/j.ic.2007.07.007
[9] Mauw, S.; Radomirović, S.; Dashti, M. T., Minimal message complexity of asynchronous multi-party contract signing, Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF ’09), IEEE CS · doi:10.1109/CSF.2009.15
[10] Mukhamedov, A.; Kremer, S.; Ritter, E., Analysis of a multi-party fair exchange protocol and formal proof of correctness in the strand space model, Financial Cryptography and Data Security. Financial Cryptography and Data Security, Lecture Notes in Computer Science, 3570, 255-269 (2005) · Zbl 1120.94329 · doi:10.1007/11507840_23
[11] Zhang, N.; Zhang, X.; Wang, Y., Formal analysis of GM multi-party contract signing protocol, Proceedings of the 2nd International Conference on Convergent Information Technology (ICCIT ’07), IEEE Computer Society Press · doi:10.1109/ICCIT.2007.4420438
[12] Sun, J.; Liu, Y.; Jin, S. D.; Chen, C., Integrating specification and programs for system modeling and verification, Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE ’09) · doi:10.1109/TASE.2009.32
[13] Pnueli, A., The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS ’77)
[14] Garay, J. A.; Mackenzie, P., Abuse-free multi-party contract signing, Distributed Computing. Distributed Computing, Lecture Notes in Computer Science, 1693, 151-165 (1999) · doi:10.1007/3-540-48169-9_11
[15] Liu, Y.; Sun, J.; Dong, J. S., PAT 3: an extensible architecture for building multi-domain model checkers, Proceedings of the 22nd IEEE International Symposium on Software Reliability Engineering (ISSRE ’11) · doi:10.1109/ISSRE.2011.19
[16] Cheval, V.; Blanchet, B., Proving more observational equivalences with ProVerif, Principles of Security and Trust. Principles of Security and Trust, Lecture Notes in Computer Science, 7796, 226-246 (2013), Springer · Zbl 1391.94737 · doi:10.1007/978-3-642-36830-1_12
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.