16669

16669

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

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

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

ارديبهشت ماه 1392

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

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

برق

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

1395/11/27

1/1/1900 12:00:00 AM

Abstract: Cryptographic protocols usually Guarantor of security in the systems an​d Computer networks, while ensuring the security of the protocol itself in terms of the nature of their Reaction, is not so simple. One of the important protocols for network management, Simple Network Management Protocol (SNMP) due to the extensive use of its components an​d network devices, has a special place among producers an​d consumers of this equipment. The protocol has three versions in versions one an​d two it is not given much importance to security but because there are some attacks, its creators have been made in version three of these protocols special importance to the security. One important issue in the world of information technology, proven security of network management protocols. In the meantime, there are many ways to prove the correctness of this protocol which is one of the most important methods, formal verification methods.The first formal verification methods in a logical model protocol analyzer, BAN logic is that a serious study of the formal verification of cryptographic protocols it began. In this thesis, due to the lack of structure for the SNMP protocol at formal analysis using BAN logic, to need, using the concepts described in RFC backup SNMP, the protocol to obtain. Then, using BAN logic an​d its laws, we describe SNMP protocol an​d its verification. The result proved, Proof authentication of the received message that is sent agent to manager o​r sent manager to agent an​d The proof of authentication manager an​d agent for one another. This is the claim that SNMP reference at the time had expressed its third edition. Keywords: Simple Network Management Protocol (SNMP), formal verification, BAN logic.