Parallel bounded model checking of security protocols

Abstract

The verification of security protocols is a difficult process taking into consideration a concept and computations. The difficulties start just during the appropriate adequate protocol specification, and during studying its properties. In case of the computation connected with constructing and searching of the modeling structures of protocol execution and scattered knowledge of the users, the problems are the sizes of those structures. For small values of parameters such as numbers of sessions, users, or encryption keys the proper models are usually not very big, and searching them is not a problem, however in case of increasing the values of the above mentioned parameters, the models are sometimes too big, and there is no possibility to construct them nor search properly. In order to increase the values of studying protocol parameters, and necessary increase the computation effectiveness, the appropriate solutions must be introduced. In the article, the solutions which enable full and effective parallelization of the computations during automatic verification of security protocols are introduced. The suitable experimental results are also presented. © 2014 Springer-Verlag.