Verifying security protocols as planning in logic programming

We illustrate ALSP (Action Language for Security Protocol), a declarative executable specification language for planning attacks to security protocols. ALSP is based on logic programming with negation as failure, and with stable model semantics. In ALSP we can give a declarative specification of a protocol with the natural semantics of send and receive actions which can be performed in parallel. By viewing a protocol trace as a plan to achieve a goal, attacks are (possibly parallel) plans achieving goals that correspond to security violations. Building on results from logic programming and planning, we map the existence of an attack into the existence of a model for the protocol that satisfies the specification of an attack. We show that our liberal model of parallel actions can adequately represent the traditional Dolev-Yao trace-based model used in the formal analysis of security protocols. Specifications in ALSP are executable, as we can automatically search for attacks via an efficient model generator (smodels), implementing the stable model semantics of normal logic programs.