Change search
ReferencesLink to record
Permanent link

Direct link
An automatic protocol composition checker
Norwegian University of Science and Technology, Faculty of Information Technology, Mathematics and Electrical Engineering, Department of Telematics.
2012 (English)MasteroppgaveStudent thesis
Abstract [en]

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.

Place, publisher, year, edition, pages
Institutt for telematikk , 2012. , 55 p.
Keyword [no]
ntnudaim:7257, MSSECMOB Master in Security and Mobile Computing
URN: urn:nbn:no:ntnu:diva-19105Local ID: ntnudaim:7257OAI: diva2:566479
Available from: 2012-11-08 Created: 2012-11-08

Open Access in DiVA

fulltext(918 kB)248 downloads
File information
File name FULLTEXT01.pdfFile size 918 kBChecksum SHA-512
Type fulltextMimetype application/pdf
cover(184 kB)22 downloads
File information
File name COVER01.pdfFile size 184 kBChecksum SHA-512
Type coverMimetype application/pdf

By organisation
Department of Telematics

Search outside of DiVA

GoogleGoogle Scholar
Total: 248 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 22 hits
ReferencesLink to record
Permanent link

Direct link