We add an operation of group creation to the typed pi-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. We adapt a notion of secrecy introduced by Abadi, and prove a preservation of secrecy property. When applied to the ambient calculus, the same notion of group creation can be used to create and preserve shared secrets among mobile agents. © Elsevier Ltd.
Secrecy and group creation
GHELLI, GIORGIO
2001-01-01
Abstract
We add an operation of group creation to the typed pi-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. We adapt a notion of secrecy introduced by Abadi, and prove a preservation of secrecy property. When applied to the ambient calculus, the same notion of group creation can be used to create and preserve shared secrets among mobile agents. © Elsevier Ltd.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
