A Logic of Belief and a Model Checking Algorithm for Security Protocols

Model checking is a very successful technique which has been applied in the design and verification of finite state concurrent reactive processes. In this paper we show how this technique can be used for the verification of security protocols using a logic of belief. The underlying idea is to treat separately the temporal evolution and the belief aspects of principals. In practice, things work as follows: when we consider the temporal evolution of a principal we treat belief atoms (namely, atomic formulae expressing belief) as atomic propositions. When we deal with the beliefs of a principal A, we model its beliefs about another principal B as the fact that A has access to a representation of B as a process. Then, any time it needs to verify the truth value of some belief atom about B, e.g. $B_B{\phi}$, A simply tests whether, e.g. $\phi$ holds in its (appropriate) representation of B. Beliefs are essentially used to control the `jumping` among processes. Our approach allows us to reuse the technology and tools developed in model checkin