---
_id: '3252'
abstract:
- lang: eng
  text: '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.'
acknowledgement: "The research was supported by Austrian Science Fund (FWF) Grant
  No P 23499-N23 (Modern Graph Algorithmic Techniques in Formal Verification), FWF
  NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft
  faculty fellows award.\r\nThe authors would like to thank Avik Chaudhuri for his
  invaluable help and feedback."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Vishwanath
  full_name: Raman, Vishwanath
  last_name: Raman
citation:
  ama: '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>'
  apa: '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>'
  chicago: 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>.
  ieee: '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.'
  ista: 'Chatterjee K, Raman V. 2012. Synthesizing protocols for digital contract
    signing. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS,
    vol. 7148, 152–168.'
  mla: 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>.
  short: K. Chatterjee, V. Raman, in:, Springer, 2012, pp. 152–168.
conference:
  end_date: 2012-01-24
  location: Philadelphia, PA, USA
  name: 'VMCAI: Verification, Model Checking and Abstract Interpretation'
  start_date: 2012-01-22
date_created: 2018-12-11T12:02:16Z
date_published: 2012-01-20T00:00:00Z
date_updated: 2025-06-11T08:06:25Z
day: '20'
department:
- _id: KrCh
doi: 10.1007/978-3-642-27940-9_11
ec_funded: 1
external_id:
  arxiv:
  - '1004.2697'
intvolume: '      7148'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1004.2697
month: '01'
oa: 1
oa_version: Preprint
page: 152 - 168
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Springer
publist_id: '3405'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesizing protocols for digital contract signing
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7148
year: '2012'
...