Proving

security protocols with model checkers by data independence techniques

Proving security protocols with model checkers by data independence techniques A.W. Roscoe Oxford University Computing Laboratory Wolfson Building, Parks Road, Oxford OX1 3QD, UK

Abstract Model checkers such as FDR have been extremely e ective in checking for, and nding, attacks on cryptographic protocols{ see, for example 11, 12, 14] and many of the papers in 3]. Their use in proving protocols has, on the other hand, generally been limited to showing that a given small instance, usually restricted by the niteness of some set of resources such as keys and nonces, is free of attacks. While for speci c protocols there are frequently good reasons for supposing that this will nd any attack, it leaves a substantial gap in the method. The purpose of this paper is to show how techniques borrowed from data independence and related elds can be used to achieve the illusion that nodes can call upon an in nite supply of di erent nonces, keys, etc., even though the actual types used for these things remain nite. It is thus possible to create models of protocols in which nodes do not have to stop after a small number of runs and to claim that, within certain limits, a nite-state run on a model checker has proved that a given protocol is secure from attack. We use a single protocol as a case study, but believe our techniques are much more widely applicable.

1 Introduction Cryptographic protocols frequently depend on the uniqueness, and often on the unguessability, of some of the data objects they use such as keys and nonces. If we are programming an agent running such a protocol, either for practical use or as part of a program for feeding into a model checker, then each time it creates a new nonce (say) it relies on the fact that it (and usually everyone else) has not used this particular value before. Frequently, of course, there will be no mechanism in Email: Bill.Roscoe@comlab.ox.ac.uk Copyright 1998 IEEE. Published in Proceedings, 1998 IEEE Computer Security Foundations Workshop, Rockport Massachusetts, June, 1998.

place to guarantee this uniqueness, rather the contrary being discounted because of its extreme improbability. On the other hand, the way model checkers work mean that one cannot rely on probability in this way, so if using one you have to include some mechanism for enforcing no repeats. The pragmatics of running model checkers mean, unfortunately, that the sizes of types such as nonces have to be restricted to far smaller sizes than the types they represent in implementations. Usually they have to be kept down to single gures if the combinatorics of how they can create messages of the protocol is not to take other types that have to be considered, such as the overall alphabet size and the set of facts that a potential intruder might learn, beyond the level that can be managed. The models that the author and others created therefore allocated a small nite number of these values to each node that has to\invent" them during a run, so that eac

h time a nonce (say) was required a node took one of those remaining from its initial allocation or, if there were none left, simply stopped. This use of agents with the capacity for only a nite number of runs led to several di culties. First and foremost, it has meant that while model checkers are rightly regarded as extremely e ective tools for nding attacks on protocols, they could only be used to prove that no attack exists on the assumption that each node only engages in a very nite amount of activity. While there are often good intuitive reasons for believing that the limited check would nd any attack, these are generally di cult to formalise into a component of a complete proof. Therefore it has been necessary to look to other varieties of tool, such as theorem provers (see, for example, Paulson's work 16]), for proofs once one's model checker has failed to nd an attack. Secondly, it means that questions of no loss of service (in the presence, for example, of an attacker who makes a nite but unbounded number of interventions) are di cult to address, even though the formalisms (such

第1页下一页