Executable specification language for planning attacks to security protocols

Luigia Carlucci Aiello, Fabio Massacci

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

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 intuitive notation close to their traditional description - still keeping the rigor of a formal specification that, in addition, is executable.
Original languageEnglish
Title of host publicationProceedings of the Computer Security Foundations Workshop
PublisherIEEE
Pages88-102
Publication statusPublished - 2000
Externally publishedYes
Event13th IEEE Computer Security Foundations Workshop CSFW-13 -
Duration: 3 Jul 20005 Jul 2000

Publication series

NameProceedings of the Computer Security Foundations Workshop

Conference

Conference13th IEEE Computer Security Foundations Workshop CSFW-13
Period3/07/005/07/00

Fingerprint

Dive into the research topics of 'Executable specification language for planning attacks to security protocols'. Together they form a unique fingerprint.

Cite this