{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:02:52Z","timestamp":1771700572954,"version":"3.50.1"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            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\n            <jats:italic>fairness<\/jats:italic>\n            ; a property required of fair exchange protocols. We then show that\n            <jats:italic>weak<\/jats:italic>\n            (\n            <jats:italic>co-operative<\/jats:italic>\n            )\n            <jats:italic>co-synthesis<\/jats:italic>\n            and\n            <jats:italic>classical<\/jats:italic>\n            (\n            <jats:italic>strictly competitive<\/jats:italic>\n            )\n            <jats:italic>co-synthesis<\/jats:italic>\n            fail, whereas\n            <jats:italic>assume-guarantee synthesis<\/jats:italic>\n            (\n            <jats:italic>AGS<\/jats:italic>\n            ) succeeds. We demonstrate the success of AGS as follows: (a) any solution of AGS is\n            <jats:italic>attack-free<\/jats:italic>\n            ; no subset of participants can violate the objectives of the other participants; (b) the Asokan\u2013Shoup\u2013Waidner certified mail protocol that has known vulnerabilities is not a solution of AGS; (c) the Kremer\u2013Markowitch 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.\n          <\/jats:p>","DOI":"10.1007\/s00165-013-0283-6","type":"journal-article","created":{"date-parts":[[2013,6,5]],"date-time":"2013-06-05T11:00:58Z","timestamp":1370430058000},"page":"825-859","source":"Crossref","is-referenced-by-count":8,"title":["Assume-guarantee synthesis for digital contract signing"],"prefix":"10.1145","volume":"26","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria (Institute of Science and Technology Austria), Klosterneuburg, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vishwanath","family":"Raman","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, P.O. Box 1, Silicon Valley Campus, NASA Research Park, Bldg. 23 (MS 23-11), 94035-0001, Moffett Field, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Armando A Carbone R Compagna L (2007) LTL model checking for security protocols. In: CSF pp 385\u2013396","DOI":"10.1109\/CSF.2007.24"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Alur R Henzinger TA Mang FYC Qadeer S Rajamani SK Tasiran S (1998) Mocha: modularity in model checking. In: CAV pp 521\u2013525","DOI":"10.1007\/BFb0028774"},{"key":"e_1_2_1_2_3_2","unstructured":"Asokan N Shoup V Waidner M (1998) Asynchronous protocols for optimistic fair exchange. In: IEEE S&P pp 86\u201399"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Alcaide A Tapiador JM Hernandez-Castro JC Ribagorda A (2008) Nature\u2014inspired synthesis of rational protocols. In: Proceedings of the 10th international conference on parallel problem solving from nature: PPSN X. Springer Berlin pp 981\u2013990","DOI":"10.1007\/978-3-540-87700-4_97"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/77648.77649"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Clarke EM Emerson EA (1982) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of programs workshop. Springer Berlin pp 52\u201371","DOI":"10.1007\/BFb0025774"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Chatterjee K Henzinger TA (2007) Assume-guarantee synthesis. In: TACAS pp 261\u2013275","DOI":"10.1007\/978-3-540-71209-1_21"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Chatterjee K Henzinger M (2012) An o ( n 2 ) time algorithm for alternating B\u00fcchi games. In: SODA pp 1386\u20131399","DOI":"10.1137\/1.9781611973099.109"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.032"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Chadha R Kanovich MI Scedrov A (2001) Inductive methods and contract-signing protocols. In: CCS. ACM New York pp 176\u2013185","DOI":"10.1145\/501983.502008"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9019-5"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Chadha R Mitchell JC Scedrov A Shmatikov V (2003) Contract signing optimism and advantage. In: CONCUR pp 361\u2013377","DOI":"10.1007\/978-3-540-45187-7_24"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"de Alfaro L Henzinger TA (2001) Interface automata. In: Proceedings of the 8th European software engineering conference and the 9th ACM SIGSOFT symposium on the foundations of software engineering (ESEC\/FSE). ACM Press New York pp 109\u2013120","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_2_14_2","unstructured":"Even S Yacobi Y (1980) Relations among public key signature systems technical report 175. Technical report Technion Haifa Israel"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Garay JA Jakobsson M MacKenzie PD (1999) Abuse-free optimistic contract signing. In: CRYPTO pp 449\u2013466","DOI":"10.1007\/3-540-48405-1_29"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0140-3664(02)00049-X"},{"key":"e_1_2_1_2_17_2","unstructured":"Kremer S Raskin J-F (2002) Game analysis of abuse-free contract signing. In: CSFW. IEEE New York pp 206\u2013220"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.5555\/876661.876668"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/505672.505676"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Markowitch O Gollmann D Kremer S (2002) On fairness in exchange protocols. In: ICISC pp 451\u2013464","DOI":"10.1007\/3-540-36552-4_31"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Markowitch O Kremer S (2001) An optimistic non-repudiation protocol with transparent trusted third party. In: ISC pp 363\u2013378","DOI":"10.1007\/3-540-45439-X_25"},{"key":"e_1_2_1_2_22_2","volume-title":"The temporal logic of reactive and concurrent systems: specification","author":"Manna Z","year":"1991"},{"key":"e_1_2_1_2_23_2","volume-title":"On the impossibility of fair exchange without a trusted third party","author":"Pagnia H","year":"1999"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE symposium on foundations of computer science. IEEE Computer Society Press New York pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Pnueli A Rosner R (1989) On the synthesis of a reactive module. In: POPL. ACM Press New York pp 179\u2013190","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_2_26_2","unstructured":"Perrig A Song DX (2000) A first step towards the automatic generation of security protocols. In: NDSS"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"e_1_2_1_2_28_2","unstructured":"Saidi H (2002) Toward automatic synthesis of security protocols. AAAI Technical Report SS-02-05"},{"key":"e_1_2_1_2_29_2","first-page":"2001","article-title":"Athena: a novel approach to efficient automatic security protocol analysis","volume":"9","author":"Song D","year":"2001","journal-title":"J Comput Secur"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00141-4"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1999-72-304"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Thomas W (1997) Languages automata and logic. Handbook of formal languages: beyond words vol 3 pp 389\u2013455","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Zhou J Deng RH Bao F (2000) Some remarks on a fair exchange protocol. In: Public key cryptography pp 46\u201357","DOI":"10.1007\/978-3-540-46588-1_4"},{"key":"e_1_2_1_2_34_2","unstructured":"Zhou J Gollmann D (1997) An efficient non-repudiation protocol. In: PCSFW. IEEE Computer Society Press New York pp 126\u2013132"},{"key":"e_1_2_1_2_35_2","unstructured":"Zhou J Gollmann D (1998) Towards verification of non-repudiation protocols. In: Proceedings of 1998 international refinement workshop and formal methods Pacific. Springer Berlin pp 370\u2013380"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-013-0283-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-013-0283-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-013-0283-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:04:14Z","timestamp":1641485054000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-013-0283-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1007\/s00165-013-0283-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-013-0283-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7]]}}}