A theory of noninterference for the pi-calculus

We develop a theory of noninterference for a typed version of the π- calculus where types are used to assign secrecy levels to channels. We provide two equivalent characterizations of noninterference based on a typed behavioural equivalence relative to a security level σ, which captures the idea of external ob- servers of level σ. The first characterization involves a universal quantification over all the possible active attacks, i.e., malicious processes which interact with the system possibly leaking secret information. The second definition of non- interference is expressed in terms of an unwinding condition, which deals with so-called passive attacks trying to infer confidential information just by observing the behaviour of the system. This unwinding-based characterization naturally leads to efficient methods for the verification and construction of (compositional) secure systems. Furthermore, we characterize noninterference in terms of bisimulation-like (partial) equivalence relations in the style of a stream of similar studies for other process calculi (e.g., CCS and CryptoSPA) and languages (e.g., imperative and multi-threaded languages).