Information flow vs. Resource access in the asynchronous pi-caleulus

45Citations
Citations of this article
31Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We propose an extension of the asynchronous π-calculus in which a variety of security properties may be captured using types. These are an extension of the Input/Output types for the π-calculus in which I/O capabilities are assigned specific security levels. We define a typing system which ensures that processes running at security level σ cannot access resources with a security level higher than σ. The notion of access control guaranteed by this system is formalized in terms of a Type Safety theorem. We then show that, for a certain class of processes, our system prohibits implicit information flow from high-level to low-level processes. We prove that low-level behaviour can not be influenced by changes to high-level behaviour. This is formalized as a Non-Interference Theorem with respect to may testing.

Cite

CITATION STYLE

APA

Hennessy, M., & Riely, J. (2000). Information flow vs. Resource access in the asynchronous pi-caleulus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1853, pp. 415–427). Springer Verlag. https://doi.org/10.1007/3-540-45022-x_35

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free