Browsing by Author "Ozkan, Murat"

Filter results by typing the first few letters
Now showing 1 - 2 of 2
  • Thumbnail Image
    Conference Object
    Modeling efficient multi-chained stream signature protocol using communicating sequential processeses
    (2010) Ahmet Hasan Koltuksuz; Murat Ozkan; Burcu Külahçioǧlu; Kulahcioglu, Burcu; Ozkan, Murat; Koltuksuz, Ahmet
    Communicating Sequential Processes (CSP) is a process algebra designed for modeling and analyzing the behavior of concurrent systems. Several security protocols are modeled with CSP and verified using model-checking or theorem proving techniques successfully. 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 introduces difficulties for modeling and verification. In this paper, we model the EMSS stream authentication protocol using CSP and verify its authentication properties with model checking by building an infinite state model of the protocol which is reduced into a finite state model. © 2010 IEEE. © 2010 Elsevier B.V. All rights reserved.
  • Thumbnail Image
    Conference Object
    Citation - Scopus: 7
    Utilization of timed automata as a verification tool for security protocols
    (2010) Ahmet Hasan Koltuksuz; Burcu Külahçioǧlu; Murat Ozkan; Kulahcioglu, Burcu; Ozkan, Murat; Koltuksuz, Ahmet
    Timed Automata is an extension to the automata-theoretic approach for the modeling of real time systems that introduces time into the classical automata. It has become an important research area in both the context of formal languages and modeling and verification of real time systems since it was proposed by Alur and Dill in the early nineties. Timed automata proposes an efficient model checking method for verification real time systems having mature and efficient automatic verification tools. One of the application areas of timed automata is the verification of security protocols which are known to be time sensitive. This study aims to make use of timed automata as a verification tool for security protocols and gives a case study on the initial part of the Neuman- Stubblebine Repeated Authentication Protocol. © 2010 IEEE. © 2010 Elsevier B.V. All rights reserved.