• norsk
    • English
  • English 
    • norsk
    • English
  • Login
View Item 
  •   Home
  • Fakultet for informasjonsteknologi og elektroteknikk (IE)
  • Institutt for informasjonssikkerhet og kommunikasjonsteknologi
  • View Item
  •   Home
  • Fakultet for informasjonsteknologi og elektroteknikk (IE)
  • Institutt for informasjonssikkerhet og kommunikasjonsteknologi
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

An automatic protocol composition checker

Kojovic, Ivana
Master thesis
Thumbnail
View/Open
566479_COVER01.pdf (184.0Kb)
566479_FULLTEXT01.pdf (918.0Kb)
URI
http://hdl.handle.net/11250/262714
Date
2012
Metadata
Show full item record
Collections
  • Institutt for informasjonssikkerhet og kommunikasjonsteknologi [1564]
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.
Publisher
Institutt for telematikk

Contact Us | Send Feedback

Privacy policy
DSpace software copyright © 2002-2019  DuraSpace

Service from  Unit
 

 

Browse

ArchiveCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsDocument TypesJournalsThis CollectionBy Issue DateAuthorsTitlesSubjectsDocument TypesJournals

My Account

Login

Statistics

View Usage Statistics

Contact Us | Send Feedback

Privacy policy
DSpace software copyright © 2002-2019  DuraSpace

Service from  Unit