تحلیل و ارزیابی صوری پروتکل های امنیتی شبکه تترا با استفاده از ابزارهای تحلیل خودکار
Publish place: Electronic and cyber defense، Vol: 5، Issue: 4
Publish Year: 1396
نوع سند: مقاله ژورنالی
زبان: Persian
View: 339
This Paper With 21 Page And PDF Format Ready To Download
- Certificate
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
JR_PADSA-5-4_009
تاریخ نمایه سازی: 7 اردیبهشت 1400
Abstract:
در این مقاله، ساختار نسخههای مختلف پروتکل امنیتی تترا در "مدل صوری" و با استفاده از ابزارهای تحلیل خودکار پرووریف و اسکایتر مورد ارزیابی قرار میگیرند. پروتکل امنیتی شبکه تترا از نوع پروتکلهای تبادل کلید تصدیق شده است که در آن، طرفین ضمن احراز هویت یکدیگر، یک کلید نشست نیز میسازند. این پروتکل همچنین از کلیدهای محرمانه از پیش توزیع شده استفاده میکند که مبتنی بر ساز و کارهای رمزنگاری متقارن است. تحلیل امنیتی پروتکل مذکور در "مدل صوری" و با استفاده از ابزارهای تحلیل خودکار پرووریف و اسکایتر انجام شده است. در ابتدا، هشت ویژگی امنیتی: محرمانگی، احراز هویت، امنیت پیشرو، امنیت کلید ناشناخته، کلید نشست یکسان، امنیت کلید معلوم، گمنامی و تمامیت را در بستر این ابزارها مدلسازی نموده و سپس با استفاده از هر دو ابزار، امنیت پروتکل مذکور را نسبت به این ویژگیها مورد بررسی قرار میدهیم. مقایسه نتایج حاصل از تحلیل صوری این ویژگیها با نتایج حاصله از تحلیلهای غیرصوری در منابع آشکار دلالت بر وجود ضعفهایی جدید در ویژگیهای "امنیت پیشرو" و "تمامیت" در ساختار این پروتکل دارد. در نهایت، روش-هایی برای غلبه بر این ضعفها ارایه شده است.
Keywords:
Authors
مهدی ملازاده گل محله
دانشگاه امام حسین (ع)
محمد سبزی نژاد فراش
دکتری ریاضی رمز دانشگاه خوارزمی
روح اله رستاقی
دانشگاه امام حسین (ع)
مراجع و منابع این Paper:
لیست زیر مراجع و منابع استفاده شده در این Paper را نمایش می دهد. این مراجع به صورت کاملا ماشینی و بر اساس هوش مصنوعی استخراج شده اند و لذا ممکن است دارای اشکالاتی باشند که به مرور زمان دقت استخراج این محتوا افزایش می یابد. مراجعی که مقالات مربوط به آنها در سیویلیکا نمایه شده و پیدا شده اند، به خود Paper لینک شده اند :