Session Types for Access and Information Flow Control

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, it prevents leaks due to the specific 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 of security type systems and those used in session types to ensure properties like communication safety and session fidelity.
Document type :
Reports
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/inria-00511304
Contributor : Ilaria Castellani <>
Submitted on : Wednesday, August 25, 2010 - 12:17:02 PM
Last modification on : Thursday, January 11, 2018 - 4:24:41 PM
Long-term archiving on : Tuesday, October 23, 2012 - 3:00:45 PM

File

RR-7368.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00511304, version 1

Collections

Citation

Sara Capecchi, Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Tamara Rezk. Session Types for Access and Information Flow Control. [Research Report] RR-7368, INRIA. 2010, pp.48. ⟨inria-00511304⟩

Share

Metrics

Record views

231

Files downloads

302