11626

11626

تحليل صوري ويژگي هاي امنيتي پروتكل مديريت شبكه SNMP و درستي يابي آن به كمك ابزار ProVerif

كارشناسي ارشد

برق - مهندسي فناوري اطلاعات - مخابرات امن

دي ماه 1391

دي ماه 1391

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

دكتر مجيد نادري

چكيده امروزه شبكه¬هاي ارتباطي در گستره وسيعي شامل تمام جهان و با كاربران بسيار زيادي كه انتظارات مختلفي از شبكه دارند در حال فعاليت است. بديهي است چنين شبكه‌هاي بزرگي نمي‌تواند تنها توسط تلاش‌هاي انساني، نظارت و كنترل شوند. لذا پيچيدگي چنين سيستمي، استفاده از ابزارهاي خودكار مديريتي را ايجاب مي‌كند. در پاسخ به اين نيازها، استانداردهايي كه مرتبط با مديريت شبكه هستند تهيه شده كه سرويس ها، پروتكل‌ها و پايگاه هاي اطلاعات مديريتي را پوشش مي‌دهند. تا زمان حاضر پراستفاده ترين استانداردي از اين نوع، پروتكل مديريت شبكه SNMP بوده است. يكي از راه¬هاي تحليل امنيت يك سيستم، استفاده از روش¬هاي صوري است كه به دليل دقت بالا¬ي آن در تحليل و ارزيابي، مي¬تواند انتخاب مناسبي براي درستي يابي ويژگي¬هاي امنيتي در اينگونه سيستم¬ها باشد. به بيان دقيق‏تر يك روش صوري در واقع تركيبي از يك زبان توصيف براي توصيف نيازمندي‏هاي سيستم، فنون استدلال و تحليل براي درستي‏يابي رفتار سيستم و ابزارهائي براي خودكار كردن فرآيند صوري سازي است. در آخرين نسخه پروتكل مديريت شبكه SNMP دو دسته مهم ويژگي‌هاي امنيتي (احراز اصالت و محرمانگي) توسط مدل امنيتي مبتني بر كاربر USM گنجانده شده است. لزوم برقراري اين ويژگيها تاحدي است كه نقض حتي يكي از آنها مي تواند تبعات جبران ناپذيري براي آن جامعه در پي داشته باشد و از آنجايي كه اين خصوصيات امنيتي تا بحال با هيچ ابزار صوري مورد اثبات و تحليل قرار نگرفته، لذا بر آن شديم تا هدف اين پايان¬نامه را تحليل و ارائه يك اثبات صوري براي ويژگي¬هاي موجود در نسخه سوم اين پروتكل قرار دهيم. در اين پايان¬نامه برقراري دو ويژگي احراز اصالت و محرمانگي در پروتكل SNMPv3 مورد تحليل و بررسي صوري قرار مي‌گيرد. براي رسيدن به اين هدف، ساختاري براي ترسيم گام¬ها و عمليات پروتكل پيشنهاد شده است كه اين ساختار ضمن دربرداشتن تمامي عوامل مديريتي مبادله شده بين عامل و مديرSNMP بايستي ويژگي¬هاي امنيتي كه USM به SNMPv3 افزوده بود را نيز در بر داشته باشد. پس از اين مرحله، با بهره¬گيري از زبان مبتني بر حساب كاربردي π توصيفي صوري از پروتكل ارائه شده است و در نهايت به كمك ابزار ProVerif،كه در درستي¬يابي اثبات بسياري از ويژگي¬ها موفق بوده است، اين ويژگي¬هاي امنيتي بررسي شده است. نتايج بدست آمده از تحليل پروتكل SNMPv3 و در ابزار ProVerif حاكي از آن مي باشد كه ويژگي¬هاي محرمانگي و احراز اصالت در اين پروتكل برقرار مي مانند. واژه‌هاي كليدي: اثبات قضيه خودكار، درستي¬يابي پروتكل، پروتكل مديريت شبكه SNMP ، حساب كاربردي π.