{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T08:29:11Z","timestamp":1791188951242,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631415","type":"print"},{"value":"9783540691884","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63141-0_5","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:09:05Z","timestamp":1330279745000},"page":"59-73","source":"Crossref","is-referenced-by-count":30,"title":["Reasoning about cryptographic protocols in the spi calculus"],"prefix":"10.1007","author":[{"given":"Mart\u00edn","family":"Abadi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. To appear in the Proceedings of the Fourth ACM Conference on Computer and Communications Security, 1997.","DOI":"10.1145\/266420.266432"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Technical Report 414, University of Cambridge Computer Laboratory, January 1997.","DOI":"10.1145\/266420.266432"},{"issue":"1","key":"5_CR3","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M. Abadi","year":"1996","unstructured":"M. Abadi and R. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6\u201315, January 1996.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR4","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1098\/rspa.1989.0125","volume":"426","author":"M. Burrows","year":"1989","unstructured":"M. Burrows, M. Abadi, and R. M. Needham. A logic of authentication. Proceedings of the Royal Society of London A, 426:233\u2013271, 1989. A preliminary version appeared as Digital Equipment Corporation Systems Research Center report No. 39, February 1989.","journal-title":"Proceedings of the Royal Society of London A"},{"issue":"1","key":"5_CR5","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90185-I","volume":"96","author":"G. Berry","year":"1992","unstructured":"G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96(1):217\u2013248, April 1992.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"5_CR6","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1006\/inco.1995.1114","volume":"120","author":"M. Boreale","year":"1995","unstructured":"M. Boreale and R. De Nicola. Testing equivalence for mobile processes. Information and Computation, 120(2):279\u2013303, August 1995.","journal-title":"Information and Computation"},{"key":"5_CR7","unstructured":"Data encryption standard. Fed. Inform. Processing Standards Pub. 46, National Bureau of Standards, Washington DC, January 1977."},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R. Nicola De","year":"1984","unstructured":"R. De Nicola and M. C. B. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83\u2013133, 1984.","journal-title":"Theoretical Computer Science"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"J. Gray and J. McLean. Using temporal logic to specify and verify cryptographic protocols (progress report). In Proceedings of the 8th IEEE Computer Security Foundations Workshop, pages 108\u2013116, 1995.","DOI":"10.1109\/CSFW.1995.518557"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"R. A. Kemmerer. Analyzing encryption protocols using formal verification techniques. IEEE Journal on Selected Areas in Communications, 7, 1989.","DOI":"10.1109\/49.17707"},{"issue":"4","key":"5_CR11","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1145\/163640.163643","volume":"27","author":"A. Liebl","year":"1993","unstructured":"A. Liebl. Authentication in distributed systems: A bibliography. ACM Operating Systems Review, 27(4):31\u201341, 1993.","journal-title":"ACM Operating Systems Review"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science, pages 147\u2013166. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61042-1_43"},{"issue":"2","key":"5_CR13","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1109\/TSE.1987.233151","volume":"SE-13","author":"J. K. Millen","year":"1987","unstructured":"J. K. Millen, S. C. Clark, and S. B. Freedman. The Interrogator: Protocol security analysis. IEEE Transactions on Software Engineering, SE-13(2):274\u2013288, February 1987.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"5_CR14","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1992-1102","volume":"1","author":"C. Meadows","year":"1992","unstructured":"C. Meadows. Applying formal methods to the analysis of a key management protocol. Journal of Computer Security, 1(1):5\u201336, 1992.","journal-title":"Journal of Computer Security"},{"key":"5_CR15","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall International, 1989."},{"key":"5_CR16","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1017\/S0960129500001407","volume":"2","author":"R. Milner","year":"1992","unstructured":"R. Milner. Functions as processes. Mathematical Structures in Computer Science, 2:119\u2013141, 1992.","journal-title":"Mathematical Structures in Computer Science"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"J. K. Millen. The Interrogator model. In IEEE Symposium on Security and Privacy, pages 251\u2013260, 1995.","DOI":"10.1109\/SECPRI.1995.398937"},{"key":"5_CR18","unstructured":"R. Milner. The \u03c0-calculus. Undergraduate lecture notes, Cambridge University, 1995."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts I and II. Information and Computation, pages 1\u201340 and 41\u201377, September 1992.","DOI":"10.1016\/0890-5401(92)90009-5"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"S. Schneider. Security properties and CSP. In IEEE Symposium on Security and Privacy, pages 174\u2013187, 1996.","DOI":"10.1109\/SECPRI.1996.502680"},{"key":"5_CR21","unstructured":"B. Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C. John Wiley & Sons, Inc., second edition, 1996."}],"container-title":["Lecture Notes in Computer Science","CONCUR '97: Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63141-0_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:16:12Z","timestamp":1605629772000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63141-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631415","9783540691884"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-63141-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}