{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:38:02Z","timestamp":1778297882230,"version":"3.51.4"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Know. Inf. Sys."],"published-print":{"date-parts":[[2005,1]]},"DOI":"10.1007\/s10115-003-0127-4","type":"journal-article","created":{"date-parts":[[2004,7,22]],"date-time":"2004-07-22T07:47:42Z","timestamp":1090482462000},"page":"84-109","source":"Crossref","is-referenced-by-count":3,"title":["ENDL: A Logical Framework for Verifying Secure Transaction Protocols"],"prefix":"10.1007","volume":"7","author":[{"given":"Qingfeng","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chengqi","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shichao","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,1,1]]},"reference":[{"key":"127_CR1","doi-asserted-by":"crossref","unstructured":"Abadi M, Tuttle M (1991) A semantics for a logic of authentication. In: Proceedings of the 10th ACM Symposium on Principles of Distributed Computing. ACM Press, pp 201\u2013216","DOI":"10.1145\/112600.112618"},{"key":"127_CR2","unstructured":"Bai S, Chen QF (2002) The verification logic for secure electronic protocols. J Software (China) 11(2):213\u2013221"},{"key":"127_CR3","doi-asserted-by":"crossref","unstructured":"Bella G, Massacci F, Paulson L, Tramontano P (2000) Formal Verification of cardholder registration in SET. In: Proceedings of the 6th European Symposium on Research in Computer Security (ESORICS\u201900), Lecture Notes in Computer Science. Springer-Verlag, Berlin, pp 159\u2013174","DOI":"10.1007\/10722599_10"},{"key":"127_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/214451.214452","volume":"3","author":"Birrell","year":"1985","unstructured":"Birrell A (1985) Secure communications using remote procedure calls. ACM Trans Comput Syst 3(1):1\u201314","journal-title":"ACM Trans Comput Syst"},{"key":"127_CR5","doi-asserted-by":"crossref","unstructured":"Brackin S (1996) A HOL extension of GNY for automatically analyzing cryptographic protocols. In: Proceeding of the Ninth IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, pp 62\u201376","DOI":"10.1109\/CSFW.1996.503691"},{"key":"127_CR6","unstructured":"Brackin S (1997) Automatic formal analyses of two large commercial protocols. In: Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols (paper available at http:\/\/dimacs.rutgers.edu\/Workshops\/Security\/ program2\/brackin.html)"},{"key":"127_CR7","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"Burrows","year":"1990","unstructured":"Burrows M, Abadi M, Needham R (1990) A logic for authentication. ACM Trans Comput Syst 8(1):18\u201336","journal-title":"ACM Trans Comput Syst"},{"key":"127_CR8","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1145\/358722.358740","volume":"24","author":"Denning","year":"1981","unstructured":"Denning D, Sacco G (1981) Timestamp in key distribution protocols. Commun ACM 24(8):533\u2013536","journal-title":"Commun ACM"},{"key":"127_CR9","doi-asserted-by":"crossref","unstructured":"Dierks T, Allen C (1999) http:\/\/www.ietf.org\/rfc\/rfc2246.txt","DOI":"10.17487\/rfc2246"},{"key":"127_CR10","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"Dolev","year":"1983","unstructured":"Dolev D, Yao A (1983) On the security of public key protocols. IEEE Trans Inf Theory 29(2):198\u2013208","journal-title":"IEEE Trans Inf Theory"},{"key":"127_CR11","unstructured":"Foner LN (1996) A security architecture for multi-agent matchmaking. In: Proceedings of the Second International Conference on Multi-Agent Systems (ICMAS96). AAAI Press, Menlo Park, CA, pp 80\u201386"},{"key":"127_CR12","doi-asserted-by":"crossref","unstructured":"Forrester (1998) http:\/\/www.forrester.com\/ER\/research","DOI":"10.1177\/026010609801200306"},{"key":"127_CR13","doi-asserted-by":"crossref","unstructured":"Gong L (1991) Handling infeasible specifications of cryptographic protocols. In: Proceedings of Computer Security Foundations Workshop IV, Franconia, NH, pp 99\u2013102","DOI":"10.1109\/CSFW.1991.151575"},{"key":"127_CR14","doi-asserted-by":"crossref","unstructured":"Gong L, Needham R, Yahalom R (1990) Reasoning about belief in cryptographic protocols. In: Proceeding of the Symposium on Security and Privacy, Oakland, CA, pp 234\u2013248","DOI":"10.1109\/RISP.1990.63854"},{"key":"127_CR15","unstructured":"Gong L, Syverson P (1995) Fail-stop protocols: an approach to designing secure protocols. In: 5th International Working Conference on Dependable Computing for Critical Applications, pp 44\u201355"},{"key":"127_CR16","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/130704.130709","volume":"26","author":"Gong","year":"1992","unstructured":"Gong L (1992) A security risk of depending on synchronized clocks. ACM Oper Syst Rev 26(1):49\u201353","journal-title":"ACM Oper Syst Rev"},{"key":"127_CR17","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1016\/S0140-3664(99)00030-4","volume":"22","author":"Gritzalis","year":"1999","unstructured":"Gritzalis S (1999) Security protocols over open networks and distributed systems: formal methods for their analysis, design, and verification. Comput Commun 22(8):695\u2013707","journal-title":"Comput Commun"},{"key":"127_CR18","doi-asserted-by":"crossref","unstructured":"Huberman B, Franklin M, Hogg T (1999) Enhancing privacy and trust in electronic communities. Proc ACM e-Commerce 99:78\u201386","DOI":"10.1145\/336992.337012"},{"key":"127_CR19","unstructured":"ITU-T ITU-T X.509 (1998) The Directory \u2013 An Authentication Framework. ITU-T"},{"key":"127_CR20","doi-asserted-by":"crossref","unstructured":"Kailar R (1995) Reasoning about accountability in protocols for electronic commerce. In: Proceedings of the 1995 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, pp 236\u2013250","DOI":"10.1109\/SECPRI.1995.398936"},{"key":"127_CR21","doi-asserted-by":"crossref","unstructured":"Kessler V, Wedel G (1994) AUTLOG \u2013 an advanced logic of authentication. In: Proceedings of the 7th IEEE Computer Security Foundations Workshop, Los Alamitors. IEEE Computer Society Press, Los Alamitos, CA, pp 90\u201399","DOI":"10.1109\/CSFW.1994.315944"},{"key":"127_CR22","unstructured":"Kohl J, Neuman C (1990) The Kerberos Network Authentication Service. Version 5 RFC, Drft No\u20094, Network Working Group, MIT Project Athena"},{"key":"127_CR23","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"Meadows","year":"1996","unstructured":"Meadows C (1996) The NRL Protocol Analyzer: an overview. J Logic Program 26(2):113\u2013131","journal-title":"J Logic Program"},{"key":"127_CR24","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0055477","volume":"1465","author":"Meadows","year":"1998","unstructured":"Meadows C, Syverson P (1998) A formal specification of requirements for payment transactions in the SET protocol. In: Hirschfeld R (ed) Proceedings of Financial Cryptography 98. Lecture Notes in Computer Science 1465:122\u2013140. Springer-Verlag, Berlin","journal-title":"Lecture Notes in Computer Science"},{"key":"127_CR25","doi-asserted-by":"crossref","unstructured":"Millen JC (1995) The Interrogator Model. In: Proceeding of the 1995 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, pp 251\u2013260","DOI":"10.1109\/SECPRI.1995.398937"},{"key":"127_CR26","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"Needham","year":"1978","unstructured":"Needham R, Schroeder M (1978) Using encryption for authentication in large networks of computers. Commun ACM 21(12):993\u2013999","journal-title":"Commun ACM"},{"key":"127_CR27","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/35.312841","volume":"32","author":"Neuman","year":"1994","unstructured":"Neuman B, Ts\u2019o T (1994) Kerberos: an authentication service for computer networks. IEEE Commun 32(9):33\u201338","journal-title":"IEEE Commun"},{"key":"127_CR28","unstructured":"SET Secure Electronic Transaction Specification, Book 1: Business Description, Version 1.0,"},{"key":"127_CR29","unstructured":"SET Secure Electronic Transaction Specification, Book 2: Programmer\u2019s Guide, Version 1.0."},{"key":"127_CR30","unstructured":"SET Secure Electronic Transaction Specification, Book 3: Formal Protocol Definition, Version 1.0"},{"key":"127_CR31","doi-asserted-by":"crossref","unstructured":"Sherif MH (2000) Protocols for Secure Electronic Commerce. CRC Press, Boca Raton, FL","DOI":"10.1201\/b12387"},{"key":"127_CR32","doi-asserted-by":"crossref","unstructured":"Syverson P (1994) A taxonomy of replay attacks. In: Proceedings of the 7th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos, CA, pp 131\u2013136","DOI":"10.21236\/ADA463948"}],"container-title":["Knowledge and Information Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10115-003-0127-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10115-003-0127-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10115-003-0127-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10115-003-0127-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T12:10:05Z","timestamp":1624536605000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10115-003-0127-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["127"],"URL":"https:\/\/doi.org\/10.1007\/s10115-003-0127-4","relation":{},"ISSN":["0219-1377","0219-3116"],"issn-type":[{"value":"0219-1377","type":"print"},{"value":"0219-3116","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,1]]}}}