{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T12:40:20Z","timestamp":1737290420638,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":91,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540428961"},{"type":"electronic","value":"9783540456087"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45608-2_5","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:56:42Z","timestamp":1184605002000},"page":"262-330","source":"Crossref","is-referenced-by-count":18,"title":["Notes on Nominal Calculi for Security and Mobility"],"prefix":"10.1007","author":[{"given":"Andrew D.","family":"Gordon","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,10,31]]},"reference":[{"issue":"5","key":"5_CR1","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/324133.324266","volume":"46","author":"M. Abadi","year":"1999","unstructured":"M. Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749\u2013786, September 1999. 289, 323","journal-title":"Journal of the ACM"},{"issue":"4","key":"5_CR2","doi-asserted-by":"publisher","first-page":"706","DOI":"10.1145\/155183.155225","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi, M. Burrows, B. Lampson, and G. Plotkin. A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems, 15(4):706\u2013734, 1993. 273","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In 28th ACM Symposium on Principles of Programming Languages (POPL\u201901), pages 104\u2013115, 2001. 288, 289","DOI":"10.1145\/360204.360213"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"M. Abadi, C. Fournet, and G. Gonthier. Secure communications implementation of channel abstractions. In 13th IEEE Symposium on Logic in Computer Science (LICS\u201998), pages 105\u2013116, 1998. 289","DOI":"10.1109\/LICS.1998.705647"},{"key":"5_CR5","first-page":"267","volume":"5","author":"M. Abadi","year":"1998","unstructured":"M. Abadi and A. D. Gordon. A bisimulation method for cryptographic protocols. Nordic Journal of Computing, 5:267\u2013303, 1998. 289","journal-title":"Nordic Journal of Computing"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1998","unstructured":"M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148:1\u201370, 1999. An extended version with full proofs appears as Digital Equipment Corporation Systems Research Center report No. 149, January 1998. 264, 266","journal-title":"Information and Computation"},{"key":"5_CR7","series-title":"Lect Notes Comput Sci","volume-title":"COORDINATION 97","author":"R. M. Amadio","year":"1997","unstructured":"R. M. Amadio. An asynchronous model of locality, failure, and process mobility. In COORDINATION 97, volume 1282 of Lecture Notes in Computer Science. Springer, 1997. 293, 323"},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","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. 281","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/3-540-58715-2_126","volume-title":"Foundations of Software Technology and Theoretical Computer Science (FST&TCS\u201994)","author":"R. M. Amadio","year":"1994","unstructured":"R. M. Amadio and S. Prasad. Localities and failures. In Foundations of Software Technology and Theoretical Computer Science (FST&TCS\u201994), volume 880 of Lecture Notes in Computer Science, pages 205\u2013216. Springer, 1994. 317"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"R. Amadio and S. Prasad. The game of the name in cryptographic tables. In Advances in Computing Science (ASIAN\u201999), volume 1742 of Lectures Notes in Computer Science, pages 5\u201326. Springer, 1999. 289","DOI":"10.1007\/3-540-46674-6_3"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"M. Abadi and P. Rogaway. Reconciling two views of cryptography. In Theoretical Computer Science (IFIP TCS 2000), volume 1872 of Lectures Notes in Computer Science, pages 3\u201333. Springer, 2000. 273","DOI":"10.1007\/3-540-44929-9_1"},{"key":"5_CR12","doi-asserted-by":"publisher","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. 270,272, 273, 274","journal-title":"Proceedings of the Royal Society of London A"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"G. Berry and G. Boudol. The chemical abstract machine. In 17th ACM Symposium on Principles of Programming Languages (POPL\u201990), pages 81\u201394, 1990. 284","DOI":"10.1145\/96709.96717"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"M. Bugliesi and G. Castagna. Secure safe ambients. In 28th ACM Symposium on Principles of Programming Languages (POPL\u201901), pages 222\u2013235, 2001. 324","DOI":"10.1145\/360204.360223"},{"key":"5_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/BFb0055617","volume-title":"CONCUR\u201998: Concurrency Theory","author":"C. Bodei","year":"1998","unstructured":"C. Bodei, P. Degano, F. Nielson, and H. Nielson. Control flow analysis for the-calculus. In CONCUR\u201998: Concurrency Theory, volume 1466 of Lecture Notes in Computer Science, pages 84\u201398. Springer, 1998. 323"},{"issue":"2","key":"5_CR16","doi-asserted-by":"publisher","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. 272, 286","journal-title":"Information and Computation"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"M. Boreale, R. De Nicola, and R. Pugliese. Proof techniques for cryptographic processes. In 14th IEEE Symposium on Logic in Computer Science, pages 157\u2013166, 1999. 289","DOI":"10.1109\/LICS.1999.782608"},{"key":"5_CR18","unstructured":"D. Box. Essential COM. Addison-Wesley, 1998. 263"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"M. Bellare and P. Rogaway. Provably secure session key distribution: The three party case. In 27th ACM Symposium on Theory of Computing, 1995.273","DOI":"10.1145\/225058.225084"},{"key":"5_CR20","unstructured":"C. Bryce and J. Vitek. The JavaSeal mobile agent kernel. Agent Systems Journal, 2001. To appear. A preliminary version appears in the proceedings of the 3rd International Symposium on Mobile Agents (MA\/ASA\u201999), 1999. 266"},{"issue":"1","key":"5_CR21","first-page":"27","volume":"8","author":"L. Cardelli","year":"1995","unstructured":"L. Cardelli. A language with distributed scope. Computing Systems, 8(1):27\u201359, January 1995. 265, 292","journal-title":"Computing Systems"},{"key":"5_CR22","unstructured":"L. Cardelli. Mobile ambient synchronization. SRC Technical Note 1997-013, Digital Equipment Corporation Systems Research Center, July 1997.325"},{"key":"5_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/3-540-48749-2_4","volume-title":"Secure Internet Programming: Issues in Distributed and Mobile Object Systems","author":"L. Cardelli","year":"1999","unstructured":"L. Cardelli. Abstractions for mobile computation. In C. Jensen and J. Vitek, editors, Secure Internet Programming: Issues in Distributed and Mobile Object Systems, volume 1603 of Lecture Notes in Computer Science, pages 51\u201394. Springer, 1999. 265, 324"},{"key":"5_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Foundations of Software Science and Computation Structures (FoSSaCS\u2019 01)","author":"W. Charatonik","year":"2001","unstructured":"W. Charatonik, S. Dal Zilio, A. D. Gordon, S. Mukhopadhyay, and J.-M. Talbot. The complexity of model checking mobile ambients. In Foundations of Software Science and Computation Structures (FoSSaCS\u2019 01), Lecture Notes in Computer Science. Springer, 2001. To appear.324"},{"issue":"4","key":"5_CR25","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1145\/63334.63337","volume":"32","author":"N. Carriero","year":"1989","unstructured":"N. Carriero and D. Gelernter. Linda in context. Communications of the ACM, 32(4):444\u2013458, 1989. 292","journal-title":"Communications of the ACM"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"L. Cardelli and A. D. Gordon. Types for mobile ambients. In 26th ACM Symposium on Principles of Programming Languages (POPL\u201999), pages79\u201392, January 1999. 266, 298, 317, 324","DOI":"10.1145\/292540.292550"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"L. Cardelli and A. D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In 27th ACM Symposium on Principles of Programming Languages (POPL\u201900), pages 365\u2013377 2000. 324","DOI":"10.1145\/325694.325742"},{"key":"5_CR28","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(99)00231-5","volume":"240","author":"L. Cardelli","year":"2000","unstructured":"L. Cardelli and A. D. Gordon. Mobile ambients. Theoretical Computer Science, 240:177\u2013213, 2000. 265, 266, 294, 297, 324","journal-title":"Theoretical Computer Science"},{"key":"5_CR29","series-title":"Lect Notes Comput Sci","volume-title":"Typed Lambda Calculi and Applications (TLCA\u201901)","author":"L. Cardelli","year":"2001","unstructured":"L. Cardelli and A. D. Gordon. Logical properties of name restriction. In Typed Lambda Calculi and Applications (TLCA\u201901), Lecture Notes in Computer Science. Springer, 2001. To appear. 324"},{"key":"5_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-48523-6_20","volume-title":"26th International Colloquium on Automata, Languages and Programming (ICALP\u201999)","author":"L. Cardelli","year":"1999","unstructured":"L. Cardelli, G. Ghelli, and A. D. Gordon. Mobility types for mobile ambients. In 26th International Colloquium on Automata, Languages and Programming (ICALP\u201999), volume 1644 of Lecture Notes in Computer Science, pages 230\u2013239. Springer, 1999. 322, 324"},{"key":"5_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-44929-9_25","volume-title":"Theoretical Computer Science (IFIP TCS 2000)","author":"L. Cardelli","year":"2000","unstructured":"L. Cardelli, G. Ghelli, and A. D. Gordon. Ambient groups and mobility types. In Theoretical Computer Science (IFIP TCS 2000), volume 1872 of Lecture Notes in Computer Science, pages 333\u2013347. Springer, 2000. 266,324"},{"key":"5_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/3-540-44618-4_27","volume-title":"CONCUR 2000\u2014Concurrency Theory","author":"L. Cardelli","year":"2000","unstructured":"L. Cardelli, G. Ghelli, and A. D. Gordon. Group creation and secrecy. In C. Palamidessi, editor, CONCUR 2000\u2014Concurrency Theory, volume 1877 of Lecture Notes in Computer Science, pages 365\u2013379. Springer, 2000.323"},{"key":"5_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-59450-7_5","volume-title":"Object-Based Models and Languages for Concurrent Systems","author":"N. Carriero","year":"1995","unstructured":"N. Carriero, D. Gelernter, and L. Zuck. Bauhaus linda. In P. Ciancarini, O. Nierstrasz, and A. Yonezawa, editors, Object-Based Models and Languages for Concurrent Systems, volume 924 of Lecture Notes in Computer Science, pages 66\u201376. Springer, 1995. 292"},{"issue":"2\/3","key":"5_CR34","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76(2\/3):95\u2013120, February\/March 1988. 297","journal-title":"Information and Computation"},{"issue":"1","key":"5_CR35","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1996.0072","volume":"129","author":"M. Dam","year":"1996","unstructured":"M. Dam. Model checking mobile processes. Information and Computation,129(1):35\u201351, 1996. 272","journal-title":"Information and Computation"},{"key":"5_CR36","first-page":"255","volume":"VII","author":"M. Dam","year":"1998","unstructured":"M. Dam. Proving trust in systems of second-order processes. In 31st Hawaii International Conference on System Sciences, volume VII, pages 255\u2013264, 1998. 272","journal-title":"31st Hawaii International Conference on System Sciences"},{"key":"5_CR37","unstructured":"Data encryption standard. Fed. Inform. Processing Standards Pub. 46, National Bureau of Standards, Washington DC, January 1977. 274"},{"key":"5_CR38","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-48749-2_6","volume-title":"Secure Internet Programming 1999","author":"R. Nicola De","year":"1999","unstructured":"R. De Nicola, G. Ferrari, and R. Pugliese. Types as specifications of access policies. In Secure Internet Programming 1999, volume 1603 of Lecture Notes in Computer Science, pages 117\u2013146. Springer, 1999. 323"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"S. Dal Zilio and A. D. Gordon. Region analysis and a \u03c0-calculus with groups. In Mathematical Foundations of Computer Science 2000 (MFCS2000), volume 1893 of Lectures Notes in Computer Science, pages 1\u201321. Springer, 2000. 324","DOI":"10.1007\/3-540-44612-5_1"},{"issue":"6","key":"5_CR40","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"IT-22","author":"W. Diffie","year":"1976","unstructured":"W. Diffie and M. Hellman. New directions in cryptography. IEEE Transactions on Information Theory, IT-22(6):644\u2013654, November 1976. 287","journal-title":"IEEE Transactions on Information Theory"},{"key":"5_CR41","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. 286","journal-title":"Theoretical Computer Science"},{"issue":"8","key":"5_CR42","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1145\/358722.358740","volume":"24","author":"D. E. Denning","year":"1981","unstructured":"D. E. Denning and G. M. Sacco. Timestamps in key distribution protocols. Communications of the ACM, 24(8):533\u2013536, 1981. 264","journal-title":"Communications of the ACM"},{"issue":"2","key":"5_CR43","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"IT-29","author":"D. Dolev","year":"1983","unstructured":"D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(2):198\u2013208, 1983. 273","journal-title":"IEEE Transactions on Information Theory"},{"issue":"1","key":"5_CR44","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1994\/1995-3103","volume":"3","author":"R. Focardi","year":"1994","unstructured":"R. Focardi and R. Gorrieri. A classification of security properties for process algebra. Journal of Computer Security, 3(1):5\u201333, 1994. 273","journal-title":"Journal of Computer Security"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"C. Fournet and G. Gonthier. The reflexive CHAM and the Joincalculus. In 23rd ACM Symposium on Principles of Programming Languages (POPL\u201996), pages 372\u2013385, 1996. 264, 266, 293","DOI":"10.1145\/237721.237805"},{"key":"5_CR46","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1007\/3-540-61604-7_67","volume-title":"CONCUR\u201996: Concurrency Theory","author":"C. Fournet","year":"1996","unstructured":"C. Fournet, G. Gonthier, J.-J. L\u00e9vy, L. Maranget, and D. R\u00e9my. A calculus of mobile agents. In CONCUR\u201996: Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 406\u2013421. Springer, 1996. 266,293"},{"key":"5_CR47","series-title":"Lect Notes Comput Sci","volume-title":"Theoretical Computer Science (IFIP TCS 2000)","author":"C. Fournet","year":"2000","unstructured":"C. Fournet, J.-J. L\u00e9;vy, and A. Schmitt. An asynchronous, distributed implementation of mobile ambients. In Theoretical Computer Science (IFIP TCS 2000), volume 1872 of Lecture Notes in Computer Science. Springer, 2000. 266, 325"},{"key":"5_CR48","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/3-540-49019-1_15","volume":"1578","author":"A. D. Gordon","year":"1999","unstructured":"A. D. Gordon and L. Cardelli. Equational properties of mobile ambients. In Foundations of Software Science and Computation Structures (FoSSaCS\u201999), volume 1578 of Lecture Notes in Computer Science, pages 212\u2013226. Springer, 1999. An extended version appears as Microsoft Research Technical Report MSR-TR-99-11, April 1999. 324","journal-title":"Foundations of Software Science and Computation Structures (FoSSaCS\u201999)"},{"key":"5_CR49","unstructured":"A. D. Gordon and A. Jeffrey. Authenticity by typing for security protocols. Submitted for publication. Available at http:\/\/research.microsoft.com\/~adg\/Publications , 2001. 289"},{"key":"5_CR50","unstructured":"J. Gosling, B. Joy, and G. Steele. The Java language specification. Addison-Wesley, 1996. 292"},{"key":"5_CR51","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. 273","DOI":"10.1109\/CSFW.1995.518557"},{"key":"5_CR52","doi-asserted-by":"crossref","unstructured":"A. D. Gordon and D. Syme. Typing a multi-language intermediate code. In 28th ACM Symposium on Principles of Programming Languages (POPL\u201901), pages 248\u2013260, 2001. 297","DOI":"10.1145\/360204.360228"},{"key":"5_CR53","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-48294-6_9","volume-title":"Static Analysis Symposium (SAS\u201999)","author":"R. R. Hansen","year":"1999","unstructured":"R. R. Hansen, J. G. Jensen, F. Nielson, and H. R. Nielson. Abstract interpretation of mobile ambients. In Static Analysis Symposium (SAS\u201999), volume 1694 of Lecture Notes in Computer Science, pages 134\u2013148. Springer, 1999. 323"},{"key":"5_CR54","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985. 263"},{"key":"5_CR55","doi-asserted-by":"crossref","unstructured":"A. Igarashi and N. Kobayashi. A generic type system for the pi calculus. In 28th ACM Symposium on Principles of Programming Languages, pages 128\u2013141, 2001. 272","DOI":"10.1145\/360204.360215"},{"issue":"4","key":"5_CR56","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1109\/49.17707","volume":"7","author":"R. Kemmerer","year":"1989","unstructured":"R. Kemmerer. Analyzing encryption protocols using formal verification techniques. IEEE Journal on Selected Areas in Communications, 7(4):448\u2013457, 1989. 273","journal-title":"IEEE Journal on Selected Areas in Communications"},{"issue":"4","key":"5_CR57","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1145\/138873.138874","volume":"10","author":"B. Lampson","year":"1992","unstructured":"B. Lampson, M. Abadi, M. Burrows, and E. Wobber. Authentication in distributed systems: Theory and practice. ACM Transactions on Computer Systems, 10(4):265\u2013310, November 1992. 273","journal-title":"ACM Transactions on Computer Systems"},{"issue":"4","key":"5_CR58","doi-asserted-by":"publisher","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. 272","journal-title":"ACM Operating Systems Review"},{"key":"5_CR59","doi-asserted-by":"crossref","unstructured":"P. Lincoln, J. Mitchell, M. Mitchell, and A. Scedrov. A probabilistic poly-time framework for protocol analysis. In Fifth ACM Conference on Computer and Communications Security, pages 112\u2013121, 1998. 273","DOI":"10.1145\/288090.288117"},{"key":"5_CR60","doi-asserted-by":"crossref","unstructured":"G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In T. Margaria and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996), volume 1055 of Lectures Notes in Computer Science, pages 147\u2013166. Springer, 1996. 264, 273","DOI":"10.1007\/3-540-61042-1_43"},{"key":"5_CR61","doi-asserted-by":"crossref","unstructured":"F. Levi and D. Sangiorgi. Controlling interference in ambients. In 27th ACM Symposium on Principles of Programming Languages (POPL\u201900), pages 352\u2013364, 2000. 324","DOI":"10.1145\/325694.325741"},{"key":"5_CR62","doi-asserted-by":"crossref","unstructured":"T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1997. 297","DOI":"10.1016\/S1353-4858(97)83033-4"},{"key":"5_CR63","unstructured":"W. Mao. On two proposals for on-line bankcard payments using open networks: Problems and solutions. In IEEE Symposium on Security and Privacy, pages 201\u2013210, 1996. 289"},{"issue":"2","key":"5_CR64","doi-asserted-by":"publisher","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, 1987. 273","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"5_CR65","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. 273","journal-title":"Journal of Computer Security"},{"key":"5_CR66","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall International, 1989. 263"},{"key":"5_CR67","doi-asserted-by":"publisher","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. 283","journal-title":"Mathematical Structures in Computer Science"},{"key":"5_CR68","unstructured":"R. Milner. Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, 1999. 263, 272, 298, 318, 323"},{"key":"5_CR69","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-77, 1992. 263,272","DOI":"10.1016\/0890-5401(92)90009-5"},{"key":"5_CR70","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0304-3975(93)90156-N","volume":"114","author":"R. Milner","year":"1993","unstructured":"R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. Theoretical Computer Science, 114:149\u2013171, 1993. 272","journal-title":"Theoretical Computer Science"},{"key":"5_CR71","series-title":"Lect Notes Comput Sci","volume-title":"19th International Colloquium on Automata, Languages and Programming (ICALP\u201992)","author":"R. Milner","year":"1992","unstructured":"R. Milner and D. Sangiorgi. Barbed bisimulation. In 19th International Colloquium on Automata, Languages and Programming (ICALP\u201992), volume 623 of Lecture Notes in Computer Science. Springer, 1992. 272"},{"key":"5_CR72","doi-asserted-by":"crossref","unstructured":"R. M. Needham. Names. In S. Mullender, editor, Distributed Systems, pages 89\u2013101. Addison-Wesley, 1989. 263","DOI":"10.1145\/90417.90741"},{"key":"5_CR73","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"712","DOI":"10.1007\/BFb0030636","volume-title":"Proceedings TAPSOFT\u201997","author":"R. Nicola De","year":"1997","unstructured":"R. De Nicola, G.-L. Ferrari, and R. Pugliese. Locality based linda: programming with explicit localities. In Proceedings TAPSOFT\u201997, volume 1214 of Lecture Notes in Computer Science, pages 712\u2013726. Springer, 1997.293"},{"key":"5_CR74","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/3-540-48320-9_32","volume-title":"CONCUR\u201999: Concurrency Theory","author":"F. Nielson","year":"1999","unstructured":"F. Nielson, H. R. Nielson, R. R. Hansen, and J. G. Jensen. Validating firewalls in mobile ambients. In CONCUR\u201999: Concurrency Theory, volume 1664 of Lecture Notes in Computer Science, pages 463\u2013477. Springer, 1999. 323"},{"issue":"12","key":"5_CR75","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. M. Needham","year":"1978","unstructured":"R. M. Needham and M. D. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993\u2013999, 1978. 264, 272","journal-title":"Communications of the ACM"},{"key":"5_CR76","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"European Symposium on Programming (ESOP 2000)","author":"M. Odersky","year":"2000","unstructured":"M. Odersky. Functional nets. In European Symposium on Programming (ESOP 2000), volume 1782 of Lecture Notes in Computer Science, pages 1\u201325. Springer, 2000. 264"},{"issue":"5","key":"5_CR77","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1017\/S096012950007002X","volume":"6","author":"B. Pierce","year":"1996","unstructured":"B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409\u2013454, 1996. 272","journal-title":"Mathematical Structures in Computer Science"},{"key":"5_CR78","unstructured":"B. C. Pierce and D. N. Turner. Pict: A programming language based on the pi-calculus. In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000. 264"},{"key":"5_CR79","doi-asserted-by":"crossref","unstructured":"J. Riely and M. Hennessy. A typed language for distributed mobile processes. In 25th ACM Symposium on Principles of Programming Languages (POPL\u201998), pages 378\u2013390, 1998. 292, 317, 323","DOI":"10.1145\/268946.268978"},{"issue":"2","key":"5_CR80","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1145\/359340.359342","volume":"21","author":"R. L. Rivest","year":"1978","unstructured":"R. L. Rivest, A. Shamir, and L. Adleman. A method for obtaining digital signatures and public-key cryptosystems. Communications of the ACM, 21(2):120\u2013126, February 1978. 287","journal-title":"Communications of the ACM"},{"key":"5_CR81","doi-asserted-by":"crossref","unstructured":"D. Sangiorgi. Extensionality and intensionality of the ambient logics. In 28th ACM Symposium on Principles of Programming Languages (POPL\u201901), pages 4\u201313, 2001. 324","DOI":"10.1145\/360204.375707"},{"key":"5_CR82","doi-asserted-by":"crossref","unstructured":"S. Schneider. Security properties and CSP. In IEEE Symposium on Security and Privacy, pages 174\u2013187, 1996. 273","DOI":"10.1109\/SECPRI.1996.502680"},{"key":"5_CR83","unstructured":"B. Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C. John Wiley & Sons, Inc., second edition, 1996. 286"},{"key":"5_CR84","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/BFb0055094","volume-title":"25th International Colloquium on Automata, Languages and Programming (ICALP\u201998)","author":"P. Sewell","year":"1998","unstructured":"P. Sewell. Global\/local subtyping and capability inference for a distributed \u03c0-calculus. In 25th International Colloquium on Automata, Languages and Programming (ICALP\u201998), volume 1443 of Lecture Notes in Computer Science, pages 695\u2013706. Springer, 1998. 292, 317, 323"},{"key":"5_CR85","doi-asserted-by":"crossref","unstructured":"D. Sangiorgi and A. Valente. A distributed abstract machine for Safe Ambients. Available from the authors, 2001. 325","DOI":"10.1007\/3-540-48224-5_34"},{"key":"5_CR86","unstructured":"D. Sangiorgi and D. Walker. The \u03c0-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001. 263, 272"},{"issue":"2","key":"5_CR87","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1996.2613","volume":"132","author":"M. Tofte","year":"1997","unstructured":"M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109\u2013176, 1997. 323","journal-title":"Information and Computation"},{"key":"5_CR88","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/3-540-47959-7_3","volume-title":"Internet Programming Languages","author":"J. Vitek","year":"1999","unstructured":"J. Vitek and G. Castagna. Seal: A framework for secure mobile computations. In Internet Programming Languages, volume 1686 of Lecture Notes in Computer Science, pages 47\u201377. Springer, 1999. 266"},{"key":"5_CR89","unstructured":"J. E. White. Mobile agents. In J. Bradshaw, editor, Software Agents. AAAI Press\/The MIT Press, 1996. 265, 292"},{"key":"5_CR90","doi-asserted-by":"crossref","unstructured":"T. Y. C. Woo and S. S. Lam. A semantic model for authentication protocols. In IEEE Symposium on Security and Privacy, pages 178\u2013194, 1993.289","DOI":"10.1109\/RISP.1993.287633"},{"key":"5_CR91","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/3-540-46432-8_25","volume-title":"Foundations of Software Science and Computation Structures (FoSSaCS\u2019 00)","author":"P. Zimmer","year":"2000","unstructured":"P. Zimmer. Subtyping and typing algorithms for mobile ambients. In Foundations of Software Science and Computation Structures (FoSSaCS\u2019 00), volume 1784 of Lecture Notes in Computer Science, pages 375\u2013390. Springer, 2000. 300, 312, 324"}],"container-title":["Lecture Notes in Computer Science","Foundations of Security Analysis and Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45608-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T12:08:35Z","timestamp":1737288515000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45608-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540428961","9783540456087"],"references-count":91,"URL":"https:\/\/doi.org\/10.1007\/3-540-45608-2_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}