Please use this identifier to cite or link to this item: https://hdl.handle.net/11147/3819
Title: Modeling and verification of a stream authentication protocol using communicating sequential processes
Authors: Aytaç, İsmail Sıtkı
Özkan, Süleyman Murat
Issue Date: 2010
Publisher: Izmir Institute of Technology
Abstract: Although most systems used for computation are concurrent systems, classical theories of computation are generally involved in sequential formalisms. Thus, mathematical methods are developed for modeling and analyzing the behavior of concurrent and reactive systems. One of these formal methods is Communicating Sequential Processes (CSP), which is a process algebra proposed by Hoare in the 1970s. Broad theory of CSP captures different properties of processes by using different approaches within a unifying formalization. Many security protocols are modeled with CSP and successfully verified using model-checking or theorem proving techniques. Unlike other authentication protocols modeled using CSP, each of the Efficient Multi-chained Stream Signature (EMSS) protocol messages are linked to the previous messages, forming hash chains, which introduce difficulties into the modeling and verification. In this thesis the EMSS stream authentication protocol is modeled using CSP and its authentication properties are verified using model checking, which in turn calls for building an infinite state model of the protocol that is also successfully reduced into a finite state 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
x, 71 leaves
URI: http://hdl.handle.net/11147/3819
Appears in Collections:Master Degree / Yüksek Lisans Tezleri

Files in This Item:
File Description SizeFormat 
T000847.pdfMasterThesis1.57 MBAdobe PDFThumbnail
View/Open
Show full item record

CORE Recommender

Page view(s)

32
checked on Dec 5, 2022

Download(s)

20
checked on Dec 5, 2022

Google ScholarTM

Check


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