Part of the book series:Lecture Notes in Computer Science ((LNTCS,volume 7148))
Included in the following conference series:
953Accesses
Abstract
We study the automatic synthesis of fair non-repudiation protocols, a class of fair exchange protocols, used for digital contract signing. First, we show how to specify the objectives of the participating agents, the trusted third party (TTP) and the protocols as path formulas in Linear Temporal Logic (LTL) and prove that the satisfaction of the objectives of the agents and the TTP imply satisfaction of the protocol objectives. We then show thatweak (co-operative) co-synthesis andclassical (strictly competitive) co-synthesis fail in synthesizing these protocols, whereasassume-guarantee synthesis (AGS) succeeds. We demonstrate the success of assume-guarantee synthesis as follows: (a) any solution of assume-guarantee synthesis is attack-free; no subset of participants can violate the objectives of the other participants without violating their own objectives; (b) the Asokan-Shoup-Waidner (ASW) certified mail protocol that has known vulnerabilities is not a solution of AGS; and (c) the Kremer-Markowitch (KM) non-repudiation protocol is a solution of AGS. To our knowledge this is the first application of synthesis to fair non-repudiation protocols, and our results show how synthesis can generate correct protocols and automatically discover vulnerabilities. The solution to assume-guarantee synthesis can be computed efficiently as the secure equilibrium solution of three-player graph games.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5719
- Price includes VAT (Japan)
- Softcover Book
- JPY 7149
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: Mocha: Modularity in Model Checking. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
Asokan, N., Shoup, V., Waidner, M.: Asynchronous protocols for optimistic fair exchange. In: IEEE S&P, pp. 86–99 (1998)
Chadha, R., Kanovich, M.I., Scedrov, A.: Inductive methods and contract-signing protocols. In: CCS, pp. 176–185. ACM (2001)
Chadha, R., Mitchell, J.C., Scedrov, A., Shmatikov, V.: Contract Signing, Optimism, and Advantage. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 366–382. Springer, Heidelberg (2003)
Chatterjee, K., Henzinger, T.A.: Assume-Guarantee Synthesis. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 261–275. Springer, Heidelberg (2007)
Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Games with secure equilibria. Theor. Comput. Sci. 365(1-2), 67–82 (2006)
Chatterjee, K., Raman, V.: Assume-guarantee synthesis for digital contract signing. CoRR, abs/1004.2697 (2010)
Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic. In: Engeler, E. (ed.) Logic of Programs 1979. LNCS, vol. 125, pp. 52–71. Springer, Heidelberg (1981)
Even, S., Yacobi, Y.: Relations among public key signature systems, technical report 175. Technical report, Technion, Haifa, Israel (1980)
Garay, J.A., Jakobsson, M., MacKenzie, P.D.: Abuse-Free Optimistic Contract Signing. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 449–466. Springer, Heidelberg (1999)
Kremer, S., Raskin, J.-F.: Game analysis of abuse-free contract signing. In: CSFW, pp. 206–220. IEEE (2002)
Kremer, S., Raskin, J.-F.: A game-based verification of non-repudiation and fair exchange protocols. JCS 11(3), 399–430 (2003)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1991)
Markowitch, O., Gollmann, D., Kremer, S.: On Fairness in Exchange Protocols. In: Lee, P.J., Lim, C.H. (eds.) ICISC 2002. LNCS, vol. 2587, pp. 451–464. Springer, Heidelberg (2003)
Markowitch, O., Kremer, S.: An Optimistic Non-repudiation Protocol with Transparent Trusted Third Party. In: Davida, G.I., Frankel, Y. (eds.) ISC 2001. LNCS, vol. 2200, pp. 363–378. Springer, Heidelberg (2001)
Pagnia, H., Gärtner, F.C.: On the impossibility of fair exchange without a trusted third party. Technical report, Darmstadt (1999)
Perrig, A., Song, D.X.: A first step towards the automatic generation of security protocols. In: NDSS (2000)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. Found. of Comp. Sci., pp. 46–57. IEEE Computer Society Press (1977)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190. ACM Press (1989)
Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes. Siam J. Control and Optimization 25(1) (1987)
Saïdi, H.: Toward automatic synthesis of security protocols. AAAI Technical Report, SS-02-05 (2002)
Shmatikov, V., Mitchell, J.C.: Finite-state analysis of two contract signing protocols. Theor. Comput. Sci. 283(2), 419–450 (2002)
Song, D., Berezin, S., Perrig, A.: Athena: a novel approach to efficient automatic security protocol analysis. JCS 9 (2001)
Thomas, W.: Languages, automata, and logic, pp. 389–455 (1997)
Zhou, J., Gollmann, D.: An efficient non-repudiation protocol. In: PCSFW, pp. 126–132. IEEE Computer Society Press (1997)
Author information
Authors and Affiliations
IST (Institute of Science and Technology Austria), Austria
Krishnendu Chatterjee
Carnegie Mellon Silicon Valley, Moffett Field, USA
Vishwanath Raman
- Krishnendu Chatterjee
You can also search for this author inPubMed Google Scholar
- Vishwanath Raman
You can also search for this author inPubMed Google Scholar
Editor information
Editors and Affiliations
Swiss Federal Institute of Technology Lausanne (EPFL), IC IIF LARA INR 318, Station 14, 1015, Lausanne, Switzerland
Viktor Kuncak
Institut für Informatik, Technische Universität München, Boltzmannstr. 3, 85748, Munich, Germany
Andrey Rybalchenko
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chatterjee, K., Raman, V. (2012). Synthesizing Protocols for Digital Contract Signing. In: Kuncak, V., Rybalchenko, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2012. Lecture Notes in Computer Science, vol 7148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27940-9_11
Download citation
Publisher Name:Springer, Berlin, Heidelberg
Print ISBN:978-3-642-27939-3
Online ISBN:978-3-642-27940-9
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative