Secrecy and group creation |
| |
Authors: | Luca Cardelli Giorgio Ghelli Andrew D Gordon |
| |
Affiliation: | aMicrosoft Research, Roger Needham Building, 7 Thomson Ave, Cambridge, UK;bDipartimento di Informatica, Università di Pisa, Via Buonarroti 2, Pisa, Italy |
| |
Abstract: | 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. |
| |
Keywords: | π -Calculus Secrecy Security types |
本文献已被 ScienceDirect 等数据库收录! |
|