Introduction

In their ground-breaking paper [BAN89] Burrows, Abadi and Needham give a formalism, BAN logic, that can be used to reason about security properties of protocols. There are, however, several implicit or informally described assumptions. Moreover, the semantics gets very little attention, and is mentioned only in a short, informal description. As pointed out by Syverson [Syv91], having only an intuitive understanding of the semantics directly opposes the usual goal of having semantics at all: to see the logic as part of a system, and to be able to prove statements about a (more or less) existing model formally. Our aim was, therefore, to construct a sound semantics for BAN, as well as a notion of correctness that makes the additional requirements for both specification and protocol explicit.

Various authors have tried to give a semantics to BAN logic; some of them left the logic more or less intact, while others developed semantics for a new logic based on BAN logic. All these approaches are, just like BAN logic itself, restricted in their description of reality -- the world can only be described through the (belief) eyes of the participants. However, to be able to judge cryptographic protocols, one cannot avoid looking beyond the individual beliefs of participants. Since all individual beliefs may be wrong, the outside world must be looked at separately. Therefore, we have not only looked for a precise semantics for BAN logic (and a proof of its soundness), but we have also chosen the semantics in such a way that it enables us to reason about knowledge (and, as a result, about the rightness of the participants' beliefs).

For our investigation we use an extension of BAN logic. Its language has, apart from the constructs taken from BAN, a few additional constructs, such as $P \possesses K$, used to express possession of a key -- and the resulting ability to decrypt messages with that key -- without necessarily believing that it belongs to a certain pair of principals; and $P \rightlybelieves \phi$, which expresses that not only $P \believes \phi$, but also $\phi$ itself holds.

We present the axioms of the logic in a general form: one can derive statements about the beliefs of principals, but also about the rightness of those beliefs (or of statements in general, independent of any beliefs). Defining a rectify operation that maps formulas of the form $P \believes \phi$ to $P \rightlybelieves \phi$, leaving other formulas intact, leads to a theorem that expresses that principals draw the right conclusions from their beliefs. In other words: if their initial beliefs are right, their conclusions will be right as well.

However, logical soundness does not yet establish that principals draw correct conclusions during a protocol run. We define, using operational semantics, what it means for a protocol to meet its specification. In order to prove that property of a protocol, we need certain restrictions on the protocol, depending on the assumptions. Besides, as it turns out, the assumptions need to be of a certain form as well, in order to secure monotonicity. Those requirements can be checked statically and do not exclude well-known examples of protocols.