P-congruences as noninterference for the pi-calculus.

We introduce a notion of noninterference for a typed version of the pi-calculus where types are used to assign secrecy levels to channels. Noninterference is expressed in terms of a partial congruence (p-congruence, for short). We provide a proof technique in the form of a bisimulation-like partial equivalence relation that is a binary relation which is symmetric and transitive but not reflexive. We show that the noninterference property is compositional with respect to most of the operators of the language leading to efficient proof techniques for the verification and the construction of (compositional) secure systems. In order to allow downgrading of sensitive information, we extend the pi-calculus with declassification primitives and we study a property which scales to noninterference when downgrading is not permitted.