A Unified Cryptographic Protocol Logic
NAVAL RESEARCH LAB WASHINGTON DC
Pagination or Media Count:
We present a logic for analyzing cryptographic protocols. This logic is based on a unification of four of its predecessors in the BAN family of logics, namely those given in GNY90, AT91, vO93b, and BAN itself BAN89. The logic herein captures the desirable features of its predecessors and more nonetheless, as a logic it is relatively simple and simple to use. We also present a model-theoretic semantics, and we prove soundness for the logic with respect to that semantics. We illustrate the logic by applying it to the Needham- Schroeder protocol, revealing that BAN analysis of it may lead to inappropriate conclusions in some settings. We also use the logic to analyze two key agreement protocols, examining an attack on one of them.