@MASTERSTHESIS\{IMM2012-06373,
    author       = "I. Kojovic",
    title        = "An Automatic Protocol Composition Checker",
    year         = "2012",
    school       = "Technical University of Denmark, {DTU} Informatics, {E-}mail: reception@imm.dtu.dk",
    address      = "Asmussens Alle, Building 305, {DK-}2800 Kgs. Lyngby, Denmark",
    type         = "",
    note         = "Supervised by Associate Professor Sebastian Alexander M{\"{o}}densheim, samo@imm.dtu.dk, {DTU} Informatics, co-supervision Danilo Gligoroski from {NTNU}.",
    url          = "http://www.imm.dtu.dk/English.aspx",
    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."
}