Geri Dön

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ı

  1. Tez No: 266633
  2. Yazar: SÜLEYMAN MURAT ÖZKAN
  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ı: 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

  1. 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

    İngilizce

    2021

    Elektrik ve Elektronik Mühendisliğiİstanbul Teknik Üniversitesi

    Elektronik ve Haberleşme Mühendisliği Ana Bilim Dalı

    PROF. DR. SIDDIKA BERNA ÖRS YALÇIN

  2. 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

    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

  3. 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

    Türkçe

    2024

    İnşaat MühendisliğiPamukkale Üniversitesi

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

    PROF. DR. MAHMUD GÜNGÖR

  4. 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

    İngilizce

    2020

    Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik Üniversitesi

    Bilgisayar Mühendisliği Ana Bilim Dalı

    PROF. DR. MUSTAFA ERSEL KAMAŞAK

    PROF. DR. MUHİTTİN GÖKMEN

  5. 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

    Doktora

    Türkçe

    Türkçe

    2021

    CoğrafyaFırat Üniversitesi

    Coğrafya Ana Bilim Dalı

    PROF. DR. MURAT SUNKAR