A long-standing research problem is how to efficiently verify security protocols with tamper-resistant global states, especially when the global states evolve unboundedly. We propose a protocol specification framework, which facilitates explicit modeling of states and state transformations. On the basis of that, we develop an algorithm for verifying security properties of protocols with unbounded state-evolving, by tracking state transformation and checking the validity of the state-evolving traces. We prove the correctness of the verification algorithm, implement both of the specification framework and the algorithm, and evaluate our implementation using a number of stateful security protocols. The experimental results show that our approach is both feasible and practically efficient. Particularly, we have found a security flaw on the digital envelope protocol, which cannot be detected with existing security protocol verifiers.
CITATION STYLE
Li, L., Dong, N., Pang, J., Sun, J., Bai, G., Liu, Y., & Dong, J. S. (2017). A Verification Framework for Stateful Security Protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10610 LNCS, pp. 262–280). Springer Verlag. https://doi.org/10.1007/978-3-319-68690-5_16
Mendeley helps you to discover research relevant for your work.