×

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
PDFBibTeX XMLCite
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.; 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.; 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.; 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] A preliminary version appeared as Report 122, Digital Systems Research, June 1994.; 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.; 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.; 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: The MIT Press Cambridge, MA · Zbl 0744.68047
[9] Math. Structures Comput. Sci., to appear.; 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.; 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.; 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: 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.; 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.; 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.; 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.; 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. 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.