Modeling and verification of a stream authentication protocol using communicating sequential processes
Haberleşen sıralı süreçler kullanarak bir akış kimlik denetimi protokolünün modellenmesi ve doğrulanması
- Tez No: 266633
- 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: Belirtilmemiş.
- 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ı: 81
Özet
Hesaplamada kullanılan sistemlerin çoğu eşzamanlı sistemler olmasına rağmen, klasik hesaplama kuramı genel olarak sıralı sistemler üzerinde durmaktadır. Bu nedenle, eşzamanlı ve birbiriyle iletişim içinde olan sistemlerin modellenmesi ve doğrulanması için matematiksel yöntemler geliştirilmiştir. Bu yöntemlerden birisi olan Haberleşen Sıralı Süreçler (CSP), Hoare tarafından yetmişli yıllarda geliştirilen bir süreç cebiridir. CSP'nin kapsamlı kuramı, süreçlerin değişik özelliklerini, değişik yaklaşımları kullanarak yakalamaya izin verir.Birçok güvenlik protokolü CSP ile modellenmiş ve model denetimi veya kuram ispatı teknikleri kullanılarak bu protokollerin doğruluğu gösterilmiştir. CSP ile modellenmiş olan diğer kimlik denetimi protokollerinden farklı olarak, her bir Verimli Çoklu-Zincirli Akış İmzası (EMSS) protokol mesajı, modelleme ve doğrulamada zorluk yaratacak şekilde, önceki mesajlara özet zincirleri ile bağlıdır. Bu tezde, EMSS akış kimlik denetimi protokolü CSP ile modellenmiş ve kimlik denetimi özellikleri, model denetimi yöntemlerini kullanarak doğrulanmıştır.
Özet (Çeviri)
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.
Benzer Tezler
- An FPGA implementation of a RISC-V based SOC system with custom instruction set for image processing applications
Görüntü işleme uygulamaları için özel komut setine sahip RISC-V tabanlı bir SOC sısteminin FPGA gerçeklemesi
ERFAN GHOLIZADEHAZARI
Yüksek Lisans
İngilizce
2021
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiElektronik ve Haberleşme Mühendisliği Ana Bilim Dalı
PROF. DR. SIDDIKA BERNA ÖRS YALÇIN
- Küçük akarsu havzalarında hidroenerji potansiyelinin belirlenmesi için en uygun modelin araştırılması
Investigation of the optimal method for determining hydropower potential of small stream basins
İBRAHİM HALİL DEMİREL
Doktora
Türkçe
2021
İnşaat MühendisliğiYıldız Teknik Üniversitesiİnşaat Mühendisliği Ana Bilim Dalı
PROF. DR. İBRAHİM YÜKSEL
- Denizli ili Serinhisar ilçe merkezi taşkın yayılım alanlarının coğrafi bilgi sistemleri ve HEC-RAS paket programı ile modellenmesi
Modeling of flood inundation areas in Denizli province Serinhisar district center with geographical information systems and HEC-RAS package program
ABDUL LATIF RUSTAM OGHLY
Yüksek Lisans
Türkçe
2024
İnşaat MühendisliğiPamukkale Üniversitesiİnşaat Mühendisliği Ana Bilim Dalı
PROF. DR. MAHMUD GÜNGÖR
- Face recognition and person re-identification for person recognition
Kişi tanıma için yüz tanıma ve kişinin yeniden tanınması
EMRAH BAŞARAN
Doktora
İngilizce
2020
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. MUSTAFA ERSEL KAMAŞAK
PROF. DR. MUHİTTİN GÖKMEN
- Ağrı ve Doğubayazıt havzalarında coğrafi faktörlerin sel ve taşkın oluşumundaki etkisi ve taşkın risk analizleri
Effects of geographical factors on torrent and flood formation in Ağrı and Doğubayazıt basins and flood risk analysis
AHMET TOPRAK