Cryptology Academy · درس

ProVerif: التحقق الآلي من البروتوكولات

حدّد خصائص مصافحة TLS وتحقّق منها باستخدام ProVerif

الدرس 3 من 412 خطوة

ProVerif: التحقق الآلي من البروتوكولات درس مجاني في Cryptology Academy على CoddyKit. هذا هو الدرس 3 من أصل 4. يمكنك قراءة الدرس كاملاً أدناه مجاناً — ثم تمرن عليه مباشرة في المتصفح باستخدام محرر أكواد مدمج ومدرس ذكاء اصطناعي متاح 24/7. هذا الدرس جزء من مسار التعلم في Cryptology Academy، وتقدمك يتزامن عبر الويب وتطبيق CoddyKit. تتضمن دورة Cryptology Academy 4 دروس في المجموع.

ما هو ProVerif؟

ProVerif (Bruno Blanchet, 2001) هو أداة آلية للتحقق من بروتوكولات التشفير. يأخذ بروتوكولًا موصوفًا بحساب π التطبيقي ويقرر آليًا خصائص السرية والمصادقة.

كيف يعمل ProVerif

يحوّل ProVerif البروتوكول إلى بنود هورن ويطبّق خوارزمية قائمة على الاستدلال بالحل لاشتقاق ما يمكن للمهاجم معرفته. إذا أمكن اشتقاق حقيقة تتعلق بالسرية، فهذا يعني أن البروتوكول مخترق؛ وإلا فقد ثبت أمانه.

لغة إدخال ProVerif

تُوصَف البروتوكولات بصورة تصريحية: تعريف القنوات والأنواع والدوال (enc, dec, sign, verify)، والمعادلات (dec(enc(m,k),k)=m)، والعمليات التي تتواصل عبر القنوات.

تعريف البدائيات التشفيرية

مثال على تعريفات ProVerif:

(* Symmetric encryption *)
fun senc(bitstring, key): bitstring.
fun sdec(bitstring, key): bitstring.
equation forall m: bitstring, k: key; sdec(senc(m, k), k) = m.

(* Asymmetric encryption *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring.
equation forall m: bitstring, sk: skey; adec(aenc(m, pk(sk)), sk) = m.

كتابة عملية بروتوكول بسيطة

نمذِج Alice وBob كعمليتين متوازيتين:

(* Alice sends nonce to Bob, encrypted *)
let Alice(skA: skey, pkB: pkey) =
  new na: nonce;
  out(c, aenc((na, pk(skA)), pkB));
  in(c, m: bitstring);
  let nb = adec(m, skA) in
  out(c, aenc(nb, pkB)).

(* Main process: run attacker with full channel control *)
process
  new skA: skey; new skB: skey;
  out(c, pk(skA)); out(c, pk(skB));  (* publish public keys *)
  (Alice(skA, pk(skB)) | Bob(skB, pk(skA)))

صياغة استعلامات الأمان

يتحقق ProVerif من استعلامات مثل:

(* Secrecy: attacker cannot learn na *)
query attacker(na).

(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).

تفسير مخرجات ProVerif

يُخرج ProVerif العبارة "RESULT ... is true" (أي ثبت الأمان)، أو العبارة "RESULT ... is false" ويطبع مسار هجوم مضادًا يوضح رسائل المهاجم. ويوضح المسار بدقة كيفية تنفيذ الهجوم.

التحقق من TLS 1.3 باستخدام ProVerif

استخدم Bhargavan et al. (2016) أداة ProVerif لتحليل نموذج من TLS 1.3. وقد عثروا على هجوم على آلية استئناف 0-RTT وأبلغوا عنه، ثم أُصلح قبل اعتماد RFC بصيغته النهائية.

الحدود: التقريب والحلقات

يستخدم ProVerif تقريبًا علويًا: فقد يبلغ عن هجمات زائفة (أي يقول "false" مع أن البروتوكول آمن فعليًا)، لكنه لا يفوّت أي هجوم حقيقي. وقد لا تنتهي جلسات البروتوكول غير المحدودة؛ إذ يفك ProVerif الحلقات بطريقة استرشادية.

عندما يقول ProVerif «لا يمكن إثباته»

إذا لم يتمكن ProVerif من تحديد النتيجة ضمن تقريبه، فإنه يُخرج العبارة "CANNOT BE PROVED." وهذا لا يثبت انعدام الأمان، بل يعني أن الأداة استنفدت قدرتها الاسترشادية. وقد ينجح Tamarin في هذه الحالات.

اختبار المعرفة

ماذا تعني مخرجات ProVerif "RESULT ... is false" بالنسبة إلى استعلام عن السرية؟

أجب عليها في الدرس التفاعلي

مراجعة الدرس

يؤتمت ProVerif التحقق من البروتوكولات باستخدام الاستدلال ببنود هورن. وتُكتب البروتوكولات بحساب π التطبيقي مع معادلات تشفيرية. وتسأل الاستعلامات عن السرية والمصادقة. تعني false إثبات الأمان؛ وتعني true الاختراق (مع مسار هجوم). ومن حدوده أن التقريبات قد تؤدي إلى نتيجة «لا يمكن إثباته».

البدء مجانًا

تعلم Cryptology Academy مع معلم ذكاء اصطناعي — مجانًا

اكتب وقم بتشغيل أكوادك الفعلية في المتصفح، واحصل على مساعدة فورية من معلم ذكاء اصطناعي متاح 24/7، واستمر من حيث توقفت على الويب أو في التطبيق.

الدورات: 67
الدروس: 261

ابدأ التعلم مجانًا عرض الدورة الكاملة

الأسئلة الشائعة

هل درس «ProVerif: التحقق الآلي من البروتوكولات» مجاني؟

نعم — نص درس «ProVerif: التحقق الآلي من البروتوكولات» كامل متاح مجاناً هنا على الويب. لتمرينه بشكل تفاعلي (محرر أكواد مدمج ومدرس ذكاء اصطناعي متاح 24/7) وفتح باقي دورة Cryptology Academy، انتقل إلى CoddyKit PRO. تتضمن دورة Cryptology Academy 4 دروس في المجموع.

ماذا ستتعلم في «ProVerif: التحقق الآلي من البروتوكولات»؟

حدّد خصائص مصافحة TLS وتحقّق منها باستخدام ProVerif تتمرن على Cryptology Academy مع أكواد عملية تشغلها مباشرة في المتصفح، ومدرس ذكاء اصطناعي متاح 24/7 يجيب على أسئلتك أثناء عملك.

هل أحتاج إلى خبرة سابقة لأبدأ Cryptology Academy؟

لا تُشترط خبرة سابقة. Cryptology Academy على CoddyKit منظم للمبتدئين حتى المتقدمين، لذا يمكنك البدء من هنا أو من البداية والتقدم بسرعتك الخاصة. هذا هو الدرس 3 من أصل 4.

كم من الوقت يستغرق درس «ProVerif: التحقق الآلي من البروتوكولات»؟

معظم دروس CoddyKit تستغرق حوالي 5–10 دقائق. كل منها موجز وتفاعلي، لذا تحرز تقدماً مستمراً وتستأنف من حيث توقفت عبر الويب والتطبيق.

هل يمكنني كتابة وتشغيل أكواد في درس Cryptology Academy هذا؟

نعم. كل درس في Cryptology Academy يتضمن محرر أكواد مدمج، لذا تكتب وتشغل أكواداً حقيقية مباشرة في متصفحك وتحصل على تعليقات فورية من الذكاء الاصطناعي — بدون إعداد محلي.

جميع الدروس في هذه الدورة

← العودة إلى Cryptology Academy