Stateful Security Protocol Verification

TL;DR

This paper introduces a novel framework and algorithm for verifying security protocols with explicit state representations, demonstrating practical efficiency and uncovering previously undetectable security flaws.

Contribution

It proposes a new specification framework and verification algorithm for stateful security protocols, with a practical tool implementation and empirical validation.

Findings

Successfully verified stateful protocols with the tool SSPA

Detected a security flaw in the digital envelope protocol

Demonstrated the approach's practical efficiency

Abstract

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.