لماذا لا تكفي البراهين غير الرسمية

يقدّم مصممو البروتوكولات بانتظام حججًا غير رسمية حول الأمان — وهي استدلالات نثرية تشرح سبب عجز المهاجم عن النجاح. ويُظهر التاريخ أن هذه الحجج تكون خاطئة في كثير من الأحيان، حتى في البروتوكولات التي صممها خبراء.

صُمم Needham-Schroeder عام 1978 للمصادقة المتبادلة. وفي عام 1995، اكتشف Gavin Lowe هجوم رجل في الوسط باستخدام التحقق الآلي — أي بعد 17 عامًا من النشر. فقد أغفل البرهان غير الرسمي إعادة تشغيل دقيقة.

اعتمد IEEE بروتوكول WEP عام 1997 مع ادعاءات أمان غير رسمية. وبحلول عام 2001، اكتشف الباحثون إعادة استخدام دفق مفاتيح RC4، وتصادمات IV، وغياب السلامة — ما أدى إلى كسره خلال دقائق. ولم يستطع الاستدلال غير الرسمي اكتشاف أي من ذلك.

يعتمد أمان البروتوكولات على التفاعلات بين جلسات متزامنة عديدة، ومهاجمين نشطين، وافتراضات تشفيرية. ويواجه الاستدلال البشري صعوبة في التعامل مع انفجار الحالات والتنفيذات المتزامنة المتداخلة.

تنمذج الأساليب الشكلية البروتوكول رياضيًا، وتثبت — أو تدحض — خصائص الأمان (السرية والمصادقة والسرية الأمامية) لجميع استراتيجيات المهاجم الممكنة، لا لتلك التي أخذها المصمم في الحسبان فقط.

الرمزية (Dolev-Yao): التشفير صندوق أسود مثالي؛ والتركيز على منطق البروتوكول. الحسابية: ألعاب أمان احتمالية فعلية؛ وهي أقرب إلى الضمانات الواقعية. ويكشف كلاهما أخطاء حقيقية.

استغلت POODLE (عام 2014) قناةً جانبيةً تعتمد على الحشو في CBC الخاص بـ SSL 3.0. وكانت الثغرة عيبًا في تصميم البروتوكول على مستوى البروتوكول، وليست خطأً في التنفيذ. وكان من شأن التحليل الشكلي لمواصفات SSL 3.0 أن يكشف هذه القناة قبل النشر.

صُمم TLS 1.3 ‏(RFC 8446) بالتزامن مع تحليلات شكلية باستخدام ProVerif وmiTLS. وجرى تكرار المواصفات استنادًا إلى النتائج الشكلية — في محطة بارزة لاعتماد الهيئات المعنية بالمعايير للأساليب الشكلية.

تتحقق الأدوات الشكلية من نموذج البروتوكول، لا من التنفيذ. لذلك قد يظل البروتوكول المتحقق منه شكليًا ذا تنفيذ غير آمن. وتمتد F* / HACL* بالتحقق ليشمل الشيفرة التشفيرية نفسها.

التحقق الشكلي مكلف: إذ تستغرق نمذجة البروتوكول أسابيع وتتطلب خبرة متخصصة. لكن التكلفة مبررة في الأهداف عالية القيمة (TLS وSSH وSignal) — فقد يؤثر عيب واحد في البروتوكول في مليارات المستخدمين.

ما الذي جعل اكتشاف Lowe عام 1995 لهجوم Needham-Schroeder مهمًا؟

تفشل البراهين غير الرسمية لأن الاستدلال البشري يغفل التفاعلات بين الجلسات المتزامنة واستراتيجيات المهاجمين. احتوت Needham-Schroeder وWEP وPOODLE جميعًا على حجج أمان غير رسمية. وأُدرج التحليل الشكلي في تصميم TLS 1.3. وتكشف الأدوات الشكلية الأخطاء على مستوى البروتوكول قبل النشر.