Secrecy by typing in security protocols
- 1 September 1999
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 46 (5) , 749-786
- https://doi.org/10.1145/324133.324266
Abstract
We develop principles and rules for achieving secrecy properties in security protocols. Our approach is based on traditional classification techniques, and extends those techniques to handle concurrent processes that use shared-key cryptography. The rules have the form of typing rules for a basic concurrent language with cryptographic primitives, the spi calculus. They guarantee that, if a protocol typechecks, then it does not leak its secret inputs.Keywords
This publication has 24 references indexed in Scilit:
- A calculus of mobile processes, IPublished by Elsevier ,2004
- Mobile ambientsPublished by Springer Nature ,1998
- Protection in programming-language translationsPublished by Springer Nature ,1998
- Trust in the λ-calculusJournal of Functional Programming, 1997
- The Compositional Security Checker: a tool for the verification of information flow security propertiesIEEE Transactions on Software Engineering, 1997
- Prudent engineering practice for cryptographic protocolsIEEE Transactions on Software Engineering, 1996
- A lesson on authentication protocol designACM SIGOPS Operating Systems Review, 1994
- A logic of authenticationProceedings of the Royal Society of London. Series A. Mathematical and Physical Sciences, 1989
- Testing equivalences for processesTheoretical Computer Science, 1984
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978