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 eld of a message. Complex type confusions occur instead when tags can be confused with data and when elds or sub-segments of elds may be confused with concatenations of elds 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 elds with a single eld, by extending the notation of one-to-one variable binding to many-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, inc...

• Type: Conference
• Year: 2008
• Where: AMAST
• Authors: Han Gao, Chiara Bodei, Pierpaolo Degano
• Keywords: AMAST 2008, Complex Type Confusions, Software Engineering, Type Confusion Attack, Type Confusions