تحلیل و ارزیابی صوری پروتکل های امنیتی شبکه تترا با استفاده از ابزارهای تحلیل خودکار

Abstract

در این مقاله، ساختار نسخه‌های مختلف پروتکل امنیتی تترا در "مدل صوری" و با استفاده از ابزارهای تحلیل خودکار پرووریف و اسکایتر مورد ارزیابی قرار می‌گیرند. پروتکل امنیتی شبکه تترا از نوع پروتکل‌های تبادل کلید تصدیق شده است که در آن، طرفین ضمن احراز هویت یکدیگر، یک کلید نشست نیز می‌سازند. این پروتکل همچنین از کلیدهای محرمانه از پیش توزیع شده استفاده می‌کند که مبتنی بر ساز و کارهای رمزنگاری متقارن است. تحلیل امنیتی پروتکل مذکور در "مدل صوری" و با استفاده از ابزارهای تحلیل خودکار پرووریف و اسکایتر انجام شده است. در ابتدا، هشت ویژگی امنیتی: محرمانگی، احراز هویت، امنیت پیشرو، امنیت کلید ناشناخته، کلید نشست یکسان، امنیت کلید معلوم، گمنامی و تمامیت را در بستر این ابزارها مدل‌سازی نموده و سپس با استفاده از هر دو ابزار، امنیت پروتکل مذکور را نسبت به این ویژگی‌ها مورد بررسی قرار می‌دهیم. مقایسه نتایج حاصل از تحلیل صوری این ویژگی‌ها با نتایج حاصله از تحلیل‌های غیرصوری در منابع آشکار دلالت بر وجود ضعف‌هایی جدید در ویژگی‌های "امنیت پیشرو" و "تمامیت" در ساختار این پروتکل دارد. در نهایت، روش-هایی برای غلبه بر این ضعف‌ها ارایه شده است.