×

zbMATH — the first resource for mathematics

Towards a behavioural theory of access and mobility control in distributed systems. (English) Zbl 1071.68009
Summary: We define a typed bisimulation equivalence for the language \(D_PI\), a distributed version of the \(\pi\)-calculus in which processes may migrate between dynamically created locations. It takes into account resource access policies, which can be implemented in \(D_PI\) using a novel form of dynamic capability types. The equivalence, based on typed actions between configurations, is justified by showing that it is fully abstract with respect to a natural distributed version of a contextual equivalence.
In the second part of the paper we study the effect of controlling the migration of processes. This affects the ability to perform observations at specific locations, as the observer may be denied access. We show how the typed actions can be modified to take this into account, and generalise the full-abstraction result to this more delicate scenario.

MSC:
68M14 Distributed systems
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
SafeDpi
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] R.M. Amadio, S. Prasad, Modelling IP mobility, in: D. Sangiorgi, R. de Simone (Eds.), CONCUR’98: Concurrency Theory, 9th Internat. Conf., Nice, France, Lecture Notes in Computer Science, Vol. 1466, Springer, Berlin, 1998, pp. 301-316.
[2] M. Boreale, D. Sangiorgi, Bisimulation in name-passing calculi without matching, in: 13th LICS Conf., IEEE Computer Society Press, Silver Spring, MD, 1998.
[3] M. Bugliesi, S. Crafa, M. Merro, V. Sassone, Communication and mobility control in boxed ambients, Information and Computation, to appear, 2004. · Zbl 1101.68943
[4] Short version in Proc. POPL ’95;; A preliminary version appeared as Report 122, Digital Systems Research, June 1994.
[5] Cardelli, L.; Gordon, A.D., Mobile ambients, Theoret. comput. sci., 240, 1, 177-213, (2000) · Zbl 0954.68108
[6] G. Castagna, F.Z. Nardelli, The Seal calculus revisited: contextual equivalences and bisimilarity, in: Proc. FSTTCS, Lecture Notes in Computer Science, Springer, Berlin, 2002. · Zbl 1027.68088
[7] C. Fournet, G. Gonthier, J.-J. Lévy, L. Maranget, D. Rémy, A calculus of mobile agents, in: 7th Internat. Conf. on Concurrency Theory (CONCUR’96), Pisa, Italy, August 26-29, Lecture Notes in Computer Science, Vol. 1119, Springer, Berlin, 1996, pp. 406-421.
[8] Hennessy, M., Algebraic theory of processes, (1988), The MIT Press Cambridge, MA · Zbl 0744.68047
[9] M. Hennessy, J. Rathke, Typed behavioural equivalences for processes in the presence of subtyping, in: J. Harland (Ed.), Electronic Notes in Theoretical Computer Science, Vol. 61, Elsevier Science Publishers, Amsterdam, 2002;; Math. Structures Comput. Sci., to appear. · Zbl 1268.68127
[10] M. Hennessy, J. Rathke, N. Yoshida, Safedpi: a language for controlling mobile code, Computer Science Report 02:2003, University of Sussex, 2003. · Zbl 1081.68003
[11] Hennessy, M.; Riely, J., Resource access control in systems of mobile agents, Inform. and comput., 173, 82-120, (2002) · Zbl 1009.68081
[12] Honda, K.; Yoshida, N., On reduction-based process semantics, Theoret. comput. sci., 152, 2, 437-486, (1995) · Zbl 0871.68122
[13] Merro, M.; Hennessy, M., Bisimulation congruences in safe ambients, ACM SIGPLAN notices, 31, 1, 71-80, (2002) · Zbl 1323.68412
[14] Merro, M.; Kleist, J.; Nestmann, U., Mobile objects as mobile processes, J. inform. comput., 177, 2, 195-241, (2002) · Zbl 1093.68562
[15] M. Merro, F.Z. Nardelli, Bisimulation proof techniques for mobile ambients, in: Proc. 30th Internat. Coll. on Automata, Languages, and Programming (ICALP 2003), Eindhoven, Lecture Notes in Computer Science, Springer, Berlin, 2003. · Zbl 1039.68085
[16] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[17] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes (parts I and II), Inform. and comput., 100, 1-77, (1992)
[18] Extended abstract in LICS ’93. · Zbl 0861.68030
[19] P. Sewell, Global/local subtyping and capability inference for a distributed pi-calculus, in: ICALP 98, Lecture Notes in Computer Science, Vol. 1443, Springer, Berlin, 1998. · Zbl 0910.03021
[20] A. Unypoth, P. Sewell, Nomadic pict: correct communication infrastructure for mobile computation, in: Conf. Record of POPL’01: The 28th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, London, United Kingdom, January 17-19, 2001, pp. 236-247.
[21] J. Vitek, G. Castagna, A calculus of secure mobile computations, in: Secure Internet Programming: Security Issues for Distributed and Mobile Objects, Lecture Notes in Computer Science, Vol. 1603, Springer, Berlin, 1999.
[22] Yoshida, N.; Hennessy, M., Assigning types to processes, Inform. and comput., 172, 82-120, (2002) · Zbl 1009.68085
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.