ترغب بنشر مسار تعليمي؟ اضغط هنا

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

Verification of Security Protocols Using Formal Methods

1254   0   132   0 ( 0 )
 تاريخ النشر 2017
والبحث باللغة العربية
 تمت اﻹضافة من قبل Shamra Editor




اسأل ChatGPT حول البحث

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

المراجع المستخدمة
ALSHEHRI, A. A. NFC mobile coupon protocols: developing, formal security modelling and analysis, and addressing relay attack (Doctoral dissertation, University of Surrey). (2015)
BIONDI, F., & LEGAY, A. Security and Privacy of Protocols and Software with Formal Methods. In International Symposium on Leveraging Applications of Formal Methods (pp. 883-892). Springer International Publishing. (2016)
BLANCHET, B., SMYTH, B., & CHEVAL, V. (2015). ProVerif 1.90: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial. URL: http://prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf online last accessed on 22-7-2016
قيم البحث

اقرأ أيضاً

يقترح البحث طريقة جديدة تهدف إلى التحقق من صورة التوقيع اليدوي لشخص ما، و تحديد فيما إذا كان التوقيع يعود لهذا الشخص أو أنه توقيع مزور. و تم ذلك بالاعتماد على استخلاص سمات هندسية من صورة التوقيع الموجودة في قاعدة البيانات و إجراء عمليات إحصائية رياضي ة عليها كطريقة للتحقق من توقيع هذا الشخص. تم استخلاص السمات من صورة التوقيع على مراحل متعددة حيث تم تحويل صورة التوقيع من الصيغة الرمادية إلى الصيغة الثنائية ثم استخلاص الخصائص الإحصائية للتوقيع الأصلي و هي القيم الأكبر بين القيم الأكثر تكراراً في إحداثيات الواحدات التي تحدد شكل التوقيع، بالإضافة لعدد الواحدات التي تحدد شكل التوقيع، ثم تم تحديد مجالين للقيم المقبولة للتوقيع الأصلي. و بنفس الاسلوب و يتم استخلاص السمات الإحصائية للتواقيع المزورة و اختبارها إذا كانت تنتمي إلى مجال القيم المقبولة المحدد. كما يتضمن البحث مقارنة لنتائج الطريقة المقترحة مع الطرق السابقة في هذا المجال. تم اختبار الطريقة المقترحة باستخدام قاعدة البيانات مكونة من 16200 توقيع موزعة على 300 شخص، و كنتيجة لذلك تم التحقق بنسبة جيدة من صورة التوقيع اليدوي.
نقدم طريقة عامة لحساب الدقة الملحة لتخفيف البيانات الناتجة عن الحد الأدنى من جهود المستخدم.نحن ننظر إلى Prob-Lem كهامة لفحص الحقائق للتحقق من مطالبات NU-Merical في النص.يفترض التحقق من Gorithm أن البيانات المستخدمة في الحصول على النص متاح.في هذه الور قة، نقوم بفاية استخدام الحل المقترح قد استخدمه هذه المطالبات غير الصحيحة حول ملخصات كرة السلة TEX-Tual في سياق مهمة بدقة في INLG 2021.
في هذه الورقة، نقترح نظام التحقق والتحقق من حقائق جديدة للتحقق من مطالبات محتوى ويكيبيديا.يسترد نظامنا صفحات ويكيبيديا ذات الصلة باستخدام Anserini، ويستخدم نموذج الإجابة على السؤال من Bert-Bert-bert-Berted لتحديد الأدلة الصحيحة، وتحقق من المطالبات با ستخدام نموذج الاستدلال باللغة الطبيعية XLNet بمقارنتها بالأدلة.يتم الحصول على أدلة خلية الجدول من خلال البحث عن قيم الخلايا المطابقة للكيان وسؤال الجدول Tapas نموذج الرد على نموذج.يستخدم خط الأنابيب إمكانيات الطلقة الصفرية للنماذج الحالية وجميع النماذج المستخدمة في خط الأنابيب لا يتطلب أي تدريب إضافي.حصل نظامنا على درجة حمامة من 0.06 ودقة ملصقة تبلغ 0.39 في التحدي الحمير.
يصف هذا العمل تكيف نموذج تسلسل متطلب مسبقا بمهمة التحقق من المطالبة العلمية في المجال الطبي الطبيعي.نقترح نظام يسمى Vert5erini الذي يستغل T5 لاسترجاع الملخص واختيار الجملة وتنبؤ التسمية، وهي ثلاثة مهام فرعية حرجة للتحقق من الادعاء.نقوم بتقييم خط أناب يبنا في SCIFACT، وهي مجموعة بيانات مفيدة حديثا تتطلب نماذج لا تتوقع فقط عن صحة المطالبات ولكنها توفر أيضا جمل ذات صلة من كائن من الأدبيات العلمية التي تدعم التنبؤ.تجريبيا، يتفوق نظامنا على خط أساس قوي في كل من المهام الفرعية الثلاث.نعرض أيضا قدرة Vert5erini على التعميم لمجموعات بيانات جديدة من مطالبات CovID-19 باستخدام أدلة من Cord-19 Corpus.
نقدم DataSet، Danfever، مخصص للبحث عن المعلومات الخاطئة متعددة اللغات.DataSet باللغة الدنماركية ولها نفس التنسيق مثل مجموعة بيانات الحمى الإنجليزية المعروفة.يمكن استخدامه للاختبار طرق في إعدادات متعددة اللغات، وكذلك لإنشاء الطرز في الإنتاج للغة الدنماركية.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا