Assume-guarantee synthesis for digital contract signing

K. Chatterjee, V. Raman, Formal Aspects of Computing 26 (2013) 825–859.


Journal Article | Published | English
Author
Department
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 and the trusted third party as path formulas in linear temporal logic and prove that the satisfaction of these objectives imply fairness; a property required of fair exchange protocols. We then show that weak (co-operative) co-synthesis and classical (strictly competitive) co-synthesis fail, whereas assume-guarantee synthesis (AGS) succeeds. We demonstrate the success of AGS as follows: (a) any solution of AGS is attack-free; no subset of participants can violate the objectives of the other participants; (b) the Asokan-Shoup-Waidner certified mail protocol that has known vulnerabilities is not a solution of AGS; (c) the Kremer-Markowitch non-repudiation protocol is a solution of AGS; and (d) AGS presents a new and symmetric fair non-repudiation protocol that is attack-free. To our knowledge this is the first application of synthesis to fair non-repudiation protocols, and our results show how synthesis can both automatically discover vulnerabilities in protocols and generate correct protocols. The solution to AGS can be computed efficiently as the secure equilibrium solution of three-player graph games.
Publishing Year
Date Published
2013-07-04
Journal Title
Formal Aspects of Computing
Volume
26
Issue
4
Page
825 - 859
IST-REx-ID

Cite this

Chatterjee K, Raman V. Assume-guarantee synthesis for digital contract signing. Formal Aspects of Computing. 2013;26(4):825-859. doi:10.1007/s00165-013-0283-6
Chatterjee, K., & Raman, V. (2013). Assume-guarantee synthesis for digital contract signing. Formal Aspects of Computing, 26(4), 825–859. https://doi.org/10.1007/s00165-013-0283-6
Chatterjee, Krishnendu, and Vishwanath Raman. “Assume-Guarantee Synthesis for Digital Contract Signing.” Formal Aspects of Computing 26, no. 4 (2013): 825–59. https://doi.org/10.1007/s00165-013-0283-6.
K. Chatterjee and V. Raman, “Assume-guarantee synthesis for digital contract signing,” Formal Aspects of Computing, vol. 26, no. 4, pp. 825–859, 2013.
Chatterjee K, Raman V. 2013. Assume-guarantee synthesis for digital contract signing. Formal Aspects of Computing. 26(4), 825–859.
Chatterjee, Krishnendu, and Vishwanath Raman. “Assume-Guarantee Synthesis for Digital Contract Signing.” Formal Aspects of Computing, vol. 26, no. 4, Springer, 2013, pp. 825–59, doi:10.1007/s00165-013-0283-6.

Link(s) to Main File(s)
Access Level
OA Open Access

Export

Marked Publications

Open Data IST Research Explorer

Sources

arXiv 1004.2697

Search this title in

Google Scholar