A verification framework for stateful security protocols

• Main Authors: LI, Li, DONG, Naipeng, PANG, Jun, SUN, Jun, BAI, Guangdong, LIU, Yang, DONG, Jin Song
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2017
• Subjects: Protocol specifications; Security properties; Security protocols; Information Security
• Online Access: https://ink.library.smu.edu.sg/sis_research/4722; https://ink.library.smu.edu.sg/context/sis_research/article/5725/viewcontent/Verification_Framework_ICFEM_2017_av.pdf
• Institution: Singapore Management University

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.