P-Congruences as Non-Interference for the Pi-calculus

Abstract. We develop a theory of non-interference for a typed version of the pi-calculus where types are used to assign secrecy levels to channels. We provide two equivalent characterizations of non-interference based on a typed behavioural equivalence relative to a security level σ, which cap-tures the idea of external observers 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 be-haviour of the system. This unwinding-based characterization naturally leads to efficient methods for the verification and construction of (compo-sitional) secure systems. Furthermore, we characterize non-interference 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 Cryp-toSPA) and languages (e.g., imperative and multi-threaded languages).