A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation

  • Daisuke Hoshina
  • Eijiro Sumii
  • Akinori Yonezawa
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)


We propose the πD-calculus, a process calculus that can flexibly model fine-grained control of resource access in distributed computation, with a type system that statically prevents access violations. Access control of resources is important in distributed computation, where resources themselves or their contents may be transmitted from one domain to another and thereby vital resources may be exposed to unauthorized processes. In πD, a notion of hierarchical domains is introduced as an abstraction of protection domains, and considered as the unit of access control. Domains are treated as first-class values and can be created dynamically. In addition, the hierarchal structure of domains can be extended dynamically as well. These features are the source of the expressiveness of πD. This paper presents the syntax, the operational semantics, and the type system of πD, with examples to demonstrate its expressiveness.


Access Control Type System Mobile Agent Operational Semantic Typing Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. In Proceedings of the Fourth ACM Conference on Computer and Communications Security. ACM Press, 1997.Google Scholar
  2. 2.
    M. Bugliesi and G. Castagna. Secure safe ambients. In POPL’01. ACM Press, 2001.Google Scholar
  3. 3.
    L. Cardelli and A. D. Gordon. Mobile ambients. In FoSSaCS’98. Springer-Verlag, 1998.Google Scholar
  4. 4.
    L. Cardelli and A. D. Gordon. Secrecy and group creation. In CONCUR’2000. Springer-Verlag, 2000.Google Scholar
  5. 5.
    R. De Nicola, G. Ferrari, and R. Pugliese. Klaim: a kernel language for agents interaction and mobility. IEEE Trans. on Software Engineering, 24(5), 1998.Google Scholar
  6. 6.
    M. Dezani-Ciancaglini and I. Salvo. Security types for mobile safe ambients. In ASIAN’00, 2000.Google Scholar
  7. 7.
    C. Fournet, G. Gonthier, J. J. Levy, L. Maranget, and D. Remy. A calculusof mobile agents. In CONCUR’96. Springer-Verlag, 1996.Google Scholar
  8. 8.
    J. Gosling, B. Joy, and G. Steele. The Java language specification. Addison-Wesley, 1996.Google Scholar
  9. 9.
    N. Heintze and J. G. Riecke. The SLam calculus: Programming with secrecy and integrity. In POPL’98. ACM Press, 1998.Google Scholar
  10. 10.
    M. Hennessy and J. Riely. Resource access control in systems of mobile agents. In HLCL’98. Elsevier, 1998.Google Scholar
  11. 11.
    M. Hennessy and J. Rily. Information flow vs. resource access in the asynchronous pi-calculus(extended abstract). In ICALP’00, January 2000.Google Scholar
  12. 12.
    D. Hoshina, E. Sumii, and A. Yonezawa. A typed process calculus for fine-grained resource access control in distributed computation (full version), 2001. Available from
  13. 13.
    N. Kobayashi, B. Pierce, and D. Turner. Linearity and the pi-calculus. In POPL’96. ACM Press, 1996.Google Scholar
  14. 14.
    F. Levi and D. Sangiorgi. Controlling interference in ambients. In POPL’00. ACM Press, 2000.Google Scholar
  15. 15.
    R. Milner. The polyadic π-calculus: a tutorial. Technical Report ECS-LFCS-91-180, Laboratory for Foundationsof Computer Science,Department of Computer Science, University of Edinburgh, Octorber 1991.Google Scholar
  16. 16.
    B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structure in Computer Science, 6(5):409–454, 1996.zbMATHMathSciNetGoogle Scholar
  17. 17.
    B. Pierce and D. Sangiorgi. Behavioral equivalence in the polymorphic pi-calculus. In POPL’97. ACM Press, 1997.Google Scholar
  18. 18.
    J. Riely and M. Hennessy. A typed language for distributed mobile processes. In POPL’98. ACM Press, 1998.Google Scholar
  19. 19.
    J. Riely and M. Hennessy. Trust and partial typing in open systems of mobile agents. In POPL’99. ACM Press, 1999.Google Scholar
  20. 20.
    P. Sewell. Global/local subtyping and capability inference for a distributed π-calculus. In ICALP’98. Springer-Verlag, 1998. LNCS 1433.Google Scholar
  21. 21.
    J. Vitek and G. Castagna. Seal: A framework for secure mobile computations. In Internet Programming Languages, 1999. LNCS 1686.CrossRefGoogle Scholar
  22. 22.
    N. Yoshida and M. Hennessy. Assigning types to processes. In LICS’00. IEEE, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Daisuke Hoshina
    • 1
  • Eijiro Sumii
    • 2
  • Akinori Yonezawa
    • 2
  1. 1.TOSHIBA CorporationJapan
  2. 2.Department of Computer Science, Graduate School of Information Science and EngineeringUniversity of TokyoJapan

Personalised recommendations