Catherine Meadows, ``A Model of Computation for the NRL Protocol Analyzer,''
Proceedings of 1994 Computer Security Foundations Workshop, IEEE
Computer Society, June, 1994.
<a href="1994meadows-foundations.ps">
 PostScript</a>

<blockquote>
In this paper we develop a model of computation for the NRL Protocol Analyzer
by modifying and extending the model of computation for
Burroughs, Abadi, and Needham (BAN) logic developed by Abadi and Tuttle.
We use the results to point out the similarities and differences between
the NRL Protocol Analyzer and BAN logic, and discuss the issues this raises
with respect to the possible integration of the two.
</blockquote>