A typed theory for access control and information flow control in mobile systems

We propose a novel security type system for the pi-calculus in which a fine-grained access control mechanism is guaranteed by static type checking and secure information flow can be characterized by a new form of non-interference property based on typed behavioral equivalence. In this paper, we present the syntax, subtyping rules, and typing rules of the type system, and explain how the secure data access can be controlled by typing. And then we elaborate a framework of typed level bisimulation to construct the secure information flow property named as non-interference at level. Moreover, some results are presented to indicate that our theory is an efficient enforceable model to support the specification and analysis of secure mobile systems.