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. |
Year | DOI | Venue |
---|---|---|
2005 | 10.1016/j.ic.2004.08.003 | Information & Computation |
Keywords | Field | DocType |
group creation,initial scope,security types,secrecy,π -calculus,malicious leakage,fresh group,secrecy property,certain communication | Operational semantics,Computer science,Computer security,Secrecy,Control flow,π-calculus,Intuition,Communication channel,Theoretical computer science | Journal |
Volume | Issue | ISSN |
196 | 2 | Information and Computation |
Citations | PageRank | References |
24 | 1.56 | 16 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Luca Cardelli | 1 | 6221 | 1002.41 |
Giorgio Ghelli | 2 | 1300 | 255.19 |
Andrew Gordon | 3 | 3713 | 268.70 |