Paul Sverson, ``Adding Time to a Logic of Authentication,''
Proceedings of the First ACM Conference on Computer and
Communications Security, Fairfax VA  Nov. 1993
ACM Press (New York, 1993)
<a href="1993syverson-ccs.ps">
 PostScript</a>


<blockquote>
In [BAN89] Burrows, Abadi, and Needham presented a
logic (BAN) for analyzing cryptographic protocols in terms of belief.
This logic is quite useful in uncovering flaws in protocols; however, it
also has produced confusion and controversy. Much of the
confusion was cleared up when Abadi and Tuttle provided a semantics
for a version of that logic (AT) in [AT91].<P>

In this paper we present a protocol to show that both BAN and AT are
not expressive enough to capture all of the kinds of flaws that appear to
be within their scope. We then present a logic that adds temporal
formalisms to AT and that is rich enough to reveal the flaws in the
presented protocol; nonetheless, this logic is sound with respect
to the same semantics that was given in [AT91]. Finally, we argue
that any approach of this type is inadequate by itself to demonstrate
the absence of such flaws. We must
supplement the formal logic with semantic analysis techniques.
</blockquote>