{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T10:31:04Z","timestamp":1751365864936},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2012,3,21]],"date-time":"2012-03-21T00:00:00Z","timestamp":1332288000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2012,6]]},"DOI":"10.1007\/s11334-012-0180-9","type":"journal-article","created":{"date-parts":[[2012,3,20]],"date-time":"2012-03-20T03:33:49Z","timestamp":1332214429000},"page":"111-124","source":"Crossref","is-referenced-by-count":7,"title":["Game-based verification of contract signing protocols with minimal messages"],"prefix":"10.1007","volume":"8","author":[{"given":"Ying","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chenyi","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sjouke","family":"Mauw","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,3,21]]},"reference":[{"key":"180_CR1","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0012-365X(74)90116-2","volume":"10","author":"L. Adleman","year":"1974","unstructured":"Adleman L. (1974) Short permutation strings. Discrete Math 10: 197\u2013200","journal-title":"Discrete Math"},{"issue":"1","key":"180_CR2","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur R, Henzinger TA (1999) Reactive modules. Formal Methods Syst Des 15(1): 7\u201348","journal-title":"Formal Methods Syst Des"},{"key":"180_CR3","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger TA, Mang FYC, Qadeer S, Rajamani SK, Tasiran S (1998) Mocha: modularity in model checking. In: Proceedings of 10th conference on computer aided verification. LNCS, vol 1427. Springer, Berlin, pp 521\u2013525 (1998)","DOI":"10.1007\/BFb0028774"},{"issue":"5","key":"180_CR4","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur R, Henzinger TA, Kupferman O (2002) Alternating-time temporal logic. J ACM 49(5): 672\u2013713","journal-title":"J ACM"},{"key":"180_CR5","doi-asserted-by":"crossref","unstructured":"Asokan N, Schunter M, Waidner M (1997) Optimistic protocols for fair exchange. In: Proceedings of 4th ACM conference on computer and communications security. ACM, pp 7\u201317","DOI":"10.1145\/266420.266426"},{"issue":"4","key":"180_CR6","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1109\/49.839935","volume":"18","author":"N Asokan","year":"2000","unstructured":"Asokan N, Shoup V, Waidner M (2000) Optimistic fair exchange of digital signatures. Selected Areas Commun 18(4): 591\u2013606","journal-title":"Selected Areas Commun"},{"issue":"4","key":"180_CR7","doi-asserted-by":"crossref","first-page":"463","DOI":"10.3166\/jancl.19.463-487","volume":"19","author":"I Boureanu","year":"2009","unstructured":"Boureanu I, Cohen M, Lomuscio A (2009) Automatic verification of temporal-epistemic properties of cryptographic protocols. J Appl Non-Classical Logics 19(4): 463\u2013487","journal-title":"J Appl Non-Classical Logics"},{"key":"180_CR8","doi-asserted-by":"crossref","unstructured":"Chadha R, Kanovich M, Scedrov A (2001) Inductive methods and contract-signing protocols. In: Proceedings of 8th ACM conference on computer and communications security. ACM, pp 176\u2013185","DOI":"10.1145\/501983.502008"},{"issue":"1-2","key":"180_CR9","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s10817-005-9019-5","volume":"36","author":"R Chadha","year":"2006","unstructured":"Chadha R, Kremer S, Scedrov A (2006) Formal analysis of multi-party contract signing. J Autom Reason 36(1-2): 39\u201383","journal-title":"J Autom Reason"},{"issue":"2","key":"180_CR10","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/j.jlap.2004.09.003","volume":"64","author":"R Chadha","year":"2005","unstructured":"Chadha R, Mitchell JC, Scedrov A, Shmatikov V (2005) Contract signing, optimism, and advantage. J Logic Algebraic Program 64(2): 189\u2013218","journal-title":"J Logic Algebraic Program"},{"key":"180_CR11","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an open source tool for symbolic model checking. In: Proceedings of 14th conference on computer aided verification. LNCS, vol 2404. Springer, Berlin, pp 359\u2013364 (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"180_CR12","doi-asserted-by":"crossref","unstructured":"Cortier V, K\u00fcsters R, Warinschi B (2007) A cryptographic model for branching time security properties\u2014the case of contract signing protocols. In: Proceedings of 12th European symposium on research in computer security. LNCS, vol 4734. Springer, Berlin, pp 422\u2013437 (2007)","DOI":"10.1007\/978-3-540-74835-9_28"},{"key":"180_CR13","doi-asserted-by":"crossref","unstructured":"Emerson EA (1990) Temporal and modal logic. In: Handbook of theoretical computer science. MIT Press, pp 955\u20131072 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"180_CR14","doi-asserted-by":"crossref","unstructured":"K\u00e4hler D, K\u00fcsters R, Wilke T (2006) A Dolev-Yao-based definition of abuse-free protocols. In: Proceedings of 33rd colloquium on automata, languages and programming. LNCS, vol 4052. Springer, Berlin, pp 95\u2013106","DOI":"10.1007\/11787006_9"},{"key":"180_CR15","doi-asserted-by":"crossref","unstructured":"Kremer S, Raskin J-F (2002) Game analysis of abuse-free contract signing. In: Proceedings of 15th IEEE computer security foundations workshop. IEEE CS, pp 206\u2013222","DOI":"10.1109\/CSFW.2002.1021817"},{"issue":"3","key":"180_CR16","doi-asserted-by":"crossref","first-page":"399","DOI":"10.3233\/JCS-2003-11307","volume":"11","author":"S Kremer","year":"2003","unstructured":"Kremer S, Raskin J-F (2003) A game-based verification of non-repudiation and fair exchange protocols. J Comput Sec 11(3): 399\u2013430","journal-title":"J Comput Sec"},{"issue":"17","key":"180_CR17","doi-asserted-by":"crossref","first-page":"1606","DOI":"10.1016\/S0140-3664(02)00049-X","volume":"25","author":"S Kremer","year":"2002","unstructured":"Kremer S, Markowitch O, Zhou J (2002) An intensive survey of fair non-repudiation protocols. Comput Commun 25(17): 1606\u20131621","journal-title":"Comput Commun"},{"key":"180_CR18","unstructured":"Garay JA, MacKenzie PD (1999) Abuse-free multi-party contract signing. In: Proceedings of 13th symposium on distributed computing. LNCS, vol 1693. Springer, Berlin, pp 151\u2013165"},{"key":"180_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Majumdar R, Mang FYC, Raskin JF (2000) Abstract interpretation of game properties. In: Proceedings of 7th conference on statics analysis symposium. LNCS, vol 1824. Springer, Berlin, pp 220\u2013239","DOI":"10.1007\/978-3-540-45099-3_12"},{"key":"180_CR20","doi-asserted-by":"crossref","unstructured":"Liu Z, Pang J, Zhang C (2010) Extending a key-chain based certified email protocol with transparent TTP. In: Proceedings of 6th IEEE\/IFIP symposium on trusted computing and communications. IEEE CS, pp 630\u2013636","DOI":"10.1109\/EUC.2010.101"},{"key":"180_CR21","doi-asserted-by":"crossref","unstructured":"Liu Z, Pang J, Zhang C (2011) Verification of a key-chain based TTP transparent CEM protocol. In: Proceedings of 3rd workshop on harnessing theories for tool support in software. ENTCS 274. Elsevier, Amsterdam, pp 51\u201365","DOI":"10.1016\/j.entcs.2011.07.006"},{"key":"180_CR22","doi-asserted-by":"crossref","unstructured":"Lomuscio A, Qu H, Raimondi F (2009) MCMAS: a model checker for the verification of multi-agent systems. In: Proceedings of 21st conference on computer aided verification. LNCS, vol 5643. Springer, Berlin, pp 682\u2013688","DOI":"10.1007\/978-3-642-02658-4_55"},{"key":"180_CR23","doi-asserted-by":"crossref","unstructured":"Mauw S, Radomirovi\u0107 S, Torabi Dashti M (2009) Minimal message complexity of asynchronous multi-party contract signing. In: Proceedings of 22nd IEEE computer security foundations symposium. IEEE CS, pp 13\u201325","DOI":"10.1109\/CSF.2009.15"},{"issue":"2-4","key":"180_CR24","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1016\/j.ic.2007.07.007","volume":"206","author":"A Mukhamedov","year":"2008","unstructured":"Mukhamedov A, Ryan MD (2008) Fair multi-party contract signing using private contract signatures. Inf Comput 206(2-4): 272\u2013290","journal-title":"Inf Comput"},{"issue":"1\u20132","key":"180_CR25","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"LC Paulson","year":"1998","unstructured":"Paulson LC (1998) The inductive approach to verifying cryptographic protocols. J Comput Sec 6(1\u20132): 85\u2013128","journal-title":"J Comput Sec"},{"issue":"2","key":"180_CR26","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1016\/S0304-3975(01)00141-4","volume":"283","author":"V Shmatikov","year":"2002","unstructured":"Shmatikov V, Mitchell J (2002) Finite-state analysis of two contract signing protocols. Theor Comput Sci 283(2): 419\u2013450","journal-title":"Theor Comput Sci"},{"key":"180_CR27","doi-asserted-by":"crossref","unstructured":"Zhang C, Pang J (2009) How to work with honest but curious judges? (preliminary report). In: Proceedings of 7th workshop on security issues in concurrency. EPTCS 7, pp 31\u201345","DOI":"10.4204\/EPTCS.7.3"},{"key":"180_CR28","unstructured":"Zhang Y, Zhang C, Pang J, Mauw S (2009) Game-based verification of multi-party contract signing protocols. In: Proceedings of 6th workshop on formal aspects in security and trust. LNCS, vol 5983. Springer, Berlin, pp 186\u2013200"},{"key":"180_CR29","doi-asserted-by":"crossref","unstructured":"Zhang Y, Zhang C, Pang J, Mauw S (2009) Game-based verification of multi-party contract signing protocols\u2014Mocha models and ATL properties. http:\/\/satoss.uni.lu\/members\/jun\/mpcs\/","DOI":"10.1007\/978-3-642-12459-4_14"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-012-0180-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-012-0180-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-012-0180-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T17:04:53Z","timestamp":1561482293000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-012-0180-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,21]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,6]]}},"alternative-id":["180"],"URL":"https:\/\/doi.org\/10.1007\/s11334-012-0180-9","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,21]]}}}