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.