Towards a completeness result for model checking of security protocols

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.