conference paper published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Vishwanath Raman author KrCh department VMCAI: Verification, Model Checking and Abstract Interpretation Modern Graph Algorithmic Techniques in Formal Verification project Rigorous Systems Engineering project Quantitative Graph Games: Theory and Applications project Microsoft Research Faculty Fellowship project 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. © 2012 Springer-Verlag. Springer2012Philadelphia, PA, USA eng 1004.269710.1007/978-3-642-27940-9_11 7148152 - 168 Chatterjee, Krishnendu, and Vishwanath Raman. “Synthesizing Protocols for Digital Contract Signing,” 7148:152–68. Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-27940-9_11">https://doi.org/10.1007/978-3-642-27940-9_11</a>. Chatterjee, Krishnendu, and Vishwanath Raman. <i>Synthesizing Protocols for Digital Contract Signing</i>. Vol. 7148, Springer, 2012, pp. 152–68, doi:<a href="https://doi.org/10.1007/978-3-642-27940-9_11">10.1007/978-3-642-27940-9_11</a>. Chatterjee K, Raman V. 2012. Synthesizing protocols for digital contract signing. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 7148, 152–168. Chatterjee, K., &#38; Raman, V. (2012). Synthesizing protocols for digital contract signing (Vol. 7148, pp. 152–168). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA: Springer. <a href="https://doi.org/10.1007/978-3-642-27940-9_11">https://doi.org/10.1007/978-3-642-27940-9_11</a> K. Chatterjee and V. Raman, “Synthesizing protocols for digital contract signing,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, Philadelphia, PA, USA, 2012, vol. 7148, pp. 152–168. Chatterjee K, Raman V. Synthesizing protocols for digital contract signing. In: Vol 7148. Springer; 2012:152-168. doi:<a href="https://doi.org/10.1007/978-3-642-27940-9_11">10.1007/978-3-642-27940-9_11</a> K. Chatterjee, V. Raman, in:, Springer, 2012, pp. 152–168. 32522018-12-11T12:02:16Z2025-06-11T08:06:25Z