Generic and efficient attacker models in SPIN

Abstract

In telecommunication networks, it is common that security protocol procedures rely on context information and other parameters of the global system state. Current security ver- ification tools are well suited for analyzing protocols in iso- lation and it is not clear how they can be used for protocols intended to be run in more“dynamic”settings. Think of pro- tocol procedures sharing parameters, arbitrarily interleaved or used as building blocks in more complex compound proce- dures. SPIN is a well established general purpose verification tool that has good support for modeling such systems. In contrast to specialized tools, SPIN lacks support for crypto- graphic primitives and intruder model which are necessary for checking security properties. We consider a special class of security protocols that fit well in the SPIN framework. Our modeling method is systematic, generic and efficient enough so that SPIN could find all the expected attacks on several of the classical key distribution protocols.