A finite transition model for security protocol verification

The reachable graphs and FSM methods are successfully used to analyze the network protocols and to generate computable test traces to verify the correctness of protocol communication. But these methods are hard to use to verify the security of the protocol, because the important security properties (such as nonce, encrypt methods etc.) are not compatible in the classic FSM definition. In this article, for our 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. 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 automatically.