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ı
- Tez No: 266604
- Danışmanlar: DOÇ. DR. AHMET KOLTUKSUZ, PROF. DR. SITKI AYTAÇ
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Formel doğrulama, Güvenlik protokolleri, Model doğrulama, Özdevinir, Formal verification, Security protocols, Model check, Automata
- Yıl: 2010
- Dil: İngilizce
- Üniversite: İzmir Yüksek Teknoloji Enstitüsü
- Enstitü: Mühendislik ve Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: Belirtilmemiş.
Ö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
- Bir tekstil firmasında kanban sisteminin uygulanması
An Application of kanban system in a textile company
UĞUR ÖZÇER
- 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
2023
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
DOÇ. DR. ABDUSSAMET SUBAŞI
- Kurumsal kaynakların planlaması (ERP) ve çağdaş üretim-yönetim sistemleri ile ilişkiler
Enterprise resources planning (ERP) and relationships among ERP and other computer aided systems and management information system
BURÇİN ÇARDAK
Yüksek Lisans
Türkçe
2000
Endüstri ve Endüstri Mühendisliğiİstanbul Teknik ÜniversitesiDOÇ.DR. ALPASLAN FIĞLALI
DOÇ.DR. MEHMET TANYAŞ
DOÇ.DR. SEMRA BİRGÜN BARLA
- Ai-based optimization of blockchain protocols for cybersecurity in iot systems in medium-sized organizations
Orta ölçekli kuruluşlarda ıot sistemlerinde siber güvenlik için yapay zeka tabanlı blok zinciri protokol optimizasyonu
KHALIFA EHFAYED KHALIFA SHNEINA
Yüksek Lisans
İngilizce
2025
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolAltınbaş ÜniversitesiElektrik ve Bilgisayar Mühendisliği Ana Bilim Dalı
DR. ÖĞR. ÜYESİ MUHAMMAD ILYAS
- A conceptual model for image recognition based progress monitoring: retail construction and finishing works
Görüntü tanıma tabanlı ilerleme takibi için kavramsal bir model: perakende inşaat ve ince yapı işleri
SALİH KAAN MAZLUM
Doktora
İngilizce
2025
Mimarlıkİstanbul Teknik ÜniversitesiMimarlık Ana Bilim Dalı
PROF. DR. BEGÜM SERTYEŞİLIŞIK