Abstract
Optimistic contract signing protocols may involve subproto- cols that allow a contract to be signed normally or aborted or resolved by a third party. Since there are many ways these subprotocols might interact, protocol analysis involves consideration of a number of complicated cases. With the help of Murϕ, a finite-state verification tool, we analyze the abuse-free optimistic contract signing protocol of Garay, Jakobsson, and MacKenzie. In addition to verifying a number of subtle properties, we discover an attack in which negligence or corruption of the trusted third party may allow abuse or unfairness. Contrary to the intent of the protocol, the cheated party is not able to hold the third party accountable. In addition to analyzing a modification to the protocol that avoids these problems, we discuss issues involved in the application of finite- state analysis to fair exchange protocols, in particular models of fairness guarantees, abuse, and corrupt protocol participants.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
N. Asokan, V. Shoup, and M. Waidner. Asynchronous protocols for optimistic fair exchange. In Proc. IEEE Symposium on Research in Security and Privacy, pages 86–99, 1998.
N. Asokan, V. Shoup, and M. Waidner. Fair exchange of digital signatures. Technical Report RZ2973, IBM Research Report. Extended abstract in Eurocrypt’ 98, 1998.
E. F. Brickell, D. Chaum, I. B. Damgard, and J. van de Graaf. Gradual and verifiable release of a secret. In Proc. Advances in Cryptology-Crypto’ 87, pages 156–166, 1987.
Feng Bao, R. H. Deng, and Wenbo Mao. Efficient and practical fair exchange protocols with off-line TTP. In Proc. IEEE Symposium on Research in Security and Privacy, pages 77–85, 1998.
M. Ben-Or, O. Goldreich, S. Micali, and R. L. Rivest. A fair protocol for signing contracts. IEEE Transactions on Information Theory, 36(1):40–46, 1990.
D. Bolignano. Towards a mechanization of cryptographic protocol verifi-cation. In Proc. 9th International Conference on Computer Aided Verification, pages 131–142, 1997.
A. Bahreman and J. D. Tygar. Certified electronic mail. In Proc. Internet Society Symposium on Network and Distributed Systems Security, pages 3–19, 1994.
D. Chaum, A. Fiat, and M. Naor. Untraceable electronic cash. In Proc. Advances in Cryptology-Crypto’ 88, pages 319–327, 1988.
B. Cox, J. D. Tygar, and M. Sirbu. NetBill security and transactio protocol. In Proc. 1st USENIX Workshop on Electronic Commerce, pages 77–88, 1995.
R. H. Deng, Li Gong, A. A. Lazar, and Weiguo Wang. Practical protocols for certified electronic mail. J. Network and Systems Management, 4(3):279–297, 1996.
D. Dill. The Murφ verification system. In Proc. 8th International Conference on Computer Aided Verification, pages 390–393, 1996.
M. Franklin and M. Reiter. Fair exchange with a semi-trusted third party. In Proc. Jjih ACM Conference on Computer and Communications Security, pages 1–6. ACM Press, 1997.
J. A. Garay, M. Jakobsson, and P. MacKenzie. Abuse-free optimistic contract signing. In Proc. Advances in Cryptology-Crypto’ 99, pages 449–466, 1999.
N. Heintze, J. D. Tygar, J. M. Wing, and H.-C. Wong. Model checking electronic commerce protocols. In Proc. USENIX 1996 Workshop on Electronic Commerce, pages 147–164, 1996.
R. Kemmerer, C. Meadows, and J. Millen. Three systems for cryptographic protocol analysis. J. Cryptology, 7(2):79–130, 1994.
G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In Proc. 2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 147–166. Springer-Verlag, 1996.
P. MacKenzie. Email communication, September 23, 1999.
W. Marrero, E. M. Clarke, and S. Jha. Model checking for security protocols. Technical ReportCMU-SCS-97-139, Carnegie Mellon University, May 1997.
C. Meadows. Analyzing the Needham-Schroeder public-key protocol: A comparison of two approaches. In Proc. European Symposium On Research In Computer Security, pages 365–384. Springer-Verlag, 1996.
C. Meadows. The NRL Protocol Analyzer: An overview. J. Logic Programming, 26(2):113–131, 1996.
J. C. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using Murφ. In Proc. IEEE Symposium on Research in Security and Privacy, pages 141–151. IEEE Computer Society Press, 1997.
J. C. Mitchell, V. Shmatikov, and U. Stern. Finite-state analysis of SSL 3.0. In Proc. 7th USENIX Security Symposium, pages 201–215, 1998.
L. Paulson. The inductive approach to verifying cryptographic protocols. J. Computer Security, 6:85–128, 1998.
A. W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR. In Proc. 8th IEEE Computer Security Foundations Workshop, pages 98–107. IEEE Computer Society Press, 1995.
V. Shmatikov and J. C. Mitchell. Analysis of a fair exchange protocol. In Proc. Internet Society Symposium on Network and Distributed Systems Security, 2000. to appear.
V. Shmatikov and U. Stern. Efficient finite-state analysis for large security protocols. In Proc. 11th IEEE Computer Security Foundations Workshop, pages 106–115, 1998.
J. Zhou and D. Gollmann. A fair non-repudiation protocol. In Proc. IEEE Symposium on Research in Security and Privacy, pages 55–61. IEEE Computer Society Press, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shmatikov, V., Mitchell, J.C. (2001). Analysis of Abuse-Free Contract Signing. In: Frankel, Y. (eds) Financial Cryptography. FC 2000. Lecture Notes in Computer Science, vol 1962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45472-1_13
Download citation
DOI: https://doi.org/10.1007/3-540-45472-1_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42700-1
Online ISBN: 978-3-540-45472-4
eBook Packages: Springer Book Archive