Exploiting linear type structure, we introduce a new theory of weak
bisimilarity for the pi-calculus in which we abstract away not only
tau-actions but also non-tau actions which do not affect well-typed
observers. This gives a congruence far larger than the standard
bisimilarity while retaining semantic soundness. The framework is
smoothly extendible to other settings involving nondeterminism and
state. As an application we develop a behavioural theory of secrecy in
the pi-calculus which ensures secure information flow for a strictly
greater set of processes than the type-based approach in
[Honda et al. 99, Honda and Yoshida 02], while still offering
compositional verification techniques.
