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 , 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 , which expresses that not only , but also 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 to , 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.