بروتوكول Needham-Schroeder وهجماته

كان بروتوكول Needham-Schroeder ‏(1978) من أوائل المحاولات الرسمية لتصميم بروتوكول مصادقة تشفيري باستخدام طرف ثالث موثوق (TTP). وكان الهدف هو تمكين طرفين، Alice وBob، من مصادقة كل منهما الآخر وإنشاء مفتاح جلسة مشترك باستخدام خادم مصادقة موثوق (AS) يتشارك مفاتيح طويلة الأجل مع كل طرف. وقد سبق البروتوكول البنية التحتية للمفاتيح العامة، لكنه قدم مفاهيم، مثل القيم العشوائية لمرة واحدة لضمان الحداثة وتوزيع المفاتيح عبر خادم موثوق، لا تزال محورية في بروتوكولات حديثة مثل Kerberos. وقد أسهم فهم بروتوكول NS وإخفاقاته في تشكيل مجال تحليل البروتوكولات بأكمله.

يتكون بروتوكول NS للمفتاح المتماثل من خمس خطوات. (1) يرسل Alice ‏{A, B, Na} إلى AS، طالبًا مفتاح جلسة للتواصل مع Bob. (2) يرد AS على Alice بالرسالة ‏{Na, B, Kab, {Kab, A}_Kb}_Ka، التي تتضمن مفتاح الجلسة Kab وتذكرة إلى Bob، وكلها مشفَّرة باستخدام مفتاح Alice طويل الأجل Ka. (3) يمرر Alice التذكرة ‏{Kab, A}_Kb إلى Bob. (4) يفك Bob تشفير التذكرة، ويستخرج Kab، ويرسل ‏{Nb}_Kab إلى Alice (وهو تحدٍّ). (5) ترد Alice بالرسالة ‏{Nb-1}_Kab، لتثبت أنها تملك Kab. وتمنع القيمة العشوائية لمرة واحدة Nb إعادة تشغيل الخطوة 4. ويعاني هذا البروتوكول من هجوم إعادة تشغيل معروف استغله Denning وSacco عام 1981.

اكتشف Denning وSacco عام 1981 خللًا يتمثل في أن استجابة AS في الخطوة 2 ليست حديثة؛ إذ لا تتضمن طابعًا زمنيًا أو قيمة عشوائية لمرة واحدة صادرة عن الخادم. يستطيع مهاجم يُدعى Mallory، سبق أن اعترض مفتاح جلسة قديمًا Kab (بعد اختراق جلسة سابقة)، إعادة تشغيل التذكرة القديمة ‏{Kab, A}_Kb مع Bob في أي وقت لاحق. وعندما يتلقى Bob ما يبدو أنه تذكرة شرعية من Alice، يستخدم المفتاح المخترق Kab للجلسة. وكان إصلاح Denning وSacco هو إضافة طابع زمني إلى استجابة AS والتذكرة. وقد اعتُمد هذا الإصلاح في Kerberos، حيث تُضمَّن الطوابع الزمنية في التذاكر للحد من فترة صلاحيتها.

صُمم بروتوكول NS للمفتاح العام (أيضًا عام 1978) للمصادقة المتبادلة بين طرفين باستخدام تشفير المفتاح العام. (1) يرسل Alice ‏{Na, A}_PKb إلى Bob (حيث تُشفَّر القيمة العشوائية لمرة واحدة Na باستخدام المفتاح العام لـ Bob). (2) يرد Bob بالرسالة ‏{Na, Nb}_PKa (القيمتان العشوائيتان، مشفرتان باستخدام المفتاح العام لـ Alice). (3) ترد Alice بالرسالة ‏{Nb}_PKb (إذ تعيد إرسال قيمة Bob العشوائية مشفَّرة باستخدام مفتاحه العام). بعد هذه المراسلة، يملك الطرفان القيمتين العشوائيتين Na وNb، ويمكنهما اشتقاق مفتاح جلسة. وقد بدا البروتوكول آمنًا لمدة 17 عامًا، إلى أن ظهر هجوم Lowe عام 1995.

اكتشف Gavin Lowe عام 1995 خللًا خطيرًا باستخدام أداة فحص النماذج Failures in Compositional Reasoning ‏(FDR). يستطيع Mallory انتحال شخصية Bob أمام Alice، مع تمرير الرسائل إلى Bob صادق. الخطوة 1: ترسل Alice ‏{Na, A}_PKm إلى Mallory (ظنًا منها أنها تتحدث إلى Bob). ويمرر Mallory ‏{Na, A}_PKb إلى Bob. الخطوة 2: يرد Bob بالرسالة ‏{Na, Nb}_PKa، فيفك Mallory تشفيرها ويعيد تشفيرها إلى Alice: ‏{Na, Nb}_PKa. تفك Alice التشفير وتستخرج Nb. الخطوة 3: ترسل Alice ‏{Nb}_PKm (ظنًا منها أن الرسالة تصل إلى Bob). ويفك Mallory تشفيرها ويمرر ‏{Nb}_PKb إلى Bob. ويعتقد Bob أنه أكمل مصادقة متبادلة مع Alice، لكن Alice في الواقع تصادق Mallory. ويكمن الإصلاح في أن يضمّن Bob هويته في الخطوة 2: ‏{Na, Nb, B}_PKa.

إصلاح Lowe لبروتوكول NSPK بسيط لكنه عميق: يجب أن يتضمن رد Bob في الخطوة 2 هوية Bob ‏B، بحيث يصبح {Na, Nb, B}_PKa. الآن، عندما تتلقى Alice الرد، تتحقق من أن الهوية المضمّنة ‏B تطابق الطرف الذي قصدت الاتصال به. لا يستطيع Mallory استبدال رده — إذ سيحتاج Mallory إلى المفتاح الخاص لـ Alice لإنشاء قيمة صالحة {Na, Nb, M}_PKa تجتاز فحص Alice. تُعمَّم هذه الفكرة في مبدأ Needham-Abadi: يجب أن تربط رسائل المصادقة هوية المرسل صراحةً، لا أن تعتمد على السياق وحده لتحديد الهوية.

ساعدت أداة التحقق من النماذج FDR (Failures-Divergences Refinement) في اكتشاف Lowe لخلل NSPK، إذ تستكشف بشكل شامل جميع عمليات تنفيذ البروتوكول الممكنة، بما في ذلك تدخلات الخصوم. وقد حفّز ذلك تطوير أدوات التحليل الشكلي للبروتوكولات: يستطيع Proverif (المبني على حساب pi التطبيقي) إثبات خصائص المصادقة والسرية أو نفيها في جلسات لا نهائية. ويستخدم Tamarin Prover إعادة كتابة المجموعات المتعددة، ويدعم بروتوكولات معقدة مثل TLS 1.3 وSignal. ومن الأدوات الأخرى AVISPA وScyther. تخضع تصميمات البروتوكولات الحديثة (TLS 1.3 وSignal وNoise) للتحقق الشكلي قبل نشرها — وهو إرث مباشر لحادثة NS/Lowe.

أوضحت هجمات NS الفرق بين أهداف المصادقة. مصادقة الكيان: إثبات أن طرفًا ما حي حاليًا ويشارك في البروتوكول، إذ تُعد الحداثة أمرًا مهمًا. مصادقة منشأ البيانات: إثبات أن رسالة محددة أنشأها طرف محدد، وقد لا يعني ذلك أن الطرف ما يزال حيًا. تقوّض هجمة Lowe مصادقة الكيان — تعتقد Alice أنها تصادق Bob، لكنها في الواقع تصادق Mallory الذي ينقل الرسائل إلى Bob. تحدد مواصفات البروتوكولات الحديثة الأهداف بدقة: "تتم مصادقة Alice لدى Bob بصفتها البادئ بهذه الجلسة." تؤدي الأهداف الغامضة إلى مواصفات ملتبسة تجتاز المراجعة غير الرسمية لكنها تفشل في التحليل الشكلي.

من الفئات الأخرى للهجمات المرتبطة بـ NS هجوم الانعكاس: يعيد Mallory إرسال الرسائل من Alice إلى Alice. إذا كان البروتوكول متماثلًا، أي إن الطرفين يستخدمان المفتاح نفسه وتنسيق الرسائل نفسه، فقد تقبل Alice تحديها هي بوصفه ردًا صالحًا من Bob. تتمثل الحماية في استخدام اتجاهات مختلفة للمفاتيح، أي مفاتيح تشفير وفك تشفير منفصلة لكل اتجاه، أو تضمين مؤشرات الأدوار في الرسائل، مثل أن يتضمن المشفِّر العبارة "I am initiator" في الرسالة. تتضمن البروتوكولات الحديثة مثل TLS سلاسل تسمية خاصة بالأدوار في المفاتيح المشتقة من HKDF، باستخدام "c e traffic" للعميل و"s hs traffic" للخادم، لمنع الانعكاس.

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

أثرت بروتوكولات Needham-Schroeder مباشرةً في تصميم Kerberos، من خلال الطوابع الزمنية لمنع إعادة التشغيل، والمقتبسة من إصلاح Denning-Sacco، وفي TLS، حيث تمنع MAC الخاصة بسجل التبادل في رسالة Finished التداخل والانعكاس، وفي Signal Protocol، من خلال ربط الجلسة بحالة ratchet، وفي Noise Protocol Framework، من خلال ربط الهوية بأنماط المصافحة. أثبتت هجمات NS أن الحجج الأمنية غير الرسمية غير كافية — إذ يجب تحليل كل بروتوكول في مواجهة خصم نشط يتحكم في الشبكة ويمكنه إعادة إرسال الرسائل وترتيبها من جديد وتعديلها. أصبح نموذج الخصم هذا، المعروف باسم Dolev-Yao، معيارًا في التحقق الشكلي من البروتوكولات.

ما التغيير البسيط الذي اقترحه Lowe لإصلاح الثغرة في بروتوكول NS ذي المفتاح العام؟

قدّم بروتوكول Needham-Schroeder المتماثل (1978) توزيع مفاتيح الجلسات القائم على طرف ثالث موثوق TTP. اكتشف هجوم Denning-Sacco (1981) ثغرة إعادة التشغيل، وعولجت بإضافة الطوابع الزمنية في Kerberos. تعرّض بروتوكول NSPK ذي المفتاح العام لهجوم MITM اكتشفه Lowe (1995) باستخدام التحقق من النماذج، وعولج بتضمين هوية المرسل في الرسائل. أرست هذه الهجمات التحقق الشكلي، باستخدام Proverif وTamarin، بوصفه أمرًا أساسيًا لتصميم البروتوكولات. ومن الدروس الأساسية: يجب أن تربط الرسائل هوية المرسل، ويجب عزل الجلسات عن بعضها، وتُمنع هجمات الانعكاس باشتقاق المفاتيح الاتجاهي، وتُمنع هجمات التداخل باستخدام رموز MAC لسجل التبادل.