Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

11-2017

Abstract

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.

Keywords

Protocol specifications, Security properties, Security protocols

Discipline

Information Security

Research Areas

Cybersecurity

Publication

Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17: Proceedings

Volume

10610

First Page

262

Last Page

280

ISBN

9783319686899

Identifier

10.1007/978-3-319-68690-5_16

Publisher

Springer

City or Country

Cham

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1007/978-3-319-68690-5_16

Download

Share

COinS