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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
M. Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749–786, September 1999.
M. Abadi. Security protocols and specifications. In Proceedings FOSSACS’99, volume 1578 of LNCS, pages 1–13. Springer, 1999.
M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148:1–70, 1999.
C. Bodei, P. Degano, F. Nielson, and H. Nielson. Control flow analysis for the π-calculus. In Proceedings Concur’98, volume 1466 of LNCS, pages 84–98. Springer, 1998.
L. Cardelli, G. Ghelli, and A. D. Gordon. Ambient groups and mobility types. In Proceedings TCS2000, LNCS. Springer, 2000. To appear.
S. Dal Zilio and A. D. Gordon. Region analysis and a π-calculus with groups. In Proceedings MFCS2000, LNCS. Springer, 2000. To appear.
D. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236–242, 1976.
D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IC-29(12):198–208, 1983.
S. J. Gay. A sort inference algorithm for the polyadic pi-calculus. In Proceedings POPL’93. ACM, 1993.
R. Milner. Communicating and Mobile Systems: the π-Calculus. CUP, 1999.
M. Odersky. Polarized name passing. In Proc. FST & TCS, LNCS. Springer, December 1995.
B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409–454, 1996.
J. Riely and M. Hennessy. A typed language for distributed mobile processes. In Proceedings POPL’98, pages 378–390. ACM, 1998.
P. Sewell. Global/local subtyping and capability inference for a distributed π-calculus. In Proceedings ICALP’98, volume 1443 of LNCS, pages 695–706. Springer, 1998.
M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.
V. T. Vasconcelos and K. Honda. Principal typing-schemes in a polyadic π-calculus. In Proceedings Concur’93, volume 715 of LNCS, pages 524–538. Springer, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cardelli, L., Ghelli, G., Gordon, A.D. (2000). Secrecy and Group Creation. In: Palamidessi, C. (eds) CONCUR 2000 — Concurrency Theory. CONCUR 2000. Lecture Notes in Computer Science, vol 1877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44618-4_27
Download citation
DOI: https://doi.org/10.1007/3-540-44618-4_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67897-7
Online ISBN: 978-3-540-44618-7
eBook Packages: Springer Book Archive