Type systems for the pi-calculus have gained interest over the last few years as a framework for the analysis of security protocols. In this paper, the authors develop an extended, typed pi-calculus based on the notion of a group. Under this new approach, each name belongs to a group, which may be created dynamically by a creation operator. In this context, the type system prevents information leaks (secrets).
The authors devote significant effort to studying the secrecy properties derived from the notion of a group. As in some other contributions to this area, one of the key results of the paper is a theorem that guarantees the secrecy of names. In this case, however, the secrecy is relative to an “untyped” opponent, which is a strong result.
In the conclusion, the authors present some brief notes on related work. The apparent connection between the groups introduced in this work and the channels and binders used in control flow analysis as presented in Bodei et al. [1] is explicitly mentioned. Despite the differences that exist, I suspect that both approaches could benefit from a deeper study of these connections. In fact, some other works have also established very interesting relationships between typed process calculus and other systems [2].