{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:25:37Z","timestamp":1759638337615},"reference-count":33,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,6,1]],"date-time":"2002-06-01T00:00:00Z","timestamp":1022889600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4064,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2002,6]]},"DOI":"10.1016\/s0304-3975(01)00136-0","type":"journal-article","created":{"date-parts":[[2002,10,11]],"date-time":"2002-10-11T11:37:18Z","timestamp":1034336238000},"page":"271-304","source":"Crossref","is-referenced-by-count":12,"title":["Primitives for authentication in process algebras"],"prefix":"10.1016","volume":"283","author":[{"given":"Chiara","family":"Bodei","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierpaolo","family":"Degano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riccardo","family":"Focardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corrado","family":"Priami","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(01)00136-0_BIB1","unstructured":"M. Abadi, Secrecy by typing in security protocols, J. ACM 5(46) (1999) 18\u201336. An abstract appeared in Proc. TACS 1997, Springer, Berlin, 1997."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB2","doi-asserted-by":"crossref","unstructured":"M. Abadi, C. Fournet, G. Gonthier, Secure implementation of channel abstractions, Proc. 13th Annu. IEEE Symp. Logic in Computer Science, 1998, pp. 105\u2013116.","DOI":"10.1109\/LICS.1998.705647"},{"issue":"1","key":"10.1016\/S0304-3975(01)00136-0_BIB3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1998.2740","article-title":"A calculus for cryptographic protocols: the spi calculus","volume":"148","author":"Abadi","year":"1999","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB4","doi-asserted-by":"crossref","unstructured":"G. Berry, L. Cosserat, The synchronous programming language ESTEREL and its mathematical semantics, in: Proc. of the Seminar on Concurrency, Lecture Notes in Computer Science, Vol. 197, Springer, Berlin, 1984.","DOI":"10.1007\/3-540-15670-4_19"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB5","unstructured":"C. Bodei, Security issues in process calculi, Ph.D. Thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, TD-2\/00, March, 2000."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB6","doi-asserted-by":"crossref","unstructured":"C. Bodei, P. Degano, R. Focardi, C. Priami, Authentication via localized names, Proc. of the 12th Computer Security Foundation Workshop, IEEE Press, 1999, pp. 98\u2013110.","DOI":"10.1109\/CSFW.1999.779766"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB7","doi-asserted-by":"crossref","unstructured":"C. Bodei, P. Degano, C. Priami, Names of the \u03c0-calculus agents handled locally, Theoret. Comput. Sci. 253(2) (2001) 155\u2013184. Extended abstract in: Proc. ICALP\u201996, Lecture Notes in Computer Science, Vol. 1099, Springer, Berlin.","DOI":"10.1016\/S0304-3975(00)00093-1"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB8","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 Trans. Comput. Systems"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB9","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/S0304-3975(99)80003-6","article-title":"Non interleaving semantics for mobile processes","volume":"216","author":"Degano","year":"1999","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB10","doi-asserted-by":"crossref","unstructured":"P. Degano, C. Priami, Enhanced operational semantics: a tool for describing and analysing concurrent systems, ACM Comput. Surveys, to appear.","DOI":"10.1145\/384192.384194"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB11","doi-asserted-by":"crossref","unstructured":"P. Degano, C. Priami, L. Leth, B. Thomsen, Causality for debugging mobile agents, Acta Inform. 36 (1999) 335\u2013375.","DOI":"10.1007\/s002360050164"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB12","unstructured":"A. Durante, R. Focardi, R. Gorrieri, A Compiler for Analysing Cryptographic Protocols Using Non-Interference, ACM TOSEM, to appear."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB13","doi-asserted-by":"crossref","unstructured":"F.J.T. Fabrega, J.C. Herzog, J.D. Guttman, Strand spaces: why is a security protocol correct? Proc. 1998 Symp. on Security and Privacy, IEEE Computer Society Press, May 1998.","DOI":"10.21236\/ADA459060"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB14","unstructured":"R. Focardi, Using entity locations for the analysis of authentication protocols, Proc. Sixth Italian Conf. on Theoretical Computer Science, November 1998."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB15","series-title":"Proc. DIMACS Workshop on Design and Formal Verification of Security Protocols","article-title":"Using non interference for the analysis of security protocols","author":"Focardi","year":"1997"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB16","doi-asserted-by":"crossref","unstructured":"R. Focardi, R. Gorrieri, F. Martinelli, Non interference for the analysis of cryptographic protocols, Proc. ICALP\u201900, Geneva, Switzerland, July 2000.","DOI":"10.1007\/3-540-45022-X_31"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB17","unstructured":"R. Focardi, F. Martinelli, A uniform approach for the definition of security properties, in: Proceedings of World Congress on Formal Methods in the Development of Computing Systems, Lecture Notes in Computer Science, Vol. 1708, Toulouse, France, Springer, Berlin, September 1999, pp. 794\u2013813."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB18","unstructured":"C. Fournet, Gonthier, The reflexive chemical abstract machine and the join calculus, Proc. 23rd ACM Symp. on Principles of Programming Languages, 1996."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB19","unstructured":"International Organization for Standardization, Information Technology\u2014Security Techniques\u2014Entity Authentication Mechanism; Part 1: General Model, ISO\/IEC 9798-1, 2nd Edition, September 1991."},{"issue":"2","key":"10.1016\/S0304-3975(01)00136-0_BIB20","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00197942","article-title":"Three systems for cryptographic protocol analysis","volume":"7","author":"Kemmerer","year":"1994","journal-title":"J. Cryptol."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB21","doi-asserted-by":"crossref","unstructured":"G. Lowe, Breaking and fixing the Needham\u2013Schroeder public-key protocol using FDR, in: Proc. Second Internat. Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996), Passau, Germany, Lecture Notes in Computer Science, Vol. 1055, Springer, Berlin, March 1996, pp. 146\u2013166.","DOI":"10.1007\/3-540-61042-1_43"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB22","doi-asserted-by":"crossref","unstructured":"G. Lowe, A hierarchy of authentication specification, Proc. 10th Computer Security Foundation Workshop, IEEE Press, 1997.","DOI":"10.1109\/CSFW.1997.596782"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB23","doi-asserted-by":"crossref","first-page":"221","DOI":"10.3233\/FI-1999-402306","article-title":"Applying techniques of asynchronous concurrency to synchronous languages","volume":"40","author":"Maggiolo-Schettini","year":"1999","journal-title":"Fund. Informat."},{"issue":"1","key":"10.1016\/S0304-3975(01)00136-0_BIB24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes (I and II)","volume":"100","author":"Milner","year":"1992","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB25","doi-asserted-by":"crossref","unstructured":"J.C. Mitchell, M. Mitchell, U. Stern, Automated analysis of cryptographic protocols using Mur\u03c6, Proc. 1997 IEEE Symp. on Research in Security and Privacy, IEEE Computer Society Press, 1997, pp. 141\u2013153.","DOI":"10.1109\/SECPRI.1997.601329"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB26","unstructured":"National Bureau of Standards, Data Encryption Standard (DES), FIPS Publication 46, 1977."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB27","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/0304-3975(95)00017-8","article-title":"From CML to its process algebra","volume":"155","author":"Nielson","year":"1996","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB28","series-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner","article-title":"PICT: a programming language based on the pi-calculus","author":"Pierce","year":"2000"},{"issue":"9","key":"10.1016\/S0304-3975(01)00136-0_BIB29","doi-asserted-by":"crossref","first-page":"741","DOI":"10.1109\/32.713329","article-title":"Verifying authentication protocols in CSP","volume":"24","author":"Schneider","year":"1998","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB30","series-title":"Applied Cryptography","author":"Schneier","year":"1996"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB31","doi-asserted-by":"crossref","unstructured":"R. Thayer, N. Doraswamy, R. Glenn, RFC 2411: IP security document roadmap, November 1998.","DOI":"10.17487\/rfc2411"},{"key":"10.1016\/S0304-3975(01)00136-0_BIB32","unstructured":"B. Thomsen, L. Leth, S. Prasad, T.-M. Kuo, A. Kramer, F. Knabe, A. Giacalone, Facile Antigua Release Programming Guide, Tech. Report ECRC-93-20, European Computer-Industry Research Centre, 1993."},{"key":"10.1016\/S0304-3975(01)00136-0_BIB33","doi-asserted-by":"crossref","unstructured":"J. Vitek, G. Castagna, Seal: a framework for secure mobile computations, in: Internet Programming Languages, LNCS 1686, Springer, 1999.","DOI":"10.1007\/3-540-47959-7_3"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501001360?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501001360?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,5]],"date-time":"2020-03-05T14:13:06Z","timestamp":1583417586000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397501001360"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,6]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,6]]}},"alternative-id":["S0304397501001360"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(01)00136-0","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2002,6]]}}}