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

نویسندگان

1 دانشگاه امام حسین (ع)

2 دکتری ریاضی رمز دانشگاه خوارزمی

چکیده

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

کلیدواژه‌ها

مراجع

  1. B. Torke Ladani, “Formal Analyzing of Security Protocols,” PHD Dissertation, Tarbiat Modars Universiry, 2004.
  2. M. Abadi, B. Blanchet, and C. Fournet, “The applied pi calculus: Mobile values, new names, and secure
  3. communication,” Report arXiv: 1609.03003v1, September 2016. Available at http://arxiv.org/abs/1609.03003v1.
  4. B. Blanchet, “Automatic Verification of Security Protocols in the Symbolic Model: the Verifier ProVerif. In FOSAD 7,” LNCS, vol. 8604, pp. 54-87, 2014.
  5. B. Blanchet, “Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif,” Foundations and Trends in Privacy and Security, pp. 1-135, October 2016.
  6. Proverif, http://prosecco.gforge.inria.fr/personal/bblanche/proverif/
  7. D. Basin, C. Cremers, and C. Meadow, “Handbook of Model Checking: Model Checking Security Protocols,” springer,
  8. C. Cremers and S. Mauw, “Operational Semantics and Verification of Security Protocols,” Springer, 2012.
  9. C. Cremers, “The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols,” CAV 2008, LNCS, vol. 5123, pp. 414-418, 2008.
  10. S. Duan, “Security Analysis of TETRA,” Master thesis, Norwegian University of Science and Technology, 2013.
  11. Scyther,
  12. https://www.cs.ox.ac.uk/people/cas.cremers/scyther/index.html
  13. “ETSI Technical Standard ETSI EN 302 109 V1.1.1 Terrestrial Trunked Radio (TETRA),” Security
  14. Synchronization mechanism for end-to-end encryption, 2003.
  15. “TETRA Association SFPG Information document,” Overview of Standard TETRA Cryptographic Algorithms and
  16. their rules for management and distribution.
  17. ETSI Technical Report TR 052101 V1.1.1: SAGE Rules for the management of the TETRA standard authentication and key management algorithm set TAA1.
  18. ETSI Technical Report TR 1-0530101 V1.1.2: SAGE Rules for the management of the TETRA standard encryption algorithms Part1 TEA1.
  19. ETSI Technical Standard ETSI EN 300 392-7 V2.1.1: Terrestrial Trunked Radio (TETRA), Voice plus Data( V+D), Part 7: Security.
پدافند الکترونیکی و سایبری
دوره 5، شماره 4 - شماره پیاپی 4
800
اسفند 1396
صفحه 109-129

فایل ها

سابقه مقاله

  • تاریخ دریافت: 01 مرداد 1395
  • تاریخ بازنگری:
  • تاریخ پذیرش: 28 شهریور 1397
  • تاریخ انتشار: 10 دی 1396

هم رسانی

ارجاع به این مقاله

آمار