Modeling and analysis of agent-based specifications of security protocols using CSANs and PDETool

Coloured stochastic activity networks (CSANs) are a useful formalism for modeling and analysis of computer systems and networks. PDETool is a new powerful modeling tool that supports CSANs. This paper is an attempt to propose a new approach for modeling and automatic verification of security protocols using CSANs and PDETool. In the proposed approach, the existing agents in the protocol are expressed formally as roles using the security protocols language (SPL) and then are modeled by CSANs. The approach has three steps. Firstly, the security protocol will be modeled regardless of the existence of any intruder. Secondly, different potential intruders will be modeled. Finally, by state space analysis of the model, the possibility of any security flaw in the protocol will be checked. As a case study, the Needham-Schroder and TMN protocols have been modeled and verified.