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

توجد العديد من الطرق الرسمية المعتمدة 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.