Secure Information Flow as Typed Process Behaviour

  • Kohei Honda
  • Vasco Vasconcelos
  • Nobuko Yoshida
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)


We propose a new type discipline for the π-calculus in which secure information flow is guaranteed by static type checking. Secrecy levels are assigned to channels and are controlled by subtyping. A behavioural notion of types capturing causality of actions plays an essential role for ensuring safe information flow in diverse interactive behaviours, making the calculus powerful enough to embed known calculi for type-based security. The paper introduces the core part of the calculus, presents its basic syntactic properties, and illustrates its use as a tool for programming language analysis by a sound embedding of a secure multi-threaded imperative calculus of Volpano and Smith. The embedding leads to a practically meaningful extension of their original type discipline.


Secure Information Action Type Safe Information Passing Process Imperative Variable 
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.


  1. 1.
    Abadi, M., Secrecy by typing in security protocols. TACS’97, LNCS, 611–637, Springer, 1997.Google Scholar
  2. 2.
    Abadi, M., Banerjee, A., Heintze, N. and Riecke, J., A core calculus of dependency, POPL’99, ACM, 1999.Google Scholar
  3. 3.
    Abadi, M., Fournet, C. and Gonthier, G., Secure Communications Processing for Distributed Languages. LICS’98, 868–883, IEEE, 1998.Google Scholar
  4. 4.
    Abramsky, S., Computational Interpretation of Linear Logic. TCS, vol 111, 1993.Google Scholar
  5. 5.
    Bodei, C, Degano, P., Nielson, F., and Nielson, H. Control Flow Analysis of π-Calculus. CONCUR’98, LNCS 1466, 84–98, Springer, 1998.Google Scholar
  6. 6.
    Boudol, G., The pi-calculus in direct style, POPL’97, 228–241, ACM, 1997.Google Scholar
  7. 7.
    Denning, D. and Denning, P., Certification of programs for secure information flow. Communication of ACM, ACM, 20:504–513, 1997.CrossRefGoogle Scholar
  8. 8.
    Focardi, R. and Gorrieri, R., The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering, 23(9), 1997.Google Scholar
  9. 9.
    Gay, S. and Hole, M., Types and Subtypes for Client-Server Interactions, ESOP’99, LNCS 1576, 74–90, Springer, 1999.Google Scholar
  10. 10.
    Girard, J.-Y., Linear Logic, TCS, Vol. 50, 1–102, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Goguen, J. and Meseguer, J., Security policies and security models. IEEE Symposium on Security and Privacy, 11–20, IEEE, 1982.Google Scholar
  12. 12.
    Gong, L., Prafullchandra, H. and Shcemers, R., Going beyond sandbox: an overview of the new security architecture in the Java development kit 1.2. USENIX Symposium on Internet Technologies and Systems, 1997.Google Scholar
  13. 13.
    Gray, J., Probabilistic interference. Symposium on Security and Privacy, 170–179, IEEE, 1990.Google Scholar
  14. 14.
    Honda, K., Types for Dyadic Interaction. CONCUR’93, LNCS 715, 509–523, 1993.Google Scholar
  15. 15.
    Honda, K., Composing Processes, POPL’96, 344–357, ACM, 1996.Google Scholar
  16. 16.
    A full version of the present paper, QMW CS technical report 767, 1999. Available at
  17. 17.
    Honda, K. and Yoshida, N. On Reduction-Based Process Semantics. TCS. 151, 437–486, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Honda, K. and Yoshida, N. Game-theoretic analysis of call-by-value computation. TCS, 221 (1999), 393–456, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Hyland, M. and Ong, L., Pi-calculus, dialogue games and PCF, FPCA’93, ACM, 1995.Google Scholar
  20. 20.
    Kobayashi, N., Pierce, B., and Turner, D., Linear types and π-calculus, POPL’96, 358–371, 1996.Google Scholar
  21. 21.
    Lafont, Y., Interaction Nets, POPL’90, 95–108, ACM, 1990.Google Scholar
  22. 22.
    Larsen, K. and Skou, A. Bisimulation through probabilistic testing. Information and Computation, 94:1–28, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    Lopes, L, Silva, F. and Vasconcelos, F. A Virtual Machine for the TyCO Process Calculus. PPDP’99, 244–260, LNCS 1702, Springer, 1999.Google Scholar
  24. 24.
    Lowe, G. Defining Information Flow. MCS technical report, University of Leicester, 1999/3, 1999.Google Scholar
  25. 25.
    McLean, J. Security models and information flow. IEEE Symposium on Security and Privacy, 1990.Google Scholar
  26. 26.
    Milner, R., Communication and Concurrency, Prentice-Hall, 1989.Google Scholar
  27. 27.
    Milner, R., Parrow, J.G. and Walker, D.J., A Calculus of Mobile Processes, Info. & Comp. 100(1), pp.1–77, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  28. 28.
    Pierce, B and Sangiorgi. D, Typing and subtyping for mobile processes, MSCS 6(5):409–453, 1996.zbMATHMathSciNetGoogle Scholar
  29. 29.
    Roscoe, A. W. Intensional Specifications of Security Protocols, CSFW’96, IEEE, 1996.Google Scholar
  30. 30.
    Sangiorgi, D. π-calculus, internal mobility, and agent-passing calculi. TCS, 167(2):235–271, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  31. 31.
    Schneider, S. Security properties and CSP. Symposium on Security and Privacy, 174–187, 1996.Google Scholar
  32. 32.
    Vasconcelos, V., Typed concurrent objects. ECOOP’94, LNCS 821, pp.100–117. Springer, 1994.Google Scholar
  33. 33.
    Volpano, D. and Smith, G., Secure information flow in a multi-threaded imperative language, pp.355–364, POPL’98, ACM, 1998.Google Scholar
  34. 34.
    Volpano, D. and Smith, G., Language Issues in Mobile Program Security. to appear in LNCS, Springer, 1999.Google Scholar
  35. 35.
    Volpano, D., Smith, G. and Irvine, C., A Sound type system for secure flow analysis. J. Computer Security, 4(2,3):167–187, 1996.Google Scholar
  36. 36.
    Yoshida, N. Graph Types for Mobile Processes. FST/TCS’16, LNCS 1180, pp.371–386, Springer, 1996. The full version as LFCS Technical Report, ECS-LFCS-96-350, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Kohei Honda
    • 1
  • Vasco Vasconcelos
    • 2
  • Nobuko Yoshida
    • 3
  1. 1.Queen Mary and Westfield CollegeLondonUK
  2. 2.University of LisbonLisbonPortugal
  3. 3.University of LeicesterLeicesterUK

Personalised recommendations