التحقق من البروتوكولات الأمنية باستخدام الطرق الرسمية

الملخص

توجد العديد من الطرق الرسمية المعتمدة Formal Methods لاختبار البروتوكولات الأمنية وكشف كونها آمنة أم لا. أهمها: أفيسبا Avispa، كاسبر Casper، بروفيرف ProVerif، سايثر Scyther. لقد تم التطرق سابقاً إلى تنفيذ مقارنات باستخدام طريقتين فقط من الطرق المذكورة (ProVerif, Scyther).

تم في هذا البحث التحقق من البروتوكولات الأمنية والقيام بتنفيذ مقارنة بين الطرق الأربعة المذكورة من حيث نفسها البارامترات التي استخدمت في تنفيذ المقارنة بين الطريقتين سابقاً: أسلوب العمل، لغة البرمجة المستخدمة، واجهة المستخدم، أسلوب الإدخال، وطريقة إظهار النتائج. وتقديم خيارات للمستخدم باختيار الطريقة المناسبة حسب البارامتر المطلوب.

تم تنفيذ الاختبار على ستة من البروتوكولات الأمنية المختلفة وهي: بروتوكول التحقق كاو شاو Kao Chow Authentication Protocol، بروتوكول 3-د الآمن 3-D Secure، بروتوكول ندهام-شرودر للمفتاح العمومي Needham-Schroeder Public Key Protocol، بروتوكول تبادل المفاتيح دفي-هلمان Diffie–Hellman key exchange، - بروتوكول اندرو سكيور Andrew Secure RPC Protocol، وبروتوكول مصادقة مصافحة التحدي Challenge Handshake Authentication Protocol.

There are many of Formal Methods for testing security protocols detecting being safe or not. Including Avispa, Casper, ProVerif, Scyther. Previously a comparisons using two of mentioned methods (ProVerif, Scyther).

In this, research a comparison between the four mentioned methods in terms of the same used parameters in the previous comparison: working style, the modeling language, user interface, input, and output. As a result, the user provided with options to choose the appropriate method depending on the desired parameter.

Six different of security protocols have been tested and finally the results have been compared; these protocols are Kao Chow Authentication Protocol, 3-D Secure Protocol, Needham-Schroeder Public Key Protocol, Diffie–Hellman key exchange, Andrew Secure RPC Protocol, and Challenge Handshake Authentication Protocol