Deciding Secrecy of Security Protocols with Well Structured Transition Systems

Security protocols are distributed programs that are designed to achieve secure communications using cryptography. They are extensively deployed today but their design is notoriously error-prone. In contrast to other safety critical systems, a distinctive feature of the security properties of protocols is that they must hold in the presence of an adversary or intruder, and this makes them challenging to verify. An important example of such a security property is secrecy : to verify that a protocol satisfies secrecy amounts to checking whether it can leak a given (secret) message to the environment as a result of interference by the intruder. In essence, to verify secrecy, we need a way of analysing the set of messages that the intruder knows; if a message does not belong to this set, then that message is not leaked. Here we assume a model of intruders as defined by Dolev and Yao [4]. The difficulty is that this set of messages is in general infinite, because the Dolev-Yao intruder is in control of three sources of infinity: a) messages of unbounded size, b) an unbounded set of nonces (and other freshly generated data such as session keys), and c) an unbounded number of sessions. Indeed the secrecy problem was proved to be undecidable by Durgin et al. [7]. Amadio et al. [2] and Heintze and Tygar [11] showed that the problem is undecidable even if the set of atomic terms is fixed and finite, assuming that terms of arbitrary size can be substituted for nonces. In [6], we show that the problem of secrecy is decidable for a class of security protocols with an unbounded number of sessions and unlimited fresh data. Roughly speaking, we show that the inability of the protocol to generate what we call encryption chains of unbounded length is a sufficient condition to guarantee decidability of secrecy. An encryption chain of length n is a set of messages of the form {N1}N2 , {N2}N3 , . . . , {Nn−1}Nn , for secret nonces N1, . . . , Nn. Besides the obvious applications, this result’s relevance is chiefly conceptual: we show, for the first time, that limiting the length of the encryption chains is enough, together with the necessary message size limitation common to other approaches, to obtain decidability of secrecy. As importantly, we show how to technically implement the restriction so that only the relevant encryption chains are considered. In this abstract we will outline the main techniques used to prove this result.