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

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