An automatic protocol composition checker

Abstract

Formal analysis is widely used to prove security properties of the 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 through 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 proto- cols to test the checker.We want to implement the checker as an extension of the existing Open-Source Fixed-Point Model-Checker OFMC to easily integrate our composition checker with a existing verification procedure that support Alice and Bob notation.