Nobuko Yoshida, Kohei Honda and Martin Berger
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.