{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T15:32:21Z","timestamp":1759937541137},"reference-count":21,"publisher":"Elsevier BV","issue":"5","license":[{"start":{"date-parts":[[2003,12,1]],"date-time":"2003-12-01T00:00:00Z","timestamp":1070236800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computer Networks"],"published-print":{"date-parts":[[2003,12]]},"DOI":"10.1016\/s1389-1286(03)00292-5","type":"journal-article","created":{"date-parts":[[2003,5,27]],"date-time":"2003-05-27T22:47:42Z","timestamp":1054075662000},"page":"601-618","source":"Crossref","is-referenced-by-count":15,"title":["Formal verification: an imperative step in the design of security protocols"],"prefix":"10.1016","volume":"43","author":[{"given":"Tom","family":"Coffey","sequence":"first","affiliation":[]},{"given":"Reiner","family":"Dojen","sequence":"additional","affiliation":[]},{"given":"Tomas","family":"Flanagan","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"12","key":"10.1016\/S1389-1286(03)00292-5_BIB1","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1145\/359657.359659","article-title":"Using encryption for authentication in large networks of computers","volume":"21","author":"Needham","year":"1978","journal-title":"Communications of the ACM"},{"issue":"5","key":"10.1016\/S1389-1286(03)00292-5_BIB2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/74851.74852","article-title":"A logic of authentication","volume":"23","author":"Burrows","year":"1989","journal-title":"ACM Operating System Review"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB3","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","article-title":"The NRL protocol analyzer: an overview","volume":"26","author":"Meadows","year":"1996","journal-title":"Journal of Logic Programming"},{"issue":"2","key":"10.1016\/S1389-1286(03)00292-5_BIB4","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1109\/TSE.1987.233151","article-title":"The interrogator: protocol security analysis","volume":"SE-13","author":"Millen","year":"1997","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB5","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","article-title":"The inductive approach to verifying cryptographic protocols","volume":"6","author":"Paulson","year":"2000","journal-title":"Journal of Computer Security"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB6","doi-asserted-by":"crossref","unstructured":"L. Gong, R. Needham, R. Yahalom, Reasoning about belief in cryptographic protocols, in: Proceedings of 1990 IEEE Computer Society Synopsis on Research in Security and Privacy, 1990, pp. 234\u2013248","DOI":"10.1109\/RISP.1990.63854"},{"issue":"1","key":"10.1016\/S1389-1286(03)00292-5_BIB7","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1049\/ip-cdt:19970838","article-title":"A logic for verifying public key cryptographic protocols","volume":"144","author":"Coffey","year":"1997","journal-title":"IEE Journal of Proceedings\u2013\u2013Computers and Digital Techniques"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB8","unstructured":"Y. Zhang, V. Varadharajan, A logic for modelling the dynamics of beliefs in cryptographic protocols, in: Proceedings of Australasian Computer Science Conference, 2001"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB9","unstructured":"Security Architecture, 3G TSPP 33.102 version 3.7.0"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB10","doi-asserted-by":"crossref","unstructured":"D.S. Wong, A.H. Chan, Efficient and mutually authenticated key exchange for low power computing devices, in: Proceedings of ASIACRYPT 2001","DOI":"10.1007\/3-540-45682-1_17"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB11","doi-asserted-by":"crossref","first-page":"183","DOI":"10.3233\/JCS-2000-82-306","article-title":"Authentication and payment in future mobile systems","volume":"8","author":"Horn","year":"2000","journal-title":"Journal of Computer Security"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB12","unstructured":"C. Boyd, D.-G. Park, Public key protocols for wireless communications, in: Proceedings of 1998 International Conference on Information Security and Cryptology (ICISC \u201998), Seoul, 1998"},{"issue":"6","key":"10.1016\/S1389-1286(03)00292-5_BIB13","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1109\/49.232291","article-title":"Privacy and authentication on a portable communications system","volume":"11","author":"Beller","year":"1993","journal-title":"IEEE Journal on Selected Areas in Communications"},{"issue":"3","key":"10.1016\/S1389-1286(03)00292-5_BIB14","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1145\/182110.182112","article-title":"Optimal privacy and authentication on a portable communications system","volume":"28","author":"Carlsen","year":"1994","journal-title":"ACM Operating Systems Review"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB15","series-title":"Information Security and Privacy","first-page":"134","article-title":"On the design of security protocols for mobile communications","volume":"vol. 1172","author":"Mu","year":"1996"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB16","doi-asserted-by":"crossref","unstructured":"V.D. Gligor, R. Kailar, S. Stubblebine, L. Gong, Logics for cryptographic protocols\u2013\u2013virtues and limitations, in: Proceedings of 4th Computer Security Foundation Workshop, 1991, pp. 219\u2013226","DOI":"10.1109\/CSFW.1991.151591"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB17","doi-asserted-by":"crossref","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","article-title":"New directions in cryptography","volume":"22","author":"Diffie","year":"1976","journal-title":"IEEE Transactions on Information Theory"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB18","unstructured":"M.O. Rabin, Digitalized signatures and public-key functions as intractable as factorisation, Technical Report MIT\/LCS\/TR-212, MIT, 1979"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB19","doi-asserted-by":"crossref","unstructured":"L. Gong, Handling infeasible specifications of cryptographic protocols, in: Proceedings of 4th Computer Security Foundation Workshop, 1991, pp. 99\u2013102","DOI":"10.1109\/CSFW.1991.151575"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB20","unstructured":"A. Mathuria, R. Safavi-Naini, P. Nickolas, Some remarks on the logic of Gong, Needham and Yahalom, in: Proceedings of the International Computer Symposium, Hsinchu, Taiwan, ROC, vol. 1, 1994, pp. 303\u2013308"},{"key":"10.1016\/S1389-1286(03)00292-5_BIB21","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1109\/25.994813","article-title":"Authentication protocols for mobile network environment value-added services","volume":"51","author":"Horn","year":"2002","journal-title":"IEEE Transactions on Vehicular Technology"}],"container-title":["Computer Networks"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1389128603002925?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1389128603002925?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T07:51:46Z","timestamp":1553154706000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1389128603002925"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,12]]},"references-count":21,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2003,12]]}},"alternative-id":["S1389128603002925"],"URL":"https:\/\/doi.org\/10.1016\/s1389-1286(03)00292-5","relation":{},"ISSN":["1389-1286"],"issn-type":[{"value":"1389-1286","type":"print"}],"subject":[],"published":{"date-parts":[[2003,12]]}}}