We present a framework called Formal Policy Framework for Mobility (FPFM)for the specification and verification of domain and inter-domain security policies ina multi-domain mobile network environment. FPFM supports the specification ofsecurity policies with mobility and location constraints, role hierarchy mapping, interdomainservices, inter-domain access rights and separation of duty. The specification of securityolicies in FPFM is based on a formal security policy model, called FPM-RBAC (Formal PolicyModel for Mobility with Role Based Access Control) and a XML based security policyspecification language called XFPM-RBAC (XML Based FormalPolicy Language for Mobility with Role Based Access Control). Formal verification ofsecurity policies ensure that the security policy is satisfied by the network elements in agiven network configuration. FPFM supports extraction of formal specifications fromdefined network configurations, domain and inter-domain security policies. Anothernovel aspect of FPFM is the support for formal information flow analysis related tomobility within multiple security domains. Automated verification of formal specificationsare carried out through model checking and theorem proving. A spatio-temporalmodel checking algorithm has been proposed and a model checking tool has beendeveloped for spatio-temporal model checking of location and mobility constraints insecurity policy rules. Conflicts within security policy rules are resolved through theoremproving with the help of the Coq interactive theorem prover.

Çok etki alanlı ağlarda gezgin bilgisayarların, kaynakların ve kullanıcıların hareketliliğigüvenlik açısından zorluklar meydana getirmektedir. Güvenlik etki alanları arasındahareketlilik içeren eylemler, etki alanında ve etki alanları arasında oluşturulmuş güvenlikpolitikaları bağlamında betimlenmeli ve doğrulanmalıdır. Bu tez kapsamında,FPFM (Gezginlik için Formal Güvenlik Politikası Çerçevesi) adında, çok etki alanlı gezginağlarda kullanıma yönelik, bir güvenlik politikası betimleme ve doğrulama çerçevesiortaya konulmaktadır. FPFM, gezginlik ve konum kısıtları, rol hiyerarşileri eşleştirme,etki alanları arası servisler, etki alanları arası erişim hakları ve görevlerin ayrımı unsurlarınıiçeren güvenlik politikalarının betimlenmesini desteklemektedir. Güvenlikpolitikalarının betimlenmesi için FPM-RBAC adı verilen bir formal güvenlik politikasımodeli ve XFPM-RBAC adı verilen XML tabanlı bir güvenlik politikası diliönerilmektedir. Güvenlik politikalarının doğrulanması, belirli bir ağ yapılandırmasıiçerisinde, güvenlik politikalarının sağlandığının onaylanmasını sağlar. FPFM bu kapsamdatanımlı ağ yapılandırması, etki alanı güvenlik politikası ve etki alanları arasıgüvenlik politikasından formal betimlemelerin üretilmesini sağlamaktadır. FPFM'inkatkı sağladığı alanlardan bir başkası, birden fazla etki alanı içerisindeki gezginlikkaynaklı bilgi akışlarının formal analizidir. Formal betimlemelerin otomatik doğrulanmasıiçin model denetleme ve teorem ispatlama yöntemleri kullanılmaktadır. Güvenlikpolitikaları içerisindeki konum ve hareketlilik kısıtlarının uzay-zaman tabanlı modeldenetlemesi için bir uzay-zaman tabanlı algoritma önerilmiş ve bir model denetlemearacı geliştirilmiştir. Coq etkileşimli teorem doğrulama aracı kullanılarak güvenlikpolitikaları içerisindeki çelişkilerin çözümlenmesi sağlanmıştır.