Planning attacks to security protocols: Case studies in logic programming

Formal verification of security protocols has become a key issue in computer security. Yet, it has proven to be a hard task often error prone and discouraging for non-experts in formal methods. In this paper we show how security protocols can be specified and verified efficiently and effectively by embedding reasoning about actions into a logic programming language. In a nutshell, we view a protocol trace as a plan to achieve a goal, so that protocol attacks are plans achieving goals that correspond to security violations. Building on results from logic programming and planning, we map the existence of an attack to a protocol into the existence of a model for the protocol specification that satisfies the specification of an attack. To streamline such way of modeling security protocols, we use a description language AL(SP) which makes it possible to describe protocols with declarative ease and to search for attacks by relying on efficient model finders (e.g. the smodels systems by Niemela and his group). This paper shows how to use AL(SP) for modeling two significant case studies in protocol verification: the classical Needham-Schroeder public-key protocol, and Aziz-Diffie Key agreement protocol for mobile communication.