@MASTERSTHESIS\{IMM2013-06693,
    author       = "G. Katsoris",
    title        = "A Sound Abstraction from the Parsing Problem in Security Protocols",
    year         = "2013",
    school       = "Technical University of Denmark, Department of Applied Mathematics and Computer Science",
    address      = "Matematiktorvet, Building 303B, {DK-}2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk",
    type         = "",
    note         = "{DTU} supervisor: Sebastian Alexander M{\"{o}}dersheim, samo@dtu.dk, {DTU} Compute",
    url          = "http://www.compute.dtu.dk/English.aspx",
    abstract     = "This work examines the problem of how to represent the structure of messages exchanged in security protocols. Security protocols work by exchanging information using messages. Such types of messages can be {XML} messages, or messages with different lengths and content. Protocol model checking abstracts from the specific details of messages, thereby excluding some potential security flaws that are based on confusing messages of similar form. Thus, a potential security aw is left unnoticed.
To investigate this problem, a language has been defined to precisely specify the details of the examined message structure. Second, a prototype implementation was built to perform message comparisons. The input given to the implementation is the examined message set, written in our language.
The goal is to investigate the disjointness (i.e. non-confusability) of protocol messages, using our implementation's comparison results. Such a result is important when performing parallel and vertical protocol compositions. In order
to claim that such compositions are secure, message and subsequently protocol disjointness is a necessary condition to be met.
We represent two widely used protocols with our language, {TLS} and {IKE,} and discuss the overall results given by our approach and implementation."
}