Towards a completeness result for model checking of security protocols
- 27 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Model checking approaches to the analysis of security protocols have proved remarkably successful. The basic approach is to produce a model of a small system running the protocol, together with a model of the most general intruder who can interact with the protocol, and then to use a state exploration tool to search for attacks. This has led to a number of new attacks upon protocols being discovered. However if no attack is found, this only tells one that there is no attack upon the small system modelled; there may be an attack upon some larger system. This is the question considered in the paper: the author presents sufficient conditions on the protocol and its environment such that if there is no attack upon a particular small system (with one honest agent for each role of the protocol) leading to a breach of secrecy (using a fairly strong definition of secrecy), then there is no attack on any larger system leading to a breach of secrecy (using a more general definition of secrecy).Keywords
This publication has 13 references indexed in Scilit:
- Honest ideals on strand spacesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Towards a completeness result for model checking of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Casper: a compiler for the analysis of security protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A hierarchy of authentication specificationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Using CSP to detect errors in the TMN protocolIEEE Transactions on Software Engineering, 1997
- The NRL Protocol Analyzer: An OverviewThe Journal of Logic Programming, 1996
- An attack on the Needham-Schroeder public-key authentication protocolInformation Processing Letters, 1995
- Three systems for cryptographic protocol analysisJournal of Cryptology, 1994
- Prudent engineering practice for cryptographic protocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1994
- A logic of authenticationPublished by Association for Computing Machinery (ACM) ,1989