11471

11471

تحليل صوري پروتكل مديريت شبكهNetConf به كمك ابزار ProVerif

كامپيوتر - مخابرات امن

آبان 1391

آبان 1391

دكتر هادي شهريار شاه حسيني

چكيده امروزه پروتكل‌هاي مديريت شبكه مانند SNMP، NetConf، CMIP، CORBA به طور گسترده‌اي مورد استفاده قرار مي‌گيرند، كه بايد علاوه بر تضمين محرمانگي اطلاعات، احراز هويت و در دسترس بودن، ويژگي‌هاي مورد نياز كاربردهاي مختلف را نيز برآورده كنند. لزوم برقراري اين ويژگي‌ها تا حدي است كه نقض يكي از آن‌ها منجر به مشكلات فراواني براي شبكه مي‌گردد. پروتكل‌هاي مديريتي زيادي براي برآورده سازي اين ويژگي‌هاي امنيتي ارائه شده‌اند، كه امنيت برخي از آنها تنها به صورت غير صوري بررسي شده است. از آنجا كه تحليل غير صوري از دقت بالايي برخوردار نمي‌باشد نياز به يك روش دقيق‌تر در اين زمينه لازم است. يكي از راه‌هاي تحليل امنيت يك پروتكل رمزنگاري، استفاده از روش‌هاي صوري است كه به دليل دقت بالاي آن‌ها در تحليل و ارزيابي، مي‌توانند انتخاب مناسبي براي درستي‌يابي ويژگي‌هاي امنيتي در اين گونه پروتكل‌ها باشند. همچنين بكار بردن روش‌هاي صوري درك بيشتر و دقيق‌تري از پروتكل مي‌دهد و موجب افزايش وضوح توصيف مي‌شود. در مورد پروتكل مديريتي انتخاب شده در اين پايان نامه تا كنون چنين تحليلي صورت نگرفته است. در اين پايان نامه، دو ويژگي مهم امنيتي يعني محرمانگي و احراز هويت براي پروتكل مديريت شبكه NetConf به صورت صوري مورد تحليل قرار گرفته شده است. براي اين منظور، در ابتدا يك مدل انتزاعي از پروتكل NetConf ارائه شده است. سپس به شرح ويژگي‌هاي ابزار تحليل صوري به كار گرفته شده ProVerif پرداخته شده است. در انتها براي برقراري اين ويژگي‌ها در پروتكل مربوطه، پروتكل NetConf با بهره‌گيري از زبان حساب π كاربردي و ابزار ProVerif، مورد تحليل قرار گرفته شده است. نتايج تحليل براي سناريوهاي مختلف ارائه شده از پروتكل، نشان مي‌دهند كه پروتكل مديريت شبكه NetConf براي اثبات ويژگي محرمانگي حتماً بايد از پروتكل لايه انتقال بهره ببرد اما براي اثبات ويژگي احراز هويت از روش‌هاي ديگري مي‌تواند استفاده كند. كلمات كليدي: روش‌هاي صوري، درستي‌يابي، پروتكل مديريت شبكه NetConf، حساب π كاربردي ، ابزار درستي‌يابي خودكار ProVerif