An Automatic Protocol Composition Checker | Ivana Kojovic
| | Abstract | Formal analysis is widely used to prove security properties of protocols. There are tools to check protocols in isolation, but in fact we use many protocols in parallel or even vertically stacked, e.g. running an application protocol (like login) over a secure channel (like TLS) and in general it is unclear if that is safe. There are several works that give sufficient conditions for parallel and vertical composition, but there exists no program to check whether these conditions are actually met by a given suite of protocols.
The aim of the master thesis project is to implement a protocol composition checker and present it as a service for registering protocols and checking compatibility of the protocols among each other. In order to establish the checker, it is necessary to collect and integrate different conditions defined throughout the literature. Also, we will define a framework based on Alice and Bob notation, so the checker can examine protocols in an unambiguous manner.
Further we will develop a library of widely-used protocols like TLS that are provenly compatible with each other and define a set of negative example protocols to test the checker.
We implement the checker as an extension of the existing Open-Source Fixed-Point Model-Checker OFMC to easily integrate our composition checker with an existing verification procedure that supports Alice and Bob notation. | | Type | Master's thesis [Academic thesis] | | Year | 2012 | | Publisher | Technical University of Denmark, DTU Informatics, E-mail: reception@imm.dtu.dk | | Address | Asmussens Alle, Building 305, DK-2800 Kgs. Lyngby, Denmark | | Series | IMM-M.Sc.-2012-52 | | Note | | | Electronic version(s) | [pdf] | | Publication link | http://www.imm.dtu.dk/English.aspx | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|