Analyzing security protocols with secrecy types and logic programs
- 1 January 2005
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 52 (1) , 102-146
- https://doi.org/10.1145/1044731.1044735
Abstract
We study and further develop two language-based techniques for analyzing security protocols. One is based on a typed process calculus; the other, on untyped logic programs. Both focus on secrecy properties. We contribute to these two techniques, in particular by extending the former with a flexible, generic treatment of many cryptographic operations. We also establish an equivalence between the two techniques.Keywords
This publication has 16 references indexed in Scilit:
- Automatic proof of strong secrecy for security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- Secrecy types for asymmetric communicationTheoretical Computer Science, 2003
- Efficient, DoS-resistant, secure key exchange for internet protocolsPublished by Association for Computing Machinery (ACM) ,2002
- Certified email with a light on-line trusted third partyPublished by Association for Computing Machinery (ACM) ,2002
- Secrecy by typing in security protocolsJournal of the ACM, 1999
- A Calculus for Cryptographic Protocols: The Spi CalculusInformation and Computation, 1999
- The Compositional Security Checker: a tool for the verification of information flow security propertiesIEEE Transactions on Software Engineering, 1997
- Three systems for cryptographic protocol analysisJournal of Cryptology, 1994
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978
- Protection in programming languagesCommunications of the ACM, 1973