A Sound Abstraction from the Parsing Problem in Security Protocols | Georgios Katsoris
| | 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 specifi c 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. | | Type | Master's thesis [Academic thesis] | | Year | 2013 | | Publisher | Technical University of Denmark, Department of Applied Mathematics and Computer Science | | Address | Matematiktorvet, Building 303B, DK-2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk | | Series | M.Sc.-2013-112 | | Note | | | Electronic version(s) | [pdf] | | Publication link | http://www.compute.dtu.dk/English.aspx | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|