Skip to main content

Session Types for Access and Information Flow Control

  • Conference paper
CONCUR 2010 - Concurrency Theory (CONCUR 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6269))

Included in the following conference series:

Abstract

We consider a calculus for multiparty sessions with delegation, enriched with security levels for session participants and data. We propose a type system that guarantees both session safety and a form of access control. Moreover, this type system ensures secure information flow, including controlled forms of declassification. In particular, the type system prevents leaks that could result from an unrestricted use of the control constructs of the calculus, such as session opening, selection, branching and delegation. We illustrate the use of our type system with a number of examples, which reveal an interesting interplay between the constraints used in security type systems and those used in session types to ensure properties like communication safety and session fidelity.

Work partially funded by the INRIA Sophia Antipolis COLOR project MATYSS, by the ANR-SETI-06-010 and ANR-08-EMER-010 grants, and by the MIUR Projects DISCO and IPODS.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
CHF34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
CHF 24.95
Price includes VAT (Switzerland)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
CHF 94.00
Price excludes VAT (Switzerland)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
CHF 118.00
Price excludes VAT (Switzerland)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Almeida Matos, A., Boudol, G.: On Declassification and the Non-Disclosure Policy. Journal of Computer Security 17, 549–597 (2009)

    Google Scholar 

  2. Bettini, L., Coppo, M., D’Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global Progress in Dynamically Interleaved Multiparty Sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. In: Proc. CSF 2009, pp. 124–140. IEEE Computer Society, Los Alamitos (2009)

    Google Scholar 

  4. Boreale, M., Bruni, R., Nicola, R., Loreti, M.: Sessions and Pipelines for Structured Service Programming. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 19–38. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Boudol, G., Kolundzija, M.: Access Control and Declassification. In: Proc. Computer Network Security. CCIS, vol. 1, pp. 85–98. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Denning, D.E.R.: Cryptography and Data Security. Addison-Wesley, Reading (1982)

    MATH  Google Scholar 

  7. Dezani-Ciancaglini, M., de’Liguoro, U.: Sessions and Session Types: An Overview. In: Laneve, C. (ed.) WSFM 2010. LNCS, vol. 6194, pp. 1–28. Springer, Heidelberg (2010)

    Google Scholar 

  8. Focardi, R., Gorrieri, R.: Classification of Security Properties (Part I: Information Flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  9. Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proc. IEEE Symposium on Security and Privacy, pp. 11–20. IEEE Computer Society, Los Alamitos (1982)

    Google Scholar 

  10. Honda, K., Yoshida, N.: A Uniform Type Structure for Secure Information Flow. In: Proc. POPL 2002, pp. 81–92. ACM Press, New York (2002)

    Google Scholar 

  11. Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchronous Session Types. In: Proc. POPL 2008, pp. 273–284. ACM Press, New York (2008)

    Chapter  Google Scholar 

  12. Kobayashi, N.: Type-Based Information Flow Analysis for the Pi-Calculus. Acta Informatica 42(4-5), 291–347 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  13. Kolundžija, M.: Security Types for Sessions and Pipelines. In: Bruni, R., Wolf, K. (eds.) WSFM 2008. LNCS, vol. 5387, pp. 175–190. Springer, Heidelberg (2009)

    Google Scholar 

  14. Milner, R.: Communicating and Mobile Systems: the Pi-Calculus. CUP, Cambridge (1999)

    Google Scholar 

  15. Planul, J., Corin, R., Fournet, C.: Secure Enforcement for Global Process Specifications. In: Proc. CONCUR 2009. LNCS, vol. 5710, pp. 511–526. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  16. Sabelfeld, A., Myers, A.C.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)

    Article  Google Scholar 

  17. Sabelfeld, A., Sands, D.: Probabilistic Noninterference for Multi-threaded Programs. In: Proc. CSFW 2000, pp. 200–214. IEEE Computer Society, Los Alamitos (2000)

    Google Scholar 

  18. Sabelfeld, A., Sands, D.: Dimensions and Principles of Declassification. In: Proc. CSFW 2005. IEEE Computer Society, Los Alamitos (2005)

    Google Scholar 

  19. Smith, G., Volpano, D.: Secure Information Flow in a Multi-threaded Imperative Language. In: Proc. POPL 1998, pp. 355–364. ACM Press, New York (1998)

    Chapter  Google Scholar 

  20. Takeuchi, K., Honda, K., Kubo, M.: An Interaction-based Language and its Typing System. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994)

    Google Scholar 

  21. Volpano, D., Irvine, C., Smith, G.: A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4(2,3), 167–187 (1996)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Capecchi, S., Castellani, I., Dezani-Ciancaglini, M., Rezk, T. (2010). Session Types for Access and Information Flow Control . In: Gastin, P., Laroussinie, F. (eds) CONCUR 2010 - Concurrency Theory. CONCUR 2010. Lecture Notes in Computer Science, vol 6269. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15375-4_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15375-4_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15374-7

  • Online ISBN: 978-3-642-15375-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

  NODES
INTERN 1
Note 2
Project 2