Skip to main content
Article
Automatic Compilation of Protocol Insecurity Problems into Logic Programming
Computer Science Faculty Proceedings & Presentations
  • Alessandro Armondo, Universita di Genova
  • Luca Compagna, Universita di Genova
  • Yuliya Lierler, University of Nebraska at Omaha
Document Type
Conference Proceeding
Publication Date
1-1-2004
Disciplines
Abstract

In this paper we show how protocol insecurity problems expressed in a multi-set rewriting formalism can be automatically translated into logic programming problems. The proposed translation paves the way to the construction of model-checkers for security protocols based on state-of-the-art solvers for logic programs. We have assessed the effectiveness of the approach by running the proposed reduction against a selection of insecurity problems drawn from the Clark & Jacob library of security protocols: by running state-of-the-art solvers against the resulting logic programming problems most of the (known) attacks on the considered protocols are found in a few seconds.

Comments

9th European Conference on Logics in Artificial Intelligence (JELIA)

Citation Information
Alessandro Armondo, Luca Compagna and Yuliya Lierler. "Automatic Compilation of Protocol Insecurity Problems into Logic Programming" (2004)
Available at: http://works.bepress.com/yuliya_lierler/3/