Session Types for Access and Information Flow Control

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.

• Type: Conference
• Year: 2010
• Where: CONCUR
• Authors: Sara Capecchi, Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Tamara Rezk
• Keywords: CONCUR 2010, Distributed And Parallel Computing, Session Participants, Session Safety, Type Systems