Carleton University
Technical Report TR-243
May 1994
On Unifying Some Cryptographic Protocol Logics
Paul F. Syverson & Paul C. van Oorschot
Abstract
We present a logic for analyzing cryptographic protocols. This logic encompasses a unification of four of its predecessors in the BAN family of logics, namely those given in (GNY90], (AT91], (vO93], and BAN itself (BAN89]. We also present a model-theoretic semantics with respect to which the logic is sound. The logic herein captures all of the desirable features of its predecessors and more; nonetheless, it accomplishes this with no more axioms or rules than the simplest of its predecessors.