Model checking of security protocols with pre-configuration

Abstract

Security protocols are very vulnerable to design errors. Thus many techniques have been proposed for validating the correctness of security protocols. Among these, general model checking is one of the preferred methods. Using tools such as Murψ, model checking can be performed automatically. Thus protocol designers can use it even if they are not proficient in formal techniques. Although this is an attractive approach, state space explosion prohibits model checkers from validating secure protocols with a significant number of communicating participants. In this paper, we propose "model checking with pre-configuration" which is a "divide-and-conquer" approach that reduces the amount of memory needed for verification. The verification time is also reduced since the method permits the use of symmetry more effectively in model checking. The performance of the method is shown by checking the NeedhamSchroeder-Lowe Public-Key protocol using Murψ. © Springer-Verlag 2004.