Automatic Compilation of Protocol Insecurity Problems into Logic Programming (2004)
Alesandro Armando, Luca Compagna, and Yuliya Lierler
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.
In Proceedings of 9th {E}uropean Conference in Logics in Artificial Intelligence (JELIA-04), pp. 617-627 2004. Springer.

Yuliya Lierler Ph.D. Alumni ylierler [at] unomaha edu