LTL model checking for security protocols

Most model checking techniques for security protocols make a number of simplifying assumptions on the protocol and/or on its execution environment that prevent their appli-cability in some important cases. For instance, most tech-niques assume that communication between honest princi-pals is controlled by a Dolev-Yao intruder, i.e. a malicious agent capable to overhear, divert, and fake messages. Yet we might be interested in establishing the security of a pro-tocol that relies on a less unsecure channel (e.g. a confiden-tial channel provided by some other protocol sitting lower in the protocol stack). In this paper we propose a general model for security protocols based on the set-rewriting for-malism that, coupled with the use of LTL, allows for the specification of assumptions on principals and communica-tion channels as well as complex security properties that are normally not handled by state-of-the-art protocol analysers. By using our approach we have been able to formalise all the assumptions required by the ASW protocol for optimistic fair exchange as well as some of its security properties. Be-sides the previously reported attacks on the protocol, we report a new attack on a patched version of the protocol. 1