  A long-standing research problem in security protocol design is how to
efficiently verify security protocols with tamper-resistant global states. In
this paper, we address this problem by first proposing a protocol specification
framework, which explicitly represents protocol execution states and state
transformations. Secondly, we develop an algorithm for verifying security
properties by utilizing the key ingredients of the first-order reasoning for
reachability analysis, while tracking state transformation and checking the
validity of newly generated states. Our verification algorithm is proven to be
(partially) correct, if it terminates. We have implemented the proposed
framework and verification algorithms in a tool named SSPA, and evaluate it
using a number of stateful security protocols. The experimental results show
that our approach is not only feasible but also practically efficient. In
particular, we have found a security flaw on the digital envelope protocol,
which could not be detected by existing security protocol verifiers.
