Modeling and verification of a stream authentication protocol using communicating sequential processes için kapak resmi
Modeling and verification of a stream authentication protocol using communicating sequential processes
Başlık:
Modeling and verification of a stream authentication protocol using communicating sequential processes
Yazar:
Özkan, Süleyman Murat.
Yazar Ek Girişi:
Yayın Bilgileri:
[s.l.]: [s.n.], 2010.
Fiziksel Tanımlama:
x, 71 leaves.: ill. + 1 computer laser optical disc.
Özet:
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.
Yazar Ek Girişi:
Tek Biçim Eser Adı:
Thesis (Master)--İzmir Institute of Technology: Computer Engineering.

İzmir Institute of Technology: Computer Engineering--Thesis (Master).
Elektronik Erişim:
Access to Electronic Version.
Ayırtma: Copies: