Analysis of the pkmv2 protocol in Ieee 802.16e-2005 using static analysis
Ieee 802.16e-2005 pkmv2 protokolünün statik analizi
- Tez No: 222126
- Danışmanlar: PROF.DR. MEHMET BÜLENT ÖRENCİK
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: IEEE 802.16, WiMAX, LySa, Statik Analiz, Protokol Doğrulama, IEEE 802.16, WiMAX, LySa, Static Analysis, Protocol Verification
- Yıl: 2007
- Dil: İngilizce
- Üniversite: İstanbul Teknik Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 80
Özet
IEEE 802.16e-2005, metropol (büyük şehir) alanlarında telsiz geniş bantlı internet hizmeti için bir hava arabirimi standardıdır. Wimax adıyla bilinen sertifikasyonun temeli olan ve telsiz internet alanında geleceği en parlak görülen IEEE 802.16 standardının en son sürümü olan IEEE 802.16e, gezginlik ve güvenlik alanında iyileştirmeler ve yenilikler içermektedir. Telsiz internet teknolojisi yayınlama yöntemi kullandığı ve dolayısıyla uygun cihazlarla dinlenebildiğinden telsiz internet kullanıcıları, telli ağ kullanıcılarına göre daha fazla risk ile karşı karıyadır. Önceki IEEE 802.16 standartlarında güvenlik amacıyla Gizlilik ve Anahtar Yönetimi adlı, ancak ciddi kritik açıkları bulunan bir protokol kullanılmaktaydı. IEEE 802.16e-2005'te ise bu protokolün yeni sürümü olan PKMv2 kullanılmaktadır. PKMv2 önceki sürüme göre köklü yenilikler içermekle beraber, önceki sürüme gelen ciddi eleştiriler yüzünden bilinen güvenlik önlemlerinin abartılı bir karışımı şeklinde yapılandırılmış haldedir. PKMv2 iki ana görev üstlenmiştir: paylaşılan bir asıllama anahtarı oluşturmak için kullanılan bir asıllama/yetkilendirme protokolü ve güvenlik ilişkilendirmesi trafik şifreleme anahtarının dağıtımı için kullanılan üç adımlı bir el sıkışma protokolü. Bu görevlerden ilki RSA ve EAP gibi yetkinliği ve niteliği bilinen yöntemlere bırakılarak iyileştirilmiştir. Bu tezin konusu, PKMv2'nin diğer görevi olan gezgin istasyonlar arası trafik şifreleme anahtarlarının dağıtımını sağlayan PKMv2 SA-TEK 3W HS adlı el sıkışma protokolüdür. Protokollerinin güvenlik özelliklerinin doğrulanmasında başarıyla kullanılan yöntemlerden biri de statik analizdir. Bu çalışmada statik analiz tekniğinin modern bir telsiz ağ güvenlik protokolü olan PKMv2'de kullanımı gösterilmiştir. Çalışma sonucunda protokolde güvenlikten ödün vermeden performans arttırmaya dayalı iyileştirmeler elde edilmiştir.
Özet (Çeviri)
The IEEE 802.16e-2005 specification provides an air interface standard for metropolitan area wireless broadband service. IEEE 802.16 is the basis for WiMAX certification which is the next evolution in wireless technology while IEEE 802.16e addresses mobility and also enhances the security sublayer. Since wireless technology is broadcast and transmitted data can be intercepted, wireless users are more aware of the risks than wired users. The former IEEE 802.16 standards used the Privacy and Key Management Protocol which had many critical drawbacks. In IEEE 802.16e, a new version of this protocol called PKMv2 is released. PKMv2 has radical changes and in contrast with the previous version it seems to have an exaggerated mixture of security features like nonces, message authentication codes, key ids, certificates, etc. Static analysis is successfully used for automatically validating security properties of classical protocols. In this thesis we will show how the very same technique can be used to validate modern wireless network security protocols, in particular, we study the PKMv2 SA-TEK 3W HS. We derived a model of the protocol and described it using LySa, a process calculus in the pi/spi calculus family allowing communication protocols to be specified and annotated for validation of authentication properties. After that, we carried out a static analysis of our LySa model using the static analysis tool LySa-tool. In conclusion we found improvements that increased the performance while being still secure.
Benzer Tezler
- A comprehensive study on WiMAX security
Başlık çevirisi yok
MURAT MORAN
Yüksek Lisans
İngilizce
2008
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolUniversity of EssexBilgisayar Bilimleri ve Mühendisliği Ana Bilim Dalı
PROF. STUART WALKER
- Gankyrin ve PKM2'nin prognostik biyobelirteç olarak renal hücreli karsinomdaki yeri ve ilişkisi
The prognostic significance of gankryin and PKM2 in renal cell carcinoma
ALİ KEMAL USLUBAŞ
- Erken çocukluk döneminde bilişsel oyun temelli dil gelişim programının çocukların dil gelişimleri üzerindeki etkisi
The influence of cognitive game based language development program on children's language development in early childhood period
KÜBRA ŞULE COŞGUN
Yüksek Lisans
Türkçe
2021
Eğitim ve ÖğretimNecmettin Erbakan ÜniversitesiTemel Eğitim Ana Bilim Dalı
DOÇ. DR. BENGÜ TÜRKOĞLU
- 4-morfolinoasetofenondan türeyen yeni kalkon ve hidrazon türevlerinin sentezi ve biyolojik aktivite çalışmaları
The synthesis and biological activity studies of new chalcones and hydrazones deriving from 4-morpholinoacetophenone
BEDRİYE SEDA KURŞUN AKTAR
Doktora
Türkçe
2017
KimyaGaziantep ÜniversitesiKimya Ana Bilim Dalı
PROF. DR. EMİNE ELÇİN EMRE
PROF. DR. İBRAHİM DEMİRTAŞ
- Meme kanseri ve meme kanser kök hücrelerinde telomeraz inhibitörü bıbr1532 ajanının etkisinin moleküler biyolojik açıdan incelenmesi
Molecular biological investigation of telomerase inhibitor bibr1532 agent effect in breast cancer and breast cancer stem cells
FATMA DOĞAN
Yüksek Lisans
Türkçe
2017
BiyolojiEge ÜniversitesiTıbbi Biyoloji Ana Bilim Dalı
DOÇ. DR. ÇIĞIR BİRAY AVCI