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.

PS

In Proceedings of 9th {E}uropean Conference in Logics in Artificial Intelligence (JELIA-04), pp. 617-627 2004. Springer.

@InProceedings{arm04a, title={Automatic Compilation of Protocol Insecurity Problems into Logic Programming}, author={Alesandro Armando and Luca Compagna and Yuliya Lierler}, booktitle={Proceedings of 9th {E}uropean Conference in Logics in Artificial Intelligence (JELIA-04)}, series={Lecture Notes In Artificial Intelligence}, publisher={Springer}, pages={617-627}, url="http://www.cs.utexas.edu/users/ai-lab?arm04a", year={2004} }