Analysis Of The Pkmv2 Protocol In Ieee 802.16e-2005 Using Static Analysis

Tez (Yüksek Lisans) -- İstanbul Teknik Üniversitesi, Fen Bilimleri Enstitüsü, 2007Thesis (M.Sc.) -- İstanbul Technical University, Institute of Science and Technology, 2007IEEE 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.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.Yüksek LisansM.Sc