توصيف و تحليل امنيتي پروتكل SNMP بر پايه منطق BAN

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

چكيده پروتكل‌هاي رمزنگاري معمولاً ضامن امنيت در سيستم‌ها و شبكه‌هاي رايانه‌اي به شمارمي‌آيند، حال آن‌كه حصول اطمينان از امنيت خودِ اين پروتكل‌ها به لحاظ طبيعت واكنشيِ آن‌ها، چندان ساده نيست. يكي از پروتكل‌هاي مهم مديريت شبكه، پروتكل مديريت آسان شبكه (SNMP) است كه به دليل استفاده گسترده از آن در قطعات و دستگاه‌هاي تحت شبكه، داراي جايگاه ويژه‌اي در ميان توليدكنندگان و مصرف كنندگان اين تجهيزات است. اين پروتكل داراي سه نسخه است كه در نسخه‌هاي يك و دو آن به امنيت اهميتي داده نشده است ولي به دليل وجود برخي حملات، سازندگان آن در نسخه سه اين پروتكل اهميت ويژه‌اي براي امنيت قائل شده‌اند. يكي ازموضوعات مهم در دنياي فناوري اطلاعات اثبات امنيت پروتكل‌هاي مديريت شبكه است. در اين ميان روش‌هاي متعددي براي اثبات درستي اين پروتكل‌ها وجود دارد كه يكي از مهمترين روش‌ها، روش‌هاي درستي‌يابي صوري است. از ميان روش‌هاي درستي‌يابي صوري اولين مدل منطقي براي تحليل پروتكل‌ها، منطق BAN است كه مطالعه‌ي جدي درستي‌يابي صوري پروتكل‌هاي رمزنگاري با آن شروع شد. در اين پايان‌نامه, به دليل عدم وجود ساختار پروتكلي مشخص براي SNMP, كه در تحليل صوري با استفاده از منطق BAN, به آن نياز داريم, ابتدا با استفاده از مفاهيم بيان شده در RFC‌هاي پشتيبان SNMP, شكل پروتكلي آن را به دست مي‌آوريم(شكست پروتكل انجام مي‌شود). سپس با استفاده از منطق BAN و قوانين آن به توصيف پروتكل SNMP و درستي‌يابي آن مي‌پردازيم. نتيجه كار اثبات احراز اصالت پيام دريافتي كه عامل براي مدير ارسال مي‌كند و يا مدير براي عامل ارسال مي‌كند و همچنين اثبات احراز اصالت مدير و عامل براي يكديگر مي‌شود. اين همان ادعايي بود كه مرجع SNMP در زمان ارائه نسخه سوم آن را بيان كرده بود. واژه‌هاي كليدي: پروتكل مديريت آسان شبكه SNMP، درستي‌يابي صوري، منطق BAN

189058

دانشگاه علم و صنعت ايران

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

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

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