Secrecy and Group Creation

We add an operation of group creation to the typed π-calculus, where a group is a type for channels. Creation of fresh groups has the effect of statically preventing certain communications, and can block the accidental or malicious leakage of secrets. Intuitively, no channel belonging to a fresh group can be received by processes outside the initial scope of the group, even if those processes are untyped. We formalize this intuition by adapting a notion of secrecy introduced by Abadi, and proving a preservation of secrecy property. Key words: π-calculus, secrecy, security types

• Type: Conference
• Year: 2000
• Where: CONCUR
• Authors: Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon
• Keywords: CONCUR 2000, Distributed And Parallel Computing, Fresh Group, Group, Group Creation