An executable specification language for planning attacks to security protocols

We propose AL(SP) a Declarative Executable Specification Language for Planning Attacks to Security Protocols based on logic programming. III AL(SP) we carl give a declarative specification of a protocol with the natural semantics of send and recieve actions. We view a protocol trace as a plan to reach a goal, so that attacks are just plans caching goals that correspond to security violations, which carl be also declaratively specified. 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. AL(SP) 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 rise - protocol specifications are expressed at a high level of abstraction, and with an intuitive notation close to their traditional description - still keeping the rigor of a formal specification that, in addition, is executable.