An Executable Specification Language for Planning Attacks to Security Protocols

We propose ALSP a Declarative Executable Specification Language for Planning Attacks to Security Protocols based on logic programming. In ALSP we can give a declarative specification of a protocol with the natural semantics of send and receive actions. We view a protocol trace as a plan to reach a goal, so that attacks are just plans reaching goals that correspond to security violations, which can be also declaratively specified. Building on results front 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. ALSP specifications are executable, as we can automatically search for attacks via any efficient model generator (such as smodels), that implements the stable model semantics of normal logic programs. Thus, we come to a specification language which is easy to use - protocol specifications are expressed at a high level of abstraction, and with an intu...