2010/04/15 by Krishnendu Chatterjee, Chatterjee, Krishnendu, Vishwanath Raman +1
Computer Science · Social Sciences · #Access Control and Trust #Blockchain Technology Applications and Security #Computer Science and Game Theory (cs.GT) #Cryptography and Data Security #Cryptography and Security (cs.CR) #F.1.2 #F.3.1 #FOS: Computer and information sciences #I.6.5 #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #cs.CR #cs.GT #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.1004.2697
40 pages, 1 figure, 3 tables and 3 algorithms
openalex publication_date 2010/04/15 · arxiv created 2011/11/13 · arxiv updated 2011/11/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
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 (TTP) as path formulas in LTL 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 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; (b) the Asokan-Shoup-Waidner (ASW) certified mail protocol that has known vulnerabilities is not a solution of AGS; (c) the Kremer-Markowitch (KM) 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 assume-guarantee synthesis can be computed efficiently as the secure equilibrium solution of three-player graph games.