The Cπ-calculus: A model for confidential name passing

Sharing confidential information in distributed systems is often a necessity in the context of many applications, however, it opens the problem of controlling information sharing even among trusted parties. In this paper, we present a formal model in which dissemination of information, in particular information forwarding, is not allowed. Namely, we introduce a fragment of the π-calculus where forwarding of channels is disabled directly at the level of the syntax. This is the only difference with respect to the π-calculus, i.e., that channels that are received cannot be forwarded later on. Apart from the presentation of the language, we also address a preliminary investigation in the behavioral theory of the model. Furthermore, by means of examples, we give an idea of how some privacy notions already studied in the past, such as group creation and name hiding, can be represented in our language, in contrast with previous approaches that required additional language constructs. Finally, we present an encoding of the (sum-free) π-calculus in our calculus and prove operational correspondence. Our encoding allows to put focus on a notion of name ownership that arises in the process model, by confining the name sending capability to well-determined processes which may be of use for security purposes but also for other resource control properties.