×

Communication and mobility control in boxed ambients. (English) Zbl 1101.68943

Summary: Boxed Ambients (BA) replace Mobile Ambients’ open capability with communication primitives acting across ambient boundaries. The expressiveness of the new communication model is achieved at the price of communication interferences whose resolution requires synchronisation of activities at multiple, distributed locations. We study a variant of BA aimed at controlling communication as well as mobility interferences. Our calculus modifies the communication mechanism of BA, and introduces a new form of co-capability, inspired from Safe Ambients (SA) (with passwords), that registers incoming agents with the receiver ambient while at the same time performing access control. We prove that the new calculus has a rich semantics theory, including a sound and complete coinductive characterisation, and an expressive, yet simple type system. Through a set of examples, and an encoding, we characterise its expressiveness with respect to both BA and SA.

MSC:

68U35 Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.)

Keywords:

Safe Ambients

References:

[1] Arun-Kumar, S.; Hennessy, M.: An efficiency preorder for processes. Acta informatica 29, 737-760 (1992) · Zbl 0790.68039
[2] Boreale, M.: On the expressiveness of internal mobility in name-passing calculi. Theoretical computer science 195, 205-226 (1998) · Zbl 0915.68059
[3] M. Bugliesi, G. Castagna, S. Crafa, Access Control for Mobile Agents: the Calculus of Boxed Ambients, TOPLAS, ACM Transactions on Programming Languages and Systems 26 (1) (2004) 57-124. An extended abstract appeared in TACS’01, LNCS 2215, 2001. · Zbl 1087.68541
[4] M. Bugliesi, S. Crafa, M. Merro, V. Sassone, Communication interference in mobile boxed ambients, in: FSTTCS’02, 22th Conference on the Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, vol. 2556, Springer, Berlin, 2002, pp. 71-84. · Zbl 1027.68086
[5] L. Cardelli, A. Gordon Mobile Ambients, Theoretical Computer Science 240 (1) (2000) 177-213, An extended abstract appeared in FoSSaCS’98, LNCS 1378, 1998.
[6] Cardelli, L.; Gordon, A.: Equational properties for mobile ambients. Mathematical structures in computer science 13, No. 3, 371-408 (2003) · Zbl 1085.68099
[7] L. Cardelli, Global computing, slides (2000).
[8] G. Castagna, F. Zappa Nardelli, The Seal Calculus revisited: contextual equivalence and bisimilarity, in: FST&TCS ’02, 22th Conference on the Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, vol. 2556, Springer, Berlin, 2002, pp. 85-96. · Zbl 1027.68088
[9] G. Castagna, J. Vitek, F. Zappa Nardelli, The Seal Calculus, Information and Computation x (x) (2005) xx-xx (to appear). Available from: <http://www.di.ens.fr/ castagna>. · Zbl 1101.68060
[10] S. Crafa, M. Bugliesi, G. Castagna, Information flow security for boxed ambients, in: F-WAN, International Workshop on Foundations of Wide Area Network Computing, ENTCS, vol. 66.3 Elsevier, 2002. · Zbl 1268.68123
[11] C. Fournet, J.-J. Levy, A. Schmitt, An asynchronous, distributed implementation of mobile ambients, in: IFIP TCS 2000, International Conference on Theoretical Computer Science, Lecture Notes in Computer Science, vol. 1872, Springer, Berlin, 2000, pp. 348-364. · Zbl 0998.68537
[12] Honda, K.; Yoshida, N.: On reduction-based process semantics. Theoretical computer science 152, No. 2, 437-486 (1995) · Zbl 0871.68122
[13] F. Levi, D. Sangiorgi, Mobile safe ambients, TOPLAS, ACM Transactions on Programming Languages and Systems 25 (1) (2003) 1-69, An extended abstract appeared in POPL’00, 27th ACM Symposium on Principles of Programming Languages, 2000. · Zbl 1323.68411
[14] M. Merro, M. Hennessy, A bisimulation-based semantic theory of Safe Ambients, TOPLAS, ACM Transactions on Programming Languages and Systems x (x) (2005) xx-xx (to appear). An extended abstract appeared in POPL’02, 29th ACM Symposium on Principles of Programming Languages, 2002.
[15] M. Merro, V. Sassone, Typing and subtyping mobility in boxed ambients, in: CONCUR’02, 14th International Conference on Concurrency Theory, Lecture Notes in Computer Science, vol. 2421, Springer, Berlin, 2002, pp. 304-320. · Zbl 1012.68529
[16] M. Merro, F. Zappa-Nardelli, Bisimulation proof methods for mobile ambients, in: ICALP’03, 30th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 2719, Springer, Berlin, 2003, pp. 584-598. · Zbl 1039.68085
[17] Milner, R.; Parrow, J.; Walker, D.: A calculus of mobile processes, parts I and II. Information and computation 100, 1-77 (1992) · Zbl 0752.68037
[18] R. Milner, D. Sangiorgi, Barbed bisimulation, in: ICALP’92, 19th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 623, Springer, Berlin, 1992, pp. 685-695.
[19] Milner, R.: Communicating and mobile systems: the \({\pi}\)-calculus. (1999) · Zbl 0942.68002
[20] Nestmann, U.: What is a ’good’ encoding of guarded choice?. Information and computation 156, 287-319 (2000) · Zbl 1046.68625
[21] A. Phillips, N. Yoshida, S. Eisenbach, A distributed abstract machine for boxed ambient calculi, in: ESOP’04, 7th European Symposium on Programming, LNCS, vol. 2986, Springer, Berlin, 2004, pp. 155-170. · Zbl 1126.68507
[22] Pierce, B.; Nestmann, U.: Decoding choice encodings. Information and computation 163, No. 1, 1-59 (2000) · Zbl 1003.68080
[23] D. Sangiorgi, Expressing mobility in process algebras: first-order and higher-order paradigms, PhD thesis CST-99-93, Department of Computer Science, University of Edinburgh, 1992.
[24] D. Sangiorgi, Extensionality and intensionality of the ambient logic, in: POPL’01, 28th ACM Symposium on Principles of Programming Languages, ACM Press, 2001, pp. 4-13. · Zbl 1323.68415
[25] D. Sangiorgi, A. Valente, A distributed abstract machine for Safe Ambients, in: ICALP’01, 28th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 2076, Springer, Berlin, 2001, pp. 408-420. · Zbl 0986.68511
[26] D. Sangiorgi, R. Milner, The problem of ”Weak Bisimulation up to”, in: CONCUR’92, 3rd International Conference on Concurrency Theory, Lecture Notes in Computer Science, vol. 630, Springer, Berlin, 1992, pp. 32-46.
[27] Sangiorgi, D.; Walker, D.: The pi-calculus: A theory of mobile processes. (2001) · Zbl 0981.68116
[28] Sangiorgi, D.: Bisimulation for higher-order process calculi. Information and computation 131, No. 2, 141-178 (1996) · Zbl 0876.68042
[29] J. Vitek, G. Castagna, Seal: a framework for secure mobile computations, in: ICCL Workshop: Internet Programming Languages, Lecture Notes in Computer Science, vol. 1686, Springer, Berlin, 1999, pp. 47-77.
[30] F. Zappa-Nardelli, De la sémantique des processus d’ordre supérieur, PhD thesis, Université Paris 7, 2003.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.