Abstract
Questions of belief are essential in analyzing protocols for the authentication of
principals in distributed computing systems. In this paper we motivate, set out, and
exemplify a logic specifically designed for this analysis; we show how various protocols
differ subtly with respect to the required initial assumptions of the participants and
thier final beliefs. Our formalism has enabled us to isolate and express these differences
with a precision that was not previously possible. It has drawn attention to features of
protocols of which we and thier authors were previously unaware, and allowed us to suggest
improvements to the protocols. The reasoning about some protocols has been mechanically
verified.
This paper starts with an informal account of the problem, goes on to explain the formalism
to be used, and gives examples of its application to protocols from the literature, both with
shared-key cryptography and with public-key cryptography. Some of the examples are chosen
because of their practical importance, while others serve to illustrate subtle points of the
logic and to explain how we use it. We discuss extensions of the logic motivated by actual
practice - for example, in order to account for the use of hash functions in signatures
The final sections contain a formal semantics of the logic and some conclusions.
