A procedure for verifying security against type confusion attacks

Abstract
A type confusion attack is one in which a principal ac- cepts data of one type as data of another. Although it has been shown by Heather et al. that there are simple for- matting conventions that will guarantee that protocols are free from simple type confusions in which fields of one type are substituted for fields of another, it is not clear how well they defend against more complex attacks, or against at- tacks arising from interaction with protocols that are for- matted according to different conventions. In this paper we show how type confusion attacks can arise in realistic situations even when the types are explic- itly defined in at least some of the messages, using examples from our recent analysis of the Group Domain of Interpreta- tion Protocol. We then develop a formal model of types that can capture potential ambiguity of type notation, and out- line a procedure for determining whether or not the types of two messages can be confused. This work extends our ear- lier work on the subject in that it includes an explicit model of attacker and defender and extends the informal model of the type confusion attack in terms of a game between an in- truder and a set of honest principals in or earlier work to a more formal model in which actions of intruder and honest principals are described explicitly. This gives us a simpler, more intuitive approach that allows us to calculate proba- bilities in a more systematic manner, and to compare differ- ent intruder strategies and different assumptions about the way in which the protocol is implemented in terms of their effects on type confusion.

This publication has 7 references indexed in Scilit: