Towards a completeness result for model checking of security protocols

Article type: Research Article

Authors: Lowe, Gavin

Affiliations: Department of Mathematics and Computer Science, University of Leicester, University Road, Leicester LE1 7RH, UK. E-mail: gavin.lowe@mcs.le.ac.uk

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 us that there is no attack upon the small system we modelled; there may be an attack upon some larger system. This is the question we consider in this paper: we prove that under certain conditions on the protocol and the environment in which it operates, 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, then there is no attack on any larger system leading to a breach of secrecy.

DOI: 10.3233/JCS-1999-72-302

Journal: Journal of Computer Security, vol. 7, no. 2-3, pp. 89-146, 1999