Please use this identifier to cite or link to this item: https://hdl.handle.net/11147/3046
Title: Utilization of timed automata as a verification tool for real-time security protocols
Authors: Külahçıoğlu, Burcu
Advisors: Aytaç, İsmail Sıtkı
Publisher: Izmir Institute of Technology
Abstract: Timed Automata is an extension to the automata-theoretic approach to the modeling of real time systems that introduces time into the classical automata. Since it has been first proposed by Alur and Dill in the early nineties, it has become an important research area and been widely studied in both the context of formal languages and modeling and verification of real time systems. Timed automata use dense time modeling, allowing efficient model checking of time-sensitive systems whose correct functioning depend on the timing properties. One of these application areas is the verification of security protocols. This thesis aims to study the timed automata model and utilize it as a verification tool for security protocols. As a case study, the Neuman-Stubblebine Repeated Authentication Protocol is modeled and verified employing the time-sensitive properties in the model. The flaws of the protocol are analyzed and it is commented on the benefits and challenges of the model.
Description: Thesis (Master)--Izmir Institute of Technology, Computer Engineering, Izmir, 2010
Includes bibliographical references (leaves: 85-92)
Text in English; Abstract: Turkish and English
xi, 92 leaves
URI: http://hdl.handle.net/11147/3046
Appears in Collections:Master Degree / Yüksek Lisans Tezleri

Files in This Item:
File Description SizeFormat 
T000178.pdfMasterThesis2.29 MBAdobe PDFThumbnail
View/Open
Show full item record



CORE Recommender

Page view(s)

150
checked on Mar 25, 2024

Download(s)

120
checked on Mar 25, 2024

Google ScholarTM

Check





Items in GCRIS Repository are protected by copyright, with all rights reserved, unless otherwise indicated.