Computer Engineering / Bilgisayar Mühendisliği

Permanent URI for this collectionhttps://hdl.handle.net/11147/10

Browse

Filters

2009 - 200912010 - 20113

Settings

Publisher: search.filters.publisher.Institute of Electrical and Electronics Engineers Inc.Subject: search.filters.subject.Network security

Search Results

Now showing 1 - 4 of 4
  • Conference Object
    Citation - Scopus: 1
    Mutation-Based Evaluation of Weighted Test Case Selection for Firewall Testing
    (Institute of Electrical and Electronics Engineers Inc., 2011) Tuğlular, Tuğkan; Gerçek, Gürcan
    As part of network security testing an administrator needs to know whether the firewall enforces the security policy as expected or not. In this setting black-box testing and evaluation methodologies can be helpful. In this paper we employ a simple mutation operation namely flipping a bit to generate mutant firewall policies and use them to evaluate our previously proposed weighted test case selection method for firewall testing. In the previously proposed firewall testing approach abstract test cases that are automatically generated from firewall decision diagrams are instantiated by selecting test input values from different test data pools for each field of firewall policy. Furthermore a case study is presented to validate the proposed approach. © 2011 IEEE
  • Conference Object
    Modeling Efficient Multi-Chained Stream Signature Protocol Using Communicating Sequential Processeses
    (Institute of Electrical and Electronics Engineers Inc., 2010) Koltuksuz, Ahmet; Özkan, Murat; Külahçıoğlu, Burcu
    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.
  • Conference Object
    Citation - Scopus: 7
    Utilization of Timed Automata as a Verification Tool for Security Protocols
    (Institute of Electrical and Electronics Engineers Inc., 2010) Koltuksuz, Ahmet; Külahçıoğlu, Burcu; Özkan, Murat
    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.
  • Conference Object
    Citation - WoS: 5
    Citation - Scopus: 6
    The 1st Workshop on Model-Based Verification & Validation: Directed Acyclic Graph Modeling of Security Policies for Firewall Testing
    (Institute of Electrical and Electronics Engineers Inc., 2009) Tuğlular, Tuğkan; Kaya, Özgür; Müftüoğlu, Can Arda; Belli, Fevzi
    Currently network security of institutions highly depend on firewalls, which are used to separate untrusted network from trusted one by enforcing security policies. Security policies used in firewalls are ordered set of rules where each rule is represented as a predicate and an action. This paper proposes modeling of firewall rules via directed acyclic graphs (DAG), from which test cases can be automatically generated for firewall testing. The approach proposed follows test case generation algorithm developed for event sequence graphs. Under a local area network setup with the aid of a specifically developed software for this purpose, generated test cases are converted to network test packets, test packets are sent to the firewall under test (FUT), and sent packets are compared with passed packets to determine test result.