{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:05:58Z","timestamp":1761620758690},"reference-count":108,"publisher":"Elsevier BV","issue":"8","license":[{"start":{"date-parts":[[1999,5,1]],"date-time":"1999-05-01T00:00:00Z","timestamp":925516800000},"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 Communications"],"published-print":{"date-parts":[[1999,5]]},"DOI":"10.1016\/s0140-3664(99)00030-4","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T19:03:07Z","timestamp":1027623787000},"page":"697-709","source":"Crossref","is-referenced-by-count":38,"title":["Security protocols over open networks and distributed systems: formal methods for their analysis, design, and verification"],"prefix":"10.1016","volume":"22","author":[{"given":"S","family":"Gritzalis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D","family":"Spinellis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P","family":"Georgiadis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"8","key":"10.1016\/S0140-3664(99)00030-4_BIB1","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1145\/358722.358740","article-title":"Timestamps in key distribution protocols","volume":"24","author":"Denning","year":"1981","journal-title":"Communications of the ACM"},{"issue":"12","key":"10.1016\/S0140-3664(99)00030-4_BIB2","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":"1","key":"10.1016\/S0140-3664(99)00030-4_BIB3","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/24592.24593","article-title":"Authentication revisited","volume":"21","author":"Needham","year":"1987","journal-title":"Operating Systems Review"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB4","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/S0140-3664(97)00011-X","article-title":"A timestamp model for determining real-time communications in intelligent networks","volume":"20","author":"Patel","year":"1997","journal-title":"Computer Communications"},{"issue":"1","key":"10.1016\/S0140-3664(99)00030-4_BIB5","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/77648.77649","article-title":"A logic of authentication","volume":"8","author":"Burrows","year":"1990","journal-title":"ACM Transactions on Computer Systems"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB6","series-title":"Reasoning about belief in cryptographic protocols","author":"Gong","year":"1990"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB7","series-title":"On unifying some cryptographic protocol logics","author":"Syverson","year":"1994"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB8","series-title":"A HOL extension of GNY for automatically analyzing cryptographic protocols","author":"Brackin","year":"1996"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB9","series-title":"AUTLOG\u2014an advanced logic of authentication","author":"Kessler","year":"1994"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB10","series-title":"The use of logic in the analysis of cryptographic protocols","author":"Syverson","year":"1991"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB11","series-title":"A logical language for specifying cryptographic protocol requirements","author":"Syverson","year":"1993"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB12","unstructured":"S. Gritzalis, The BAN logic for the analysis of authentication protocols in distributed systems: a review, in: Proceedings of the 1st meeting of the IKAROS Greek Computer Society\u2019s human network for the Security, Quality, and Reliability in Information and Communication Technologies, 1996 (in Greek)."},{"issue":"2","key":"10.1016\/S0140-3664(99)00030-4_BIB13","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the security of public key protocols","volume":"29","author":"Dolev","year":"1983","journal-title":"IEEE Transactions on Information Theory"},{"issue":"4","key":"10.1016\/S0140-3664(99)00030-4_BIB14","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1109\/49.17707","article-title":"Analyzing encryption protocols using formal verification techniques","volume":"7","author":"Kemmerer","year":"1989","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB15","series-title":"Breaking and fixing the Needham-Schroeder public-key protocol using FDR","author":"Lowe","year":"1996"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB16","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1992-1102","article-title":"Applying formal methods to the analysis of a key-management protocol","volume":"1","author":"Meadows","year":"1992","journal-title":"Journal of Computer Security"},{"issue":"2","key":"10.1016\/S0140-3664(99)00030-4_BIB17","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"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB18","series-title":"The interrogator model","author":"Millen","year":"1995"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB19","series-title":"Automated analysis of cryptographic protocols using Mur\u03c6","author":"Mitchell","year":"1997"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB20","series-title":"Modelling and verifying key-exchange protocols using CSP and FDR","author":"Roscoe","year":"1995"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB21","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0169-7552(86)90004-8","article-title":"Authentication protocols for computer networks","volume":"11","author":"Sidhu","year":"1986","journal-title":"Computer Networks and ISDN Systems"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB22","doi-asserted-by":"crossref","first-page":"693","DOI":"10.1016\/0167-4048(89)90008-4","article-title":"Verification of network security protocols","volume":"8","author":"Varadharajan","year":"1989","journal-title":"Computers and Security"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB23","unstructured":"E. Snekkenes, Formal Specification and Analysis of Cryptographic Protocols, PhD thesis, University of Oslo, Norway, 1995."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB24","series-title":"Proving properties of security protocols by induction","author":"Paulson","year":"1997"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB25","series-title":"An approach to the formal verification of cryptographic protocols","author":"Bolignano","year":"1996"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB26","series-title":"Mechanized proofs for a recursive authentication protocol","author":"Paulson","year":"1997"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB27","unstructured":"S. Brackin, A State-Based HOL Theory of Protocol Failure, ATR 98007, Arca Systems, Inc., 1997, http:\/\/www.arca.com\/paper.htm."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB28","unstructured":"J. Scheid, S. Holtsberg, Ina Jo Specification Language Reference Manual, System Development Group, Unisys Corporation, CA, 1988."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB29","unstructured":"A.W. Roscoe, Developing and verifying protocols in CSP, Proceedings of Mierlo workshop on protocols, TU Eidhoven, 1993."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB30","unstructured":"A. Roscoe, M. Goldsmith, The perfect spy for model-checking cryptoprotocols, in: Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997, http:\/\/dimacs.rutgers.edu\/Workshops\/Security\/."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB31","series-title":"Casper: a compiler for the analysis of security protocols","author":"Lowe","year":"1997"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB32","series-title":"Protocol verification as a hardware design aid","author":"Dill","year":"1992"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB33","series-title":"Key distribution protocol for digital mobile communication systems","author":"Tatebayashi","year":"1990"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB34","series-title":"Distributed Open Systems","article-title":"The evolution of the Kerberos authentication service ver. 5","author":"Kohl","year":"1994"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB35","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","article-title":"Introduction to the ISO specification language LOTOS","volume":"14","author":"Bolognesi","year":"1987","journal-title":"Computer Networks and ISDN Systems"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB36","unstructured":"ISO\/IEC Information Processing Systems\u2014Open Systems Interconnection: LOTOS, a Formal Description Technique based on the Temporal Ordering of Observational Behaviour, IS8807, 1989."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB37","unstructured":"F. Germeau, G. Leduc, Model-based Design and Verification of security protocols using LOTOS, in: Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997, http:\/\/dimacs.rutgers.edu\/Workshops\/Security\/."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB38","unstructured":"J. Guimaraes, J. Boucqueau, B. Macq, OKAPI: a Kernel for Access Control to Multimedia services based on TTPs, in: Proceedings of the 1996 ECMAST European Conference on Multime-dia Applications, Services and Techniques, 1996, pp. 783\u2013798."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB39","unstructured":"G. Leduc, O. Bonaventure, E. Koerner, L. Leonard, C. Pecheur, D. Zanetti, Specification and Verification of a TTP protocol for the conditional access to services, in: Proceedings of the 12th J. Cartier Workshop on Formal Methods and their applications: Telecommunications, VLSI and Real-Time Computerised Control Systems, 1996."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB40","series-title":"Formal Description Techniques and Protocol Specifications, Testing and Verification, FORTE\/PSTV\u201997","first-page":"145","article-title":"A computer-aided design pf a secure registration protocol","year":"1997"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB41","doi-asserted-by":"crossref","unstructured":"C. Ghezzi, R. Kemmerer, ASTRAL: an assertion language for specifying real-time systems, in: Proceedings of the Third European Software Engineering Conference, 1991, pp. 122\u2013146.","DOI":"10.1007\/3540547428_46"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB42","unstructured":"Z. Dang, Using the ASTRAL Model Checker for Cryptographic Protocol Analysis, in: Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997, http:\/\/dimacs.rutgers.edu\/Workshops\/Security\/."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB43","series-title":"Towards a completeness result for model checking of security protocols","author":"Lowe","year":"1998"},{"issue":"2","key":"10.1016\/S0140-3664(99)00030-4_BIB44","doi-asserted-by":"crossref","DOI":"10.1109\/TSE.1987.233151","article-title":"The interrogator: protocol security analysis","volume":"13","author":"Millen","year":"1987","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB45","series-title":"How to selectively broadcast a secret","author":"Simmons","year":"1985"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB46","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0167-4048(90)90159-Q","article-title":"A security scheme for resource sharing over a network","volume":"19","author":"Burns","year":"1990","journal-title":"Computers and Security"},{"issue":"2","key":"10.1016\/S0140-3664(99)00030-4_BIB47","first-page":"79","volume":"7","author":"Kemmerer","year":"1994","journal-title":"Three Systems for Cryptographic Protocol Analysis"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB48","series-title":"Language generation and verification in the NRL protocol analyzer","author":"Meadows","year":"1996"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB49","unstructured":"CCITT CCITT X.509, The Directory\u2014An Authentication Framework, 1988."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB50","unstructured":"J. Millen, C. Neuman, J. Schiller, J. Saltzer, Kerberos Authentication and Authorization system, Project Athena Technical Plan, Section E.2.1, M.I.T., MA, 1987."},{"issue":"1","key":"10.1016\/S0140-3664(99)00030-4_BIB51","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/24592.24594","article-title":"Efficient and timely mutual authentication","volume":"21","author":"Otway","year":"1987","journal-title":"ACM Operating Systems Review"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB52","unstructured":"G. Pal, Verification of the iKP family of secure electronic payment protocols, 1996, http:\/\/web.mit.edu\/gnpal\/www\/ikp\/verify_ikp.html."},{"issue":"2","key":"10.1016\/S0140-3664(99)00030-4_BIB53","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/232302.232305","article-title":"An authentication and key distribution system for open network systems","volume":"30","author":"Shieh","year":"1996","journal-title":"ACM Operating Systems Review"},{"issue":"4","key":"10.1016\/S0140-3664(99)00030-4_BIB54","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1145\/163640.163643","article-title":"Authentication in distributed systems: a bibliography","volume":"27","author":"Liebl","year":"1993","journal-title":"ACM Operating Systems Review"},{"issue":"2","key":"10.1016\/S0140-3664(99)00030-4_BIB55","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/382258.382789","article-title":"A critique of the BAN logic","volume":"24","author":"Nessett","year":"1990","journal-title":"ACM Operating Systems Review"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB56","series-title":"Exploring the BAN approach to protocol analysis","author":"Snekkenes","year":"1991"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB57","series-title":"Towards formal analysis of security protocols","author":"Mao","year":"1993"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB58","series-title":"An augmentation of BAN-like logics","author":"Mao","year":"1995"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB59","unstructured":"P. Syverson, Relating two models of computation for security protocols, in: Proceedings of the 1998 LICS Workshop on Formal Methods and Security Protocols, 1998, http:\/\/www.cs.bell-labs.com\/who\/nch\/fmsp\/program.html."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB60","series-title":"Extending cryptographic logics of belief to key agreement protocols","author":"van Oorschot","year":"1993"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB61","series-title":"A second generation wallet, ESORICS\u201992","author":"Anderson","year":"1992"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB62","series-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon","year":"1993"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB63","series-title":"A semantics for a logic of authentication","author":"Abadi","year":"1991"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB64","series-title":"Reasoning about accountability in protocols for electronic commerce","author":"Kailar","year":"1995"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB65","series-title":"A sound logic for analysing electronic commerce protocols, ESORICS\u201998","author":"Kessler","year":"1998"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB66","series-title":"Formal semantics for authentication logics, ESORICS\u201996","author":"Wedel","year":"1996"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB67","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Gimenec, H. Herbelin, G. Huet, P. Manoury, C. Munoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saibi, B. Werner, The Coq Proof Assistant Reference Manual, version 6.1., Project Coq, INRIA-Rocqunecourt and CNRS-Ens Lyon, 1996."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB68","series-title":"Isabelle: A Generic Theorem Prover","author":"Paulson","year":"1994"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB69","series-title":"Verifying authentication protocols with CSP","author":"Schneider","year":"1997"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB70","series-title":"Formal analysis of a non-repudiation protocol","author":"Schneider","year":"1998"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB71","series-title":"A fair non-repudiation protocol","author":"Zhou","year":"1996"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB72","series-title":"Strand spaces: why is a security protocol correct","author":"Fabrega","year":"1998"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB73","series-title":"Honest ideals on strand spaces","author":"Fabrega","year":"1998"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB74","unstructured":"F. Fabrega, J. Herzog, J. Guttman, Strand space pictures, in: Proceedings of the 1998 Workshop on Formal Methods and Security Protocols, 1998, http:\/\/www.cs.bell-labs.com\/who\/nch\/fmsp\/program.html."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB75","series-title":"An interface specification language for automatically analyzing cryptographic protocols","author":"Brackin","year":"1997"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB76","doi-asserted-by":"crossref","unstructured":"S. Brackin, Automatic Formal Analyses of Cryptographic Protocols, Arca Systems, Inc., 1997, http:\/\/www.arca.com\/paper.htm.","DOI":"10.1109\/NDSS.1997.579219"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB77","series-title":"Automatic formal analyses of cryptographic protocols","author":"Brackin","year":"1996"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB78","series-title":"Verifying the correctness of cryptographic protocols using convince","author":"Lichota","year":"1996"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB79","series-title":"Evaluating and improving protocol analysis by automatic proof","author":"Brackin","year":"1998"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB80","doi-asserted-by":"crossref","unstructured":"J. Millen, CAPSL\u2014Common Authentication Protocol Specification Language, 1997, http:\/\/www.mitre.org\/research\/capsl.","DOI":"10.1145\/304851.304879"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB81","unstructured":"G. Lowe, Casper: A Compiler for the Analysis of Security Protocols, 1996, http:\/\/www.mcs.le.ac.uk\/7sim;glowe\/Security\/Casper\/index.html."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB82","series-title":"A calculus for cryptographic protocols: the Spi calculus","author":"Abadi","year":"1997"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB83","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes","volume":"00","author":"Milner","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB84","unstructured":"S. Brackin, A HOL formalisation of CAPSL semantics, in: Proceedings of the 21st National Information Systems Security Conference, 1998."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB85","series-title":"Computer Science Today: Recent Trends and Developments, LNCS 1000","article-title":"Programming satan\u2019s computer","year":"1995"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB86","series-title":"Prudent engineering practice for cryptographic protocols","author":"Abadi","year":"1994"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB87","series-title":"Limitations on design principles for public key protocols","author":"Syverson","year":"1996"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB88","unstructured":"C. Boyd, Towards extensional goals in authentication protocols, in: Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997, http:\/\/dimacs.rutgers.edu\/Workshops\/Security."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB89","unstructured":"Panel: Y. Desmedt (Chair), M. Burmester, J. Millen, Design vs. Verification: Is Verification the Wrong Approach?, in: Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997, http:\/\/dimacs.rutgers.edu\/Workshops\/Security\/."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB90","series-title":"Formal verification of cryptographic protocols: a survey, advances in cryptology","author":"Meadows","year":"1995"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB91","series-title":"A model for secure protocols and their compositions","author":"Heintze","year":"1994"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB92","unstructured":"L. Gong, P. Syverson, Fail-stop protocols: an approach to designing secure protocols, in: pre-Proceedings of DCCA-5 Fifth International Working Conference on Dependable Computing for Critical Applications, 1995, pp. 45\u201355."},{"issue":"2","key":"10.1016\/S0140-3664(99)00030-4_BIB93","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1145\/357369.357371","article-title":"Fail-stop processors: an approach to designing fault-tolerant computing systems","volume":"2","author":"Schlichting","year":"1983","journal-title":"ACM Transactions on Computing Systems"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB94","series-title":"Generating formal cryptographic protocol specifications","author":"Carlsen","year":"1994"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB95","series-title":"A formal model for systematic design of key establishment protocols, ACISP\u201998","author":"Rudolph","year":"1998"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB96","series-title":"A simple logic for authentication protocol design","author":"Buttyan","year":"1998"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB97","series-title":"Designing secure key exchange protocols, ESORICS\u201994","author":"Boyd","year":"1994"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB98","series-title":"What do we mean by entity authentication?","author":"Gollmann","year":"1996"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB99","series-title":"Social processes and proofs of theorems and programs","author":"DeMillos","year":"1977"},{"issue":"5","key":"10.1016\/S0140-3664(99)00030-4_BIB100","doi-asserted-by":"crossref","first-page":"648","DOI":"10.1109\/49.223865","article-title":"Protecting poorly chosen secrets from guessing attacks","volume":"11","author":"Gong","year":"1993","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB101","unstructured":"S. Brackin, Automatic formal analyses of two large commercial protocols, in: Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997, http:\/\/dimacs.rutgers.edu\/Workshops\/Security\/."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB102","unstructured":"J. Mitchell, V. Shmatikov, U. Stern, Finite-state analysis of SSL 3.0 and related protocols, in: Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997, http:\/\/dimacs.rutgers.edu\/Workshops\/Security\/."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB103","doi-asserted-by":"crossref","unstructured":"L. Paulson, Inductive Analysis of the Internet Protocol TLS, TR440, University of Cambridge, Computer Laboratory, 1998.","DOI":"10.1007\/3-540-49135-X_2"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB104","unstructured":"C. Bella, L. Paulson, Using Isabelle to prove properties of the Kerberos authentication system, in: Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997, http:\/\/dimacs.rutgers.edu\/Workshops\/Security\/."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB105","series-title":"Kerberos version IV: inductive analysis of the secrecy goals, ESORICS\u201998","author":"Bella","year":"1998"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB106","series-title":"Towards the formal verification of electronic commerce protocols","author":"Bolignano","year":"1997"},{"key":"10.1016\/S0140-3664(99)00030-4_BIB107","unstructured":"C. Meadows, Using the NRL protocol analyzer to examine protocol suites, in: Proceedings of the 1998 LICS Workshop on Formal Methods and Security Protocols, 1998, http:\/\/www.cs.bell-labs.com\/who\/nch\/fmsp\/program.html."},{"key":"10.1016\/S0140-3664(99)00030-4_BIB108","doi-asserted-by":"crossref","unstructured":"D. Harkins, D. Carrel, The Internet Key Exchange (IKE) version 6, 1998, \u3008draft-ietf-ipsec-isakmp-oakley-06.txt\u3009.","DOI":"10.17487\/rfc2409"}],"container-title":["Computer Communications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0140366499000304?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0140366499000304?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,15]],"date-time":"2020-01-15T00:56:15Z","timestamp":1579049775000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0140366499000304"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,5]]},"references-count":108,"journal-issue":{"issue":"8","published-print":{"date-parts":[[1999,5]]}},"alternative-id":["S0140366499000304"],"URL":"https:\/\/doi.org\/10.1016\/s0140-3664(99)00030-4","relation":{},"ISSN":["0140-3664"],"issn-type":[{"value":"0140-3664","type":"print"}],"subject":[],"published":{"date-parts":[[1999,5]]}}}