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.

An executable specification language for planning attacks to security protocols / Carlucci, Luigia; F., Massacci. - (2000), pp. 88-102. (Intervento presentato al convegno 13th IEEE Computer Security Foundations Workshop tenutosi a CAMBRIDGE, ENGLAND nel JUL 03-05, 2000) [10.1109/csfw.2000.856928].

An executable specification language for planning attacks to security protocols

CARLUCCI, Luigia;
2000

Abstract

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.
2000
9780769506715
9780769506722
File allegati a questo prodotto
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/251518
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 4
social impact