Casper: a compiler for the analysis of security protocols
Top Cited Papers
- 22 November 2002
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 1146, 18-30
- https://doi.org/10.1109/csfw.1997.596779
Abstract
In recent years, a method for analyzing security protocols usingthe process algebra CSP (Hoare, 1985) and its model checker FDR(Roscoe, 1994) has been developed. This technique has provedremarkably successful, and has been used to discover a number ofattacks upon protocols. However, the technique has requiredproducing a CSP description of the protocol by hand; thishas proved tedious and error-prone. In this paper we describeCasper, a program that automatically produces the CSP descriptionfrom a more abstract description, thus greatly simplifying themodelling and analysis process.Keywords
This publication has 19 references indexed in Scilit:
- Design and implementation of an authentication system in WIDE Internet environmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Modelling and verifying key-exchange protocols using CSP and FDRPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Analyzing the Needham-Schroeder public key protocol: A comparison of two approachesLecture Notes in Computer Science, 1996
- An attack on the Needham-Schroeder public-key authentication protocolInformation Processing Letters, 1995
- A lesson on authentication protocol designACM SIGOPS Operating Systems Review, 1994
- A nonce-based protocol for multiple authenticationsACM SIGOPS Operating Systems Review, 1992
- Key Distribution Protocol for Digital Mobile Communication SystemsLecture Notes in Computer Science, 1990
- Reducing risks from poorly chosen keysPublished by Association for Computing Machinery (ACM) ,1989
- A logic of authenticationPublished by Association for Computing Machinery (ACM) ,1989
- Timestamps in key distribution protocolsCommunications of the ACM, 1981