تحقیق در مورد تکنیکCAPSL/CIL AVISS برای توصیف و تحلیل پروتکل های امنیتی
به همراه منابع اصلی و فارسی و نرم افزار AVISPA
بیش از 53 صفحه دکیومنت کامل با فرمت ورد
فهرست
آشنایی با پروتکلهای امنیتی.. 4
ابزارهای مدیریت سایت و شبکه ( Management Tools ) 10
ابزارهای راهبری و نظارت ( Administration Tools ) 10
پی‌گیری مسیر( Trace Route ) 11
مدیریت ترافیک ( Traffic Management ) 12
ابزارهای بررسی کننده پروتکل و ترافیک(Protocol Analyzers & Traffic Monitors) 13
ابزارهای تست پروتکل (Protocol Testers) 15
Awarenet Protocol Tester (PMT-1900) 15
ISTS (Integrated Signalling and Traffic Simulator) 15
ATS (ATM Traffic Generator) 15
ابزارهای کمین کننده (Sniffing Softwares) 15
ابزارهای گمراه کننده (Spoofing Softwares) 16
مدیریت و کنترل سیستم فایلها ( File Systems Control ) 16
محاسبه و کنترل کارکرد کاربران ( Accounting Softwares ) 17
سایر نرم افزارهای امنیتی ( Security Softwares ) 17
ابزارهای تهیه پشتیبان ( BackUp Tools ) 18
تحلیل خودکار پروتکل های امنیتی.. 18
برطرف کردن محدودیت برای تأیید: 20
ابزار تحلیل پروتکل امنیتی AVISS. 21
کنترل کننده فی البداهه مدل (OFMC): 23
کنترل کننده مدل مبتنی بر منطق قیدی: 23
کنترل کننده مدل مبتنی بر SAT(SATMC): 23
تجزیه وتحلیل خودکار پروتکل امنیتی بوسیله ابزارAVISPA. 26
کارایی ها و عملکردهای ابزار 36
پروتکل IKEv2با علائم دیجیتالی.. 40
مقدمه :
با گسترش اینترنت و خدمات بر مبنای شبکه و توسعه امکانات تکنولوژیکی نوین ؛ شمار و مقیاس پروتکل های امنیتی جدید تحت توسعه همگام با توانایی بشری برای تحلیل دقیق و معتبرنمودن آنان می باشد. چنین امری منجر به ایجاد مسأله ای جدی در استاندارد سازی سازمان هایی مانند هیئت مهندسین اینترنت (IETF) ؛ واحد ارتباطات بین المللی( ITU)؛کنسرسیوم شبکه گسترده جهانی (W3C)؛ و یا شرکت های خدماتی یا تولیدی وابسته به استانداردسازی سریع و عملکرد صحیح چنین پروتکل هایی شده است. چنین امری همچنین برای کابران این فن آوری و حقوق آنان در داده شخصی ومحرمانه با توجه به زیربنای آنها مسأله ساز شده است.
طراحی پروتکل های امنیتی مسأله ای دشوار است. درشبکه های باز مانند اینترنت، پروتکل ها باید حتی تحت بدترین شرایط مانند استراق داده های پیام ها بوسیله یک مزاحم( که اغلب مهاجم یا دشمن نامیده می شود) نیز عمل کنند.حملات و هجوم های شدید می توانند حتی بدون رمزشکنی هدایت شوند ولی در عمل با پروتکل ها ناموفق هستند؛ برای مثال " حملات ظاهری" اجرا می گردند ،که بعنوان عاملی صحیح ظاهر می شوند، و یا " حملاتی تکراری" که از یک بخش پروتکل به بخش دیگر مخابره می گردند. احتمال چنین حملاتی اغلب از تصورات غلطی در طراحی پروتکل ها نشأت می گیرد.اساسأ چنین حملاتی بسادگی قابل چشم پوشی اند،هرچند که با بازرسی دقیق پروتکل ها نیز امری دشوار برای افراد است، و به منظور تعیین تمامی راه های یپیچیده ای است که بتواند بخش های مختلف پروتکل را با وجود احتمال نفوذ مهاجمان جاگذاری نماید.
به منظور سرعت بخشیدن به توسعه نسل بعدی پروتکل های امنیتی و گسترش امنیت آنها، داشتن ابزاری در تحلیل پروتکل های امنیتی و کشف عیوب و صحت آنان بسیار حائز اهمیت است. بطور مطلوب، چنین ابزارهایی باید کاملأ خودکار،دقیق، معنادار و به آسانی قابل استفاده باشند به گونه ای که بتوانند توسعه پروتکل ها و فرآیندهای استانداردسازی را یکپارچه سازند.
در دهه اخیر، شاهد رشد شمار بسیاری از تکنیک ها در تحلیل پروتکل های امنیتی می باشیم.بسیاری از این ابزارهای تحلیلی پروتکل های امنیتی بصورت (eg,[3,21,23,26,27,28,41,42,43,61,64,66,69,71,73,76])پیشنهاد شده اند؛ که می توانند پروتکل های با مقیاس کوچک و متوسط (کتابخانه Clark/Jacob) را تجزیه و تحلیل کنند. در هر حال، پروتکل های امنیتی در مقیاس صنعتی چالشی از نظر تکنولوژی و علم است.
ابزار AVISS(تأیید خودکار سیستم های حالت نامحدود) را برای تحلیل پروتکل امنیتی شرح می دهیم؛ AVISSاز یکپارچه سازی ساده موتورهای جستجوی مختلف back-end پشتیبانی می کند. به عنوان مثال کنترل کننده فی البداهه مدل را پیاده شده است؛ این کنترل کننده یک تحلیلگر مبتنی بر منطق قیدی و یک کنترل کننده مدل مبتنی بر SATاست. اگرچه هر یک از این back-endها می توانند به صورت مستقل کار کنند، درآوردن آنها به صورت یک ابزار واحد امکان مقایسه سیستماتیک و کمی توان های نسبی آنها را میسر و راه را برای تعامل مؤثر آنها هموار می سازد. که به عنوان نخستین آزمایش از این ابزار برای تحلیل و یافتن خطاها در 36 پروتکل استفاده شده از جمله خطای از پیش نامعلوم در پروتکل Denning-Saccoو حملات قبلا گزارش شده (مأخذ 4 را ملاحظه نمایید) تا 31 پروتکل (مأخذ 2).
تحقیق در مورد تکنیکCAPSL CIL AVISS برای توصیف و تحلیل پروتکل های امنیتی