مهدی ملازاده گل محله - دانشگاه امام حسین (ع)
محمد سبزی نژاد فراش - دکتری ریاضی رمز دانشگاه خوارزمی
روح اله رستاقی - دانشگاه امام حسین (ع)

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

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