A Formal Analysis of Complex Type Flaw Attacks on Security Protocols.

A simple type confusion attack occurs in a security protocol, when a principal interprets data of one type as data of another. These attacks can be successfully prevented by tagging types of each field of a message. Complex type confusions occur instead when tags can be confused with data and when fields or sub-segments of fields may be confused with concatenations of fields of other types. Capturing these kinds of confusions is not easy in a process calculus setting, where it is generally assumed that messages are correctly interpreted. In this paper, we model in the process calculus LySa only the misinterpretation due to the confusion of a concatenation of fields with a single field, by extending the notation of one-to-one variable binding to multi-to-one binding. We further present a formal way of detecting these possible misinterpretations, based on a Control Flow Analysis for this version of the calculus. The analysis over-approximates all the possible behaviour of a protocol, including those effected by these type confusions. As an example, we considered the amended Needham-Schroeder symmetric protocol, where we succeed in detecting the type confusion that lead to a complex type flaw attacks it is subject to. Therefore, the analysis can capture potential type confusions of this kind on security protocols, besides other security properties such as confidentiality, freshness and message authentication.