Adding Time to a Logic of Authentication
Abstract
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]. 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1993
- Accession Number
- ADA462620
Entities
People
- Paul Syverson
Organizations
- United States Naval Research Laboratory