Mobile values, new names, and secure communication
Top Cited Papers
- 1 January 2001
- journal article
- conference paper
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 36 (3) , 104-115
- https://doi.org/10.1145/373243.360213
Abstract
We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security protocols, which are the main motivating examples for our work; it also appears in other programming-language contexts. Specifically, we introduce a simple, general extension of the pi calculus with value passing, primitive functions, and equations among terms. We develop semantics and proof techniques for this extended language and apply them in reasoning about some security protocols.Keywords
This publication has 20 references indexed in Scilit:
- Secrecy by typing in security protocolsJournal of the ACM, 1999
- A Calculus for Cryptographic Protocols: The Spi CalculusInformation and Computation, 1999
- On the bisimulation proof methodMathematical Structures in Computer Science, 1998
- A hierarchy of equivalences for asynchronous calculiPublished by Springer Nature ,1998
- Protection in programming-language translationsPublished by Springer Nature ,1998
- Authentication and authenticated key exchangesDesigns, Codes and Cryptography, 1992
- A Digital Signature Scheme Secure Against Adaptive Chosen-Message AttacksSIAM Journal on Computing, 1988
- Probabilistic encryptionJournal of Computer and System Sciences, 1984
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983
- New directions in cryptographyIEEE Transactions on Information Theory, 1976