Using transition systems to model and verify the implementation of security protocol

The transition system is widely used to model and to analyze the properties of protocol implementations. It presents the systems with reachable finite state graphes and can be used to calculate the possible transitions traces to verify the correctness of the protocol implementation. But this method is hard to be used to verify the security of authentication protocol, because some important security properties (such as nonce, encryption etc.) are not compatible in the classic definition of system transition. In addition, the security protocols usually need to consider the actions of possible attackers, which is also an obstacle to use transition system on security protocol. In this article, for the purpose of security protocol verification, we extend the classic IOLTS model to SG-IOLTS model, which defines variables and atoms into transitions to capture the security properties and combines the distribute concurrent components together. We also propose an finite intruder model within this SG-IOLTS, which makes the reachable graph contains the transitions of intruders and makes the security verifying traces can be generated through the transition system.