Cryptology Academy · درس

Tamarin والبراهين الحسابية

استخدم مُبرهن Tamarin لإعادة الكتابة متعددة المجموعات والتحقق القائم على التتبّع

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

ما هو Tamarin؟

Tamarin (ETH Zurich, 2012) هو أداة للتحقق من بروتوكولات الأمان، تعتمد على إعادة كتابة المجموعات المتعددة. وعلى خلاف نهج ProVerif القائم على بنود هورن، يستدل Tamarin بشأن مسارات تنفيذ البروتوكول باستخدام مُثبِت تفاعلي.

Tamarin مقابل ProVerif

ProVerif: آلي بالكامل، وقد يعطي نتيجة "cannot be proved". Tamarin: مساعد إثبات تفاعلي + وضع آلي، ويتعامل مع النظريات المعادلية (XOR وDiffie-Hellman والخرائط الثنائية الخطية). وهو أكثر تعبيرًا، لكن منحنى تعلمه أشد.

قواعد إعادة كتابة المجموعات المتعددة

ينمذج Tamarin البروتوكولات على هيئة قواعد إعادة كتابة تعمل على الحقائق. وتمثل الحقائق الحالة. وتستهلك القاعدة [ L ] --[ A ]-> [ R ] الحقائق اليسرى L، وتنتج الحقائق اليمنى R، وتسجل الإجراء A في مسار التنفيذ.

لغة إدخال Tamarin ‏(.spthy)

يعرّف ملف نظرية Tamarin الدوال والمعادلات والقواعد واللمم:

/* Diffie-Hellman key exchange */
builtins: diffie-hellman

rule Alice_1:
  [ Fr(~a) ]  /* fresh random a */
  --[ AliceSent($A, $B, 'g'^~a) ]->
  [ Alice_St($A, $B, ~a), Out('g'^~a) ]

rule Bob_1:
  [ In(ga), Fr(~b) ]
  --[ BobReceived($A, $B, ga) ]->
  [ Bob_St($A, $B, ~b, ga^~b), Out('g'^~b) ]

صياغة اللمم

تُصاغ أهداف الأمان في صورة لمم على مسارات التنفيذ:

/* Secrecy: shared secret not known to attacker */
lemma secret_key:
  "All A B k #i #j.
    AliceKey(A, B, k) @ i &
    BobKey(A, B, k) @ j
    ==> not (Ex #r. K(k) @ r)"

/* Authentication: if Bob has key, Alice sent it */
lemma authentication:
  "All A B k #j. BobKey(A, B, k) @ j
    ==> Ex #i. AliceKey(A, B, k) @ i & i < j"

تشغيل Tamarin

شغّل واجهة Tamarin الرسومية التفاعلية: tamarin-prover interactive my_protocol.spthy. تعرض واجهة المتصفح التزامات الإثبات؛ ويمكنكم توجيه الاستراتيجيات الآلية أو تطبيق خطوات يدوية في الحالات التي لا تنتهي.

السلامة الحسابية

تضمن البراهين الرمزية (ProVerif وTamarin) الأمان في ظل افتراضات التشفير المثالي. وترفع مبرهنات السلامة الحسابية (Cortier, Backes) البراهين الرمزية إلى مستوى الأمان الحسابي عند تطبيقها باستخدام بدائيات ثبت أمانها.

F* وHACL*: تطبيقات متحقق منها

F* (Microsoft Research) هي لغة برمجة موجّهة نحو البرهان. أما HACL* فهي مكتبة تشفير مكتوبة بلغة F*، وتحتوي على براهين متحقق منها آليًا للصحة ومقاومة القنوات الجانبية. وتُستخدم في Firefox NSS وmbedTLS.

EasyCrypt: براهين حسابية قائمة على الألعاب

يتيح EasyCrypt براهين أمان حسابية بالكامل (قائمة على الألعاب) للإنشاءات التشفيرية، وليس للبروتوكولات فقط. وقد جرى التحقق من طبقة السجلات في TLS 1.3 ومن ChaCha20-Poly1305 باستخدام EasyCrypt.

الأثر العملي

بدأ التشفير المتحقق منه رسميًا يدخل بيئات الإنتاج: يستخدم NSS (Firefox) مكتبة HACL*، وتستخدم AWS ‏s2n-tls مع تأكيدات حاملة للبراهين، كما جرى التحقق من بروتوكول Signal باستخدام ProVerif وTamarin. ولم تعد الأساليب الشكلية مقتصرة على المجال الأكاديمي.

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

كيف يختلف Tamarin عن ProVerif في التعامل مع الحالات التي تفشل فيها الأتمتة؟

مراجعة الدرس

يستخدم Tamarin إعادة كتابة المجموعات المتعددة والاستدلال القائم على مسارات التنفيذ، مع واجهة رسومية تفاعلية للإثبات. ويتعامل مع النظريات المعادلية لـ DH وXOR. وتعبّر اللمم عن أهداف السرية والمصادقة. وتربط السلامة الحسابية بين البراهين الرمزية والأمان الفعلي. وتمتد عملية التحقق إلى التطبيقات والإنشاءات بفضل HACL* وEasyCrypt.

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

هل درس «Tamarin والبراهين الحسابية» مجاني؟

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

ماذا ستتعلم في «Tamarin والبراهين الحسابية»؟

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

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

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

كم من الوقت يستغرق درس «Tamarin والبراهين الحسابية»؟

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

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

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

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

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