توجد العديد من الطرق الرسمية المعتمدة 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
Artificial intelligence review:
Research summary
تستعرض هذه الدراسة الطرق الرسمية المستخدمة للتحقق من البروتوكولات الأمنية، مع التركيز على أربع أدوات رئيسية: AVISPA، Casper، ProVerif، وScyther. تهدف الدراسة إلى مقارنة هذه الأدوات من حيث أسلوب العمل، لغة البرمجة، واجهة المستخدم، أسلوب الإدخال، وطريقة إظهار النتائج. تم اختبار ستة بروتوكولات أمنية مختلفة باستخدام هذه الأدوات، وهي: بروتوكول التحقق Kao Chow، بروتوكول 3-D الآمن، بروتوكول Needham-Schroeder للمفتاح العمومي، بروتوكول تبادل المفاتيح Diffie-Hellman، بروتوكول Andrew Secure RPC، وبروتوكول مصادقة مصافحة التحدي. أظهرت النتائج أن بعض البروتوكولات غير آمنة بينما كانت الأخرى آمنة. توصلت الدراسة إلى أن أداة Casper هي الأفضل من حيث الأمان، تليها AVISPA. توصي الدراسة باستخدام طرق متعددة لاختبار البروتوكولات لضمان الأمان الكامل.
Critical review
دراسة نقدية: على الرغم من أن الدراسة تقدم مقارنة شاملة بين الأدوات الأربعة، إلا أنها قد تكون محدودة من حيث عدد البروتوكولات المختبرة. يمكن أن تكون النتائج أكثر شمولية إذا تم اختبار عدد أكبر من البروتوكولات. بالإضافة إلى ذلك، قد يكون من المفيد تضمين أدوات أخرى للتحقق من البروتوكولات الأمنية للحصول على صورة أكثر شمولية. كما أن الدراسة لم تتطرق بشكل كافٍ إلى كيفية تحسين الأدوات الحالية أو تطوير أدوات جديدة بناءً على النتائج المستخلصة.
Questions related to the research
-
ما هي الأدوات الأربعة التي تم استخدامها في الدراسة للتحقق من البروتوكولات الأمنية؟
الأدوات الأربعة هي AVISPA، Casper، ProVerif، وScyther.
-
ما هي البروتوكولات الأمنية التي تم اختبارها في الدراسة؟
تم اختبار بروتوكول التحقق Kao Chow، بروتوكول 3-D الآمن، بروتوكول Needham-Schroeder للمفتاح العمومي، بروتوكول تبادل المفاتيح Diffie-Hellman، بروتوكول Andrew Secure RPC، وبروتوكول مصادقة مصافحة التحدي.
-
ما هي الأداة التي اعتبرتها الدراسة الأفضل من حيث الأمان؟
اعتبرت الدراسة أن أداة Casper هي الأفضل من حيث الأمان.
-
ما هي التوصية الرئيسية التي قدمتها الدراسة لضمان أمان البروتوكولات؟
توصي الدراسة باستخدام طرق متعددة لاختبار البروتوكولات لضمان الأمان الكامل.
References used
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
This research suggests a new method that aims to verify the manual signature image which is written by person, and specify whether this signature back to this person or that forged signature. This was done by extracting geometric features of the sign
We present a generic method to compute thefactual accuracy of a generated data summarywith minimal user effort. We look at the prob-lem as a fact-checking task to verify the nu-merical claims in the text. The verification al-gorithm assumes that the
In this paper, we propose a novel fact checking and verification system to check claims against Wikipedia content. Our system retrieves relevant Wikipedia pages using Anserini, uses BERT-large-cased question answering model to select correct evidence
This work describes the adaptation of a pretrained sequence-to-sequence model to the task of scientific claim verification in the biomedical domain. We propose a system called VerT5erini that exploits T5 for abstract retrieval, sentence selection, an
We present a dataset, DanFEVER, intended for multilingual misinformation research. The dataset is in Danish and has the same format as the well-known English FEVER dataset. It can be used for testing methods in multilingual settings, as well as for creating models in production for the Danish language.