Model checking security protocols using a logic of belief

In this paper we show how model checking can be used for the verification of security protocols using a logic of belief. We model principals as processes able to have beliefs. The idea underlying the approach is to treat separately the temporal evolution and the belief aspects of principals. Therefore, when we consider the temporal evolution, belief formulae are treated as atomic propositions; while the fact that principal A has beliefs about another principal B is modeled as the fact that A has access to a representation of B as a process. As a motivating example, we use the framework proposed to formalize the Andrew protocol. © Springer-Verlag Berlin Heidelberg 2000.