Modeling and verification of a stream authentication protocol using communicating sequential processes
by
Özkan, Süleyman Murat.
Title
:
Modeling and verification of a stream authentication protocol using communicating sequential processes
Author
:
Özkan, Süleyman Murat.
Personal Author
:
Özkan, Süleyman Murat.
Publication Information
:
[s.l.]: [s.n.], 2010.
Physical Description
:
x, 71 leaves.: ill. + 1 computer laser optical disc.
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.
Subject Term
:
CSP(Computer program language)
Secuential processing(Computer science)
Added Author
:
Aytaç, Sıtkı.
Added Corporate Author
:
İzmir Institute of Technology. Computer Engineering.
Added Uniform Title
:
Thesis (Master)--İzmir Institute of Technology: Computer Engineering.
İzmir Institute of Technology: Computer Engineering--Thesis (Master).
Electronic Access
:
Library | Material Type | Item Barcode | Shelf Number | Status |
---|
IYTE Library | Thesis | T000847 | QA76.73.C75 O99 2010 | Tez Koleksiyonu |
IYTE Library | Supplementary CD-ROM | ROM1645 | QA76.73.C75 O99 2010 EK1 | Tez Koleksiyonu |