ارسل ملاحظاتك

ارسل ملاحظاتك لنا







Toward Proving the Correctness Conditions of the Three-Way Handshake Protocol Using Temporal Logic

العنوان بلغة أخرى: إثبات شروط الصحة لبروتكول المصافحة الثلاثية باستخدام المنطق المؤقت
المؤلف الرئيسي: العمري، أحمد محمود محمد (مؤلف)
مؤلفين آخرين: الشرمان، رأفت موسى (مشرف)
التاريخ الميلادي: 2020
موقع: إربد
الصفحات: 1 - 115
رقم MD: 1125371
نوع المحتوى: رسائل جامعية
اللغة: الإنجليزية
الدرجة العلمية: رسالة ماجستير
الجامعة: جامعة اليرموك
الكلية: كلية تكنولوجيا المعلومات وعلوم الحاسوب
الدولة: الاردن
قواعد المعلومات: Dissertations
مواضيع:
رابط المحتوى:
صورة الغلاف QR قانون
حفظ في:
المستخلص: بروتوكول المصافحة الثلاثة يستخدم على نطاق واسع وخاصة كجزء من أنظمة الاتصالات والأمن المعقدة. يتم استخدام هذا البروتكول لإنشاء اتصال بين عميل (الجهاز الذي يطلب الاتصال) وخادم معين (الجهاز الذي يوفر الاتصال) تحت قواعد وقيود معينة. في هذا البحث سنستخدم تقنيات فحص النماذج الآلية والمنطق المؤقت للتحقق من صحة بروتوكول المصافحة الثلاثية تحت شروط وخصائص صحة معينة. تم نمذجة بروتوكول المصافحة الثلاثية وتحويلة إلى نموذج الحالة المحدودة باستخدام فاحص النماذج، وتم برمجة وتحويل شروط الصحة إلى صيغ مكتوبة بمنطق الشجرة الحسابية وبالتالي سيقوم فاحص النماذج بالتحقق تلقائيا من صحة نموذج الحالة المحدودة وتفسيره عبر شروط الصحة للتحقق مما إذا كان البروتوكل يحقق هذه الشروط أو إنه غير قادر على تحقيقها. أظهرت نتائج التحقق أن بروتكول المصافحة الثلاثة قد استوفى كل شروط الصحة باستثناء شروط الصحة 9، 11، 12، لذلك أنتج فاحص النماذج أمثلة مضادة أظهرت الأخطاء الموجودة في البرتكول. يهدف نهج التحقق الآلي المقترح إلى إثبات صحة عدد محدود من العملاء كل منهم يطلب الخادم لتزويده بالاتصال بشكل لانهائي.

عناصر مشابهة