Approach to Detecting Type-Flaw Attacks Based on Extended Strand Spaces
Song Wei-dong, B. Hu · The Computer Journal · 2014
Many security protocols are vulnerable to type-flaw attacks (TFAs), in which a message variable of one type is essentially substituted with a message of another type by adversary, causing a violation of a security property. The previous approaches mostly focus on how to prevent TFAs on security protocols, which avoid the question: whether an existing protocol (without any change) is vulnerable to TFAs or not. Formal methods provide well-defined languages that allow precise specifications to be written and subsequent rigorous verification procedures to be performed. Analyses of protocols susceptible to TFAs have been attempted using various formalisms. But most of them belong to heuristic methods. The research on type theory is still not mature. In this paper, we introduce a multi-branch tag tree, build a strong intruder model and make a classification to extend the strand space model (SSM). This overcomes the limitation of SSM for detecting TFAs on security protocols. Then, based on the extended strand spaces, we establish a three-level model to detect TFAs on security protocols. Our three-level model can verify whether a protocol is susceptible to TFAs and how many TFAs can be launched by the penetrator in the protocol.