آمار

تعداد نشریات39
تعداد شماره‌ها1,170
تعداد مقالات8,437
تعداد مشاهده مقاله6,314,123
تعداد دریافت فایل اصل مقاله3,561,441
ملازاده گل محله, مهدی, سبزی نژاد فراش, محمد, رستاقی, روح اله. (1396). تحلیل و ارزیابی صوری پروتکل های امنیتی شبکه تترا با استفاده از ابزارهای تحلیل خودکار. پدافند الکترونیکی و سایبری, 5(4), 109-129.
مهدی ملازاده گل محله; محمد سبزی نژاد فراش; روح اله رستاقی. "تحلیل و ارزیابی صوری پروتکل های امنیتی شبکه تترا با استفاده از ابزارهای تحلیل خودکار". پدافند الکترونیکی و سایبری, 5, 4, 1396, 109-129.
ملازاده گل محله, مهدی, سبزی نژاد فراش, محمد, رستاقی, روح اله. (1396). 'تحلیل و ارزیابی صوری پروتکل های امنیتی شبکه تترا با استفاده از ابزارهای تحلیل خودکار', پدافند الکترونیکی و سایبری, 5(4), pp. 109-129.
ملازاده گل محله, مهدی, سبزی نژاد فراش, محمد, رستاقی, روح اله. تحلیل و ارزیابی صوری پروتکل های امنیتی شبکه تترا با استفاده از ابزارهای تحلیل خودکار. پدافند الکترونیکی و سایبری, 1396; 5(4): 109-129.

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

پدافند الکترونیکی و سایبری
مقاله 6، دوره 5، شماره 4، اسفند 1396، صفحه 109-129    اصل مقاله (1.4 M)
نویسندگان
مهدی ملازاده گل محله* 1؛ محمد سبزی نژاد فراش2؛ روح اله رستاقی1
1دانشگاه امام حسین (ع)
2دکتری ریاضی رمز دانشگاه خوارزمی
تاریخ دریافت: 01 مرداد 1395،  تاریخ بازنگری: 06 اردیبهشت 1403،  تاریخ پذیرش: 28 شهریور 1397 
چکیده
در این مقاله، ساختار نسخه‌های مختلف پروتکل امنیتی تترا در "مدل صوری" و با استفاده از ابزارهای تحلیل خودکار پرووریف و اسکایتر مورد ارزیابی قرار می‌گیرند. پروتکل امنیتی شبکه تترا از نوع پروتکل‌های تبادل کلید تصدیق شده است که در آن، طرفین ضمن احراز هویت یکدیگر، یک کلید نشست نیز می‌سازند. این پروتکل همچنین از کلیدهای محرمانه از پیش توزیع شده استفاده می‌کند که مبتنی بر ساز و کارهای رمزنگاری متقارن است. تحلیل امنیتی پروتکل مذکور در "مدل صوری" و با استفاده از ابزارهای تحلیل خودکار پرووریف و اسکایتر انجام شده است. در ابتدا، هشت ویژگی امنیتی: محرمانگی، احراز هویت، امنیت پیشرو، امنیت کلید ناشناخته، کلید نشست یکسان، امنیت کلید معلوم، گمنامی و تمامیت را در بستر این ابزارها مدل‌سازی نموده و سپس با استفاده از هر دو ابزار، امنیت پروتکل مذکور را نسبت به این ویژگی‌ها مورد بررسی قرار می‌دهیم. مقایسه نتایج حاصل از تحلیل صوری این ویژگی‌ها با نتایج حاصله از تحلیل‌های غیرصوری در منابع آشکار دلالت بر وجود ضعف‌هایی جدید در ویژگی‌های "امنیت پیشرو" و "تمامیت" در ساختار این پروتکل دارد. در نهایت، روش-هایی برای غلبه بر این ضعف‌ها ارایه شده است.
کلیدواژه‌ها
تحلیل امنیتی؛ مدل های صوری؛ ابزار تحلیل خودکار؛ شبکه تترا
مراجع
  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,
  9. C. Cremers and S. Mauw, “Operational Semantics and Verification of Security Protocols,” Springer, 2012.
  10. C. Cremers, “The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols,” CAV 2008, LNCS, vol. 5123, pp. 414-418, 2008.
  11. S. Duan, “Security Analysis of TETRA,” Master thesis, Norwegian University of Science and Technology, 2013.
  12. Scyther,
  13. https://www.cs.ox.ac.uk/people/cas.cremers/scyther/index.html
  14. “ETSI Technical Standard ETSI EN 302 109 V1.1.1 Terrestrial Trunked Radio (TETRA),” Security
  15. Synchronization mechanism for end-to-end encryption, 2003.
  16. “TETRA Association SFPG Information document,” Overview of Standard TETRA Cryptographic Algorithms and
  17. their rules for management and distribution.
  18. ETSI Technical Report TR 052101 V1.1.1: SAGE Rules for the management of the TETRA standard authentication and key management algorithm set TAA1.
  19. ETSI Technical Report TR 1-0530101 V1.1.2: SAGE Rules for the management of the TETRA standard encryption algorithms Part1 TEA1.
  20. ETSI Technical Standard ETSI EN 300 392-7 V2.1.1: Terrestrial Trunked Radio (TETRA), Voice plus Data( V+D), Part 7: Security.
آمار
تعداد مشاهده مقاله: 979
تعداد دریافت فایل اصل مقاله: 373