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 that weak (co-operative) co-synthesis and classical (strictly competitive) co-synthesis fail in synthesizing these protocols, whereas assume-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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
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
Editor information
Editors and Affiliations
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
DOI: https://doi.org/10.1007/978-3-642-27940-9_11
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)