|
|
|
|
نحوه استفاده از ابزار تحلیل امنیت scyther در تحلیل امنیت پروتکل‌های ارتباطی
|
|
|
|
|
DOR
|
20.1001.2.9919138227.1399.1.1.6.5
|
|
نویسنده
|
خدارحم پور محمد ,* * ,صفخانی معصومه ,* *
|
|
منبع
|
همايش ملي آموزش - 1399 - دوره : 12 - دوازدهمین همایش ملی آموزش - کد همایش: 99191-38227
|
|
چکیده
|
امروزه با توجه به افزایش انواع شبکه‌ها، امنیت بیش از پیش مورد توجه کاربران قرار گرفته است و به همین دلیل پروتکل‌های امنیتی زیادی برای تامین امنیت ارائه و توسعه داده شده‌اند. برای اثبات امنیت و یا عدم امنیت دو دسته روش کلی وجود دارد: روش‌های غیرصوری و یا روش‌های صوری. روش‌های غیرصوری مبتنی بر خلاقیت تحلیگر هستند که از قوانین ریاضی برای یافتن خطاها و معایب امنیتی پروتکل و یا اثبات امنیتی پروتکل استفاده می‌کند. در مقابل، روش‌های صوری که خود به دو دسته دستی و خودکار تقسیم می‌‌شوند، به ترتیب از منطق‌هایی نظیر منطق ban، gny و یا ابزارهای خودکار نظیر proverif، avispa، scyther و .... برای اثبات امنیت پروتکل استفاده می کنند.در این مقاله قصد داریم یکی از ابزارهای اثبات صوری خودکار به نام scyther را معرفی کنیم. این ابزار برای تایید یا عدم تایید و تجزیه و تحلیل امنیت پروتکل‌های امنیتی استفاده می‌شود. این ابزار پس از طراحی پروتکل، آن را به صورت مجموعه‌ای از مسیر‌ها در می‌آورد. این کار به ابزار قدرت تحلیل خواهد داد و به بررسی حملات محتمل برروی پروتکل و رفتار‌های احتمالی پروتکل کمک خواهد کرد. در این مقاله، هم چنین، یکی از پروتکل‌های ارائه شده در حوزه اینترنت خودرویی را به صورت گام به گام با بیان جزئیات کامل در محیط ابزار scyther پیاده سازی خواهیم کرد و چگونگی بدست آمدن خروجی را نیز در آن نشان خواهیم داد.
|
|
کلیدواژه
|
اثبات امنیتی، scyther، ابزار اثبات صوری، اینترنت خودرویی
|
|
آدرس
|
*, *, *, *, *, *, *, *, *, *, *, *, *, *, *, *
|
|
پست الکترونیکی
|
*
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Authors
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|