Model checking is a very successful technique which has been applied in the design and verification of finite state concurrent reactive processes. This technique can be lifted to be applicable to multiagent systems. Our approach allows us to reuse the technology and tools developed in model checking, to design and verify multiagent systems in a modular and incremental way, and also to have a very efficient model checking algorithm. The paper investigates the applicability of our multiagent model checking framework to the analysis of a relevant class of multiagent protocols, namely security protocols.