A Unified Cryptographic Protocol Logic
Paul F. Syverson, Paul C. van Oorschot · 1996
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 NeedhamSchroeder 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.