Catherine Meadows, ``The NRL Protocol Analyzer: An Overview,'' Proceedings
of the 2nd Conference on the Practical Applications of Prolog, Association
for Logic Programming, April, 1994.
<a href="1994meadows-pap.ps">
 PostScript</a>

<blockquote>
The NRL Protocol Analyzer is a special-purpose verification tool,
written in Prolog,
that has been developed for the analysis of cryptographic protocols
that are used to authenticate principals and services and distribute
keys in a network.   In this paper we give an overview of how the Analyzer
works and describe its achievements so far.
We also show how our use of the Prolog language benefited us
in the design and implementation of the Analyzer.
</blockquote>