TY - JOUR ID - 200165 TI - تحلیل و ارزیابی صوری پروتکل های امنیتی شبکه تترا با استفاده از ابزارهای تحلیل خودکار JO - پدافند الکترونیکی و سایبری JA - ECD LA - fa SN - 2322-4347 AU - ملازاده گل محله, مهدی AU - سبزی نژاد فراش, محمد AU - رستاقی, روح اله AD - دانشگاه امام حسین (ع) AD - دکتری ریاضی رمز دانشگاه خوارزمی Y1 - 2017 PY - 2017 VL - 5 IS - 4 SP - 109 EP - 129 KW - تحلیل امنیتی KW - مدل های صوری KW - ابزار تحلیل خودکار KW - شبکه تترا DO - N2 - در این مقاله، ساختار نسخه‌های مختلف پروتکل امنیتی تترا در "مدل صوری" و با استفاده از ابزارهای تحلیل خودکار پرووریف و اسکایتر مورد ارزیابی قرار می‌گیرند. پروتکل امنیتی شبکه تترا از نوع پروتکل‌های تبادل کلید تصدیق شده است که در آن، طرفین ضمن احراز هویت یکدیگر، یک کلید نشست نیز می‌سازند. این پروتکل همچنین از کلیدهای محرمانه از پیش توزیع شده استفاده می‌کند که مبتنی بر ساز و کارهای رمزنگاری متقارن است. تحلیل امنیتی پروتکل مذکور در "مدل صوری" و با استفاده از ابزارهای تحلیل خودکار پرووریف و اسکایتر انجام شده است. در ابتدا، هشت ویژگی امنیتی: محرمانگی، احراز هویت، امنیت پیشرو، امنیت کلید ناشناخته، کلید نشست یکسان، امنیت کلید معلوم، گمنامی و تمامیت را در بستر این ابزارها مدل‌سازی نموده و سپس با استفاده از هر دو ابزار، امنیت پروتکل مذکور را نسبت به این ویژگی‌ها مورد بررسی قرار می‌دهیم. مقایسه نتایج حاصل از تحلیل صوری این ویژگی‌ها با نتایج حاصله از تحلیل‌های غیرصوری در منابع آشکار دلالت بر وجود ضعف‌هایی جدید در ویژگی‌های "امنیت پیشرو" و "تمامیت" در ساختار این پروتکل دارد. در نهایت، روش-هایی برای غلبه بر این ضعف‌ها ارایه شده است. UR - https://ecdj.ihu.ac.ir/article_200165.html L1 - https://ecdj.ihu.ac.ir/article_200165_c69e8ec5702966481ef6e6d5580c8eef.pdf ER -