عناصر مشابهة
Toward Proving the Correctness Conditions of the Three-Way Handshake Protocol Using Temporal Logic
| العنوان بلغة أخرى: | إثبات شروط الصحة لبروتكول المصافحة الثلاثية باستخدام المنطق المؤقت |
|---|---|
| الناشر: |
إربد
|
| المؤلف الرئيسي: | |
| مؤلفين آخرين: | |
| التاريخ الميلادي: | 2020 |
| الصفحات: | 1 - 115 |
| رقم MD: | 1125371 |
| نوع المحتوى: | رسائل جامعية |
| اللغة: | English |
| قواعد المعلومات: | Dissertations |
| الدرجة العلمية: | رسالة ماجستير |
| الجامعة: | جامعة اليرموك |
| الكلية: | كلية تكنولوجيا المعلومات وعلوم الحاسوب |
| مواضيع: | |
| رابط المحتوى: |
| المستخلص: | بروتوكول المصافحة الثلاثة يستخدم على نطاق واسع وخاصة كجزء من أنظمة الاتصالات والأمن المعقدة. يتم استخدام هذا البروتكول لإنشاء اتصال بين عميل (الجهاز الذي يطلب الاتصال) وخادم معين (الجهاز الذي يوفر الاتصال) تحت قواعد وقيود معينة. في هذا البحث سنستخدم تقنيات فحص النماذج الآلية والمنطق المؤقت للتحقق من صحة بروتوكول المصافحة الثلاثية تحت شروط وخصائص صحة معينة. تم نمذجة بروتوكول المصافحة الثلاثية وتحويلة إلى نموذج الحالة المحدودة باستخدام فاحص النماذج، وتم برمجة وتحويل شروط الصحة إلى صيغ مكتوبة بمنطق الشجرة الحسابية وبالتالي سيقوم فاحص النماذج بالتحقق تلقائيا من صحة نموذج الحالة المحدودة وتفسيره عبر شروط الصحة للتحقق مما إذا كان البروتوكل يحقق هذه الشروط أو إنه غير قادر على تحقيقها. أظهرت نتائج التحقق أن بروتكول المصافحة الثلاثة قد استوفى كل شروط الصحة باستثناء شروط الصحة 9، 11، 12، لذلك أنتج فاحص النماذج أمثلة مضادة أظهرت الأخطاء الموجودة في البرتكول. يهدف نهج التحقق الآلي المقترح إلى إثبات صحة عدد محدود من العملاء كل منهم يطلب الخادم لتزويده بالاتصال بشكل لانهائي. |
|---|
