|
مروری بر روش های تحلیل و اثبات امنیت پروتکل های امنیتی
|
سیدمحمد دخیل علیان*   ، معصومه صفخانی ، فاطمه پیرمرادیان |
| دانشکده مهندسی برق و کامپیوتر، دانشگاه صنعتی اصفهان، اصفهان، ایران |
|
|
چکیده: (1005 مشاهده) |
ارائه تمامی خدمات از راه دور مستلزم احراز اصالت متقابل طرفین شرکت‌کننده است. چارچوبی که این احراز اصالت به وسیله آن انجام می‌شود، پروتکل‌های احراز اصالت نام دارد. به‌عبارتی، پروتکل رمزنگاری یا رمزنگاشتی یک الگوریتم رمزنگاری توزیع شده است که بین حداقل دو یا چند هستار با یک هدف مشخص تعاملاتی را برقرار می‌نماید. درواقع، این پروتکل‌ها کانال‌های امن و ناامنی برای ارتباط بین طرفین شرکت‌کننده در پروتکل فراهم نموده‌اند. معمولاً از کانال‌های امن جهت ثبت‌نام و از کانال‌های ناامن جهت احراز اصالت متقابل استفاده می‌شود. کاربر بعد از ثبت‌نام در سرور و تأیید اصالت آن توسط سرور می‌تواند از خدماتی که سرور ارائه می‌دهد بهره‌مند شود. پروتکل‌های احراز اصالت بسیاری در زمینه‌هایی مانند مراقبت پزشکی الکترونیکی، اینترنت اشیاء، محاسبات ابری و غیره ارائه شده است. حریم خصوصی و گمنامی کاربران در این طرح‌ها، بزرگ‌ترین چالش در پیاده‌سازی بستر جهت بهره‌مندی خدمات از راه دور است. به دلیل اینکه احراز اصالت کاربران در بستر ناامن اینترنت اتفاق می‌افتد، پس نسبت به تمامی حملات اینترنتی موجود می‌تواند آسیب‌پذیر باشد. به طور کلی دو روش جهت تحلیل و اثبات امنیت پروتکل‌های احراز اصالت وجود دارد. روش صوری و روش غیرصوری. روش غیرصوری که مبتنی بر استدلال‌های شهودی، خلاقیت تحلیلگر و مفاهیم ریاضی است، سعی و تلاش در جهت یافتن خطاها و اثبات امنیت دارد. درحالی‌که روش صوری که به دو صورت دستی و خودکار انجام می‌شود، از انواع منطق‌های ریاضی و ابزارهای تحلیل امنیت خودکار استفاده نموده است. روش دستی با استفاده از مدل‌های ریاضی مانند مدل پیشگوی تصادفی و منطق‌های ریاضی مانند منطق BAN، منطق GNY  و غیره و روش خودکار با استفاده از ابزارهای اویسپا، سایتر، پرووریف، تامارین و غیره انجام شده است. در واقع روش‌های اثبات و تحلیل امنیت پروتکل‌های امنیتی به دو دسته کلی مبتنی بر اثبات قضیه و وارسی مدل تقسیم شده‌اند، که در این مقاله جزئیات هرکدام از این روش‌های اثبات و تحلیل امنیت، تحلیل امنیت پروتکل ECCPWS  با برخی از این روش‌ها و در نهایت مقایسه این روش‌ها با یکدیگر از لحاظ نقاط قوت، نقاط ضعف و غیره بیان شده است. در این مقاله، روش‌های مبتنی بر وارسی مدل و سپس روش‌های مبتنی بر اثبات قضیه شرح داده می‌شود. |
|
| واژه‌های کلیدی: پروتکل‌های احراز اصالت، ابزار تحلیل امنیت پرووریف، ابزار تحلیل امنیت تامارین، ابزار تحلیل امنیت اویسپا، ابزار تحلیل امنیت سایتر، منطق BAN، منطق GNY |
|
|
متن کامل [PDF 2147 kb]
(824 دریافت)
|
نوع مطالعه: مروری |
موضوع مقاله:
رمز و امنیت اطلاعات
دریافت: 1402/9/27 | پذیرش: 1402/12/21 | انتشار: 1403/1/7
|
|
|
|
|
|
|
| ارسال پیام به نویسنده مسئول |
|
|
|
| ارسال نظر درباره این مقاله |
|
|
|
