Paul Syverson,
``The Use of Logic in the Analysis of Cryptographic Protocols,''
Proceedings of the 1991 IEEE Symposium on Research in Security and
Privacy, Oakland CA May 1991 IEEE CS Press (Los Alamitos CA, 1991)

<blockquote>
Logics for cryptographic protocol analysis are discussed and a study
is made of the protocol features that they are appropirate for analyzing:
some are appropriate for analyzing trust, others security. The goals
of Burrows, Abadi, and Needham's BAN logic are examined, and it is found that
there is confusion about these. Formal semantics is explored as a
reasoning tool and the importance of soundness and completeness for
protocol security is discussed. The logic KPL is used
to resolve a debate over an alleged flaw in BAN logic.
</blockquote>