Stateful Security Protocol Verification
This addresses a long-standing problem in security protocol design for researchers and practitioners, offering a practical verification method.
The paper tackles the problem of efficiently verifying security protocols with tamper-resistant global states by proposing a specification framework and verification algorithm, implemented in tool SSPA, which found a security flaw in the digital envelope protocol that existing verifiers missed.
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.