Geri Dön

Utilization of timed automata as a verification tool for real-time security protocols

Zamanlı özdevinim kuramının gerçek zamanlı güvenlik protokollerinin doğrulanmasında kullanımı

  1. Tez No: 266604
  2. Yazar: BURCU KÜLAHÇIOĞLU
  3. Danışmanlar: DOÇ. DR. AHMET KOLTUKSUZ, PROF. DR. SITKI AYTAÇ
  4. Tez Türü: Yüksek Lisans
  5. Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
  6. Anahtar Kelimeler: Belirtilmemiş.
  7. Yıl: 2010
  8. Dil: İngilizce
  9. Üniversite: İzmir Yüksek Teknoloji Enstitüsü
  10. Enstitü: Mühendislik ve Fen Bilimleri Enstitüsü
  11. Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
  12. Bilim Dalı: Belirtilmemiş.
  13. Sayfa Sayısı: 103

Özet

Zamanlı özdevinim kuramı, klasik özdevinirler (otomata) kavramına zaman değişkenini ekleyerek bu modeli genişleten bir kuramdır. Doksanlı yılların başlarında öne sürülen zamanlı özdevinim kuramı, hem biçimsel diller hem de gerçek zamanlı sistem modelleme ve doğrulama alanlarında geniş ölçüde çalışılmaktadır. Zamanı sürekli bir değişken olarak ele alan zamanlı özdevinirler, doğru çalışması zaman kısıtlarına bağlı olan zaman kritik sistemler üzerinde model denetimine olanak sağlamaktadır. Bu uygulama alanlarından biri de güvenlik protokollerinin doğrulanmasıdır.Bu tezde, zamanlı özdevinim kuramının incelenmesi ve güvenlik protokollerinin doğrulanmasında kullanımı amaçlanmaktadır. Bir durum çalışması olarak, Neuman-Stubblebine Tekrarlı Kimlik Denetimi Protokolü'nün, zamana bağlı özellikleri de dahil edilerek modellenmesi ve doğrulanması sunulmaktadır. Protokolün doğrulama sonuçları incelenerek modelin artı ve eksileri üzerinde yorumlara da yer verilmektedir.

Özet (Çeviri)

Timed Automata is an extension to the automata-theoretic approach to the modeling of real time systems that introduces time into the classical automata. Since it has been first proposed by Alur and Dill in the early nineties, it has become an important research area and been widely studied in both the context of formal languages and modeling and verification of real time systems. Timed automata use dense time modeling, allowing efficient model checking of time-sensitive systems whose correct functioning depend on the timing properties. One of these application areas is the verification of security protocols.This thesis aims to study the timed automata model and utilize it as a verification tool for security protocols. As a case study, the Neuman-Stubblebine Repeated Authentication Protocol is modeled and verified employing the time-sensitive properties in the model. The flaws of the protocol are analyzed and it is commented on the benefits and challenges of the model.

Benzer Tezler

  1. Bir tekstil firmasında kanban sisteminin uygulanması

    An Application of kanban system in a textile company

    UĞUR ÖZÇER

    Yüksek Lisans

    Türkçe

    Türkçe

    1995

    Mühendislik Bilimleriİstanbul Teknik Üniversitesi

    DOÇ.DR. SEMRA DURMUŞOĞLU

  2. Otomasyon yönetiminde insan faktörü ve Türk Otomotiv Sektöründe bir uygulama

    Human factors in automation management and an application in Turkish Automative Industry

    HALUK KÜÇÜK

    Yüksek Lisans

    Türkçe

    Türkçe

    1995

    Mühendislik Bilimleriİstanbul Teknik Üniversitesi

    DOÇ.DR. İ. HAKKI BİÇER

  3. A data fusion approach for monitoring activities in double shift construction sites using sensor-based data tracking technologies

    Şantiyelerde aktivite ilerlemelerinin algılayıcı tabanlı veri takip teknolojileri kullanılarak tespit edilmesi için bir veri füzyonu yaklaşımı

    GÜRŞANS GÜVEN IŞIN

    Doktora

    İngilizce

    İngilizce

    2016

    Bilim ve Teknolojiİstanbul Teknik Üniversitesi

    İnşaat Mühendisliği Ana Bilim Dalı

    DOÇ. DR. ESİN ERGEN PEHLEVAN

  4. Sürdürülebilir toplu konut yerleşmesi tasarımı için Pareto genetik algoritmaya dayalı bir model önerisi: SSPM

    A model for sustainable site layout design with pareto genetic algorithm: SSPM

    YAZGI AKSOY

    Doktora

    Türkçe

    Türkçe

    2016

    Mimarlıkİstanbul Teknik Üniversitesi

    Bilişim Ana Bilim Dalı

    PROF. DR. GÜLEN ÇAĞDAŞ

  5. A fast 3d flow field prediction around bluff bodies using deep learning

    Derin öğrenme kullanılarak küt cisimler etrafındaki 3 boyutlu akış alanının tahmini

    FARHAD NEMATI TAHER

    Yüksek Lisans

    İngilizce

    İngilizce

    2023

    Makine Mühendisliğiİstanbul Teknik Üniversitesi

    Makine Mühendisliği Ana Bilim Dalı

    DOÇ. DR. ABDUSSAMET SUBAŞI