منطق بوروس-عبادي-نظيم

إن منطق بوروس- عبادي- نظيم (والذي يعرف أيضا باسم منطق بان the BAN logic) هو مجموعة من القواعد الموضوعة من أجل تعريف وتحليل موافيق (بروتوكولات) تبادل المعلومات. وعلى وجه الخصوص فإن منطق بان يساعد مستخدميه في تحديد ما إذا كانت المعلومات المتبادلة موثوقا بها، أو مؤمنة ضد التنصت أو كليهما معا. ويبدأ منطق بان بفرضية تقول أن كل المعلومات التي يتم تبادلها خلال وسائل الإعلام يجب أن تخضع للتنقيح والمراقبة العامة. وقد تطور هذا المنطق إلى المفهوم الأمني المشهور «لا تثق في الشبكة.» ويتضمن ترتيب منطق بان النمطي الخطوات الثلاثة التالية:

1. التحقق من أصل الرسالة.
2. التحقق من جدية الرسالة.
3. التحقق من مصداقية الأصل.

ويستخدم منطق بان المسلمات والتعريفات – مثل جميع النظم البديهية- من أجل تحليل موافيق (بروتوكولات) الاستيثاق. ويصاحب استخدام منطق بان في الغالب صيغة تنويت البروتوكول الأمني لبروتوكول ما وأحيانا ما تقدم في صورة ورقية.

نوع اللغة والبدائل

إن منطق بان، والمنطقيات في نفس الأسرة، تتسم بكونها قابلة لاتخاذ قرار فيها: ويوجد لوغاريتم يأخذ فرضيات بان وخاتمته المزعومة، وتكون هذه الأجوبة سواء أكانت الخاتمة أم لا مستقاة من هذه الفرضيات. وتستخدم اللوغاريتمات المقترحة مجموعة متباينة من أوعية السحر magic sets (Monniaux, 1999). وقد أثر منطق بان على العديد من الشكليات المشابهة، مثل منطق جني GNY logic. ويحاول بعض هذه المنطقيات إصلاح نقطة ضعف منطق بان وهي: الافتقاد إلى الدلاليات المناسبة ذات المعنى الواضح وفقا للمعرفة والبيئات الممكنة.

القواعد الأساسية

فيما يلي التعريفات وتطبيقاتها ( P و Q هما عميلي الشبكة، و X رسالة، و K هو مفتاح التعمية:

• P يوقن بـ X: وتعمل P كما لو أن X صحيحة، ويمكن أن تؤكد X في رسائل أخرى.
• لـ K سلطة على X: ويجب الوثوق في آراء P عن X.
• P قالت X: تقوم P بنقل (واليقين) بالرسالة X في مرة واحدة، بالرغم من أن P لم تعد يصدق بـ X.
• P تنظر لـ X: P تتلقى الرسالة X، ويمكن أن تقرأ وتعيد X.
• {X}K : X عميت بالمتاح K.
• (X) الجديدة: لم يسبق إرسال X في أية رسالة.
• المفتاح (K, P↔Q): P و Q يمكن أن يتصلا بمفتاح K المشترك

وقد تم التوصل لمعنى هذه التعريفات في سلسلة من postulates:

• إذا كانت P يصدق بالمفتاح (K, P↔Q)، وتنظر P لـ {X}K، ثم يصدق P ( Q قالت X).
• إذا كانت P يصدق بـ ( Q قالت X) ويصدق P بجدية (X)، عندها يصدق P بـ ( Q يصدق بـ X).

ويجب أن يصدق P بأن X جديد هنا، ومن ثم يمكن أن تكون رسالة متروكة، ويعاد تشغيلها بواسطة مهاجم.

• إذا كانت P يصدق بأن ( Q لها سلطة على X) ويصدق P بـ ( Q يصدق بـ X)، عندها فإن P يصدق X
• وهناك العديد من المسلمات الفنية الأخرى التي يجب القيام بها فيما يتعلق بكتابة الرسائل. على سبيل المثال، إذا كانت P يصدق بأن Q قالت <X, Y> ، وهو اللم المتسلسل الخاص بـ X و Y، عندها فإن P يصدق أيضا أن Q قالت X، ويصدق P أيضا أن Q قالت Y.

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

تحليل منطق بان لبروتوكول الضفدع عريض الفم Wide Mouth Frog

يسمح بروتوكول الضفدع عريض الفم- وهو بروتوكول بسيط للغاية لعاملين، وهما A و B، بعمل اتصال آمن، وباستخدام خادم استيثاق موثوق فيه، وهو S، وساعات متزامنة في جميع الأنحاء. وباستخدام التنويت المتعارف عليه يمكن للبروتوكول أن يكون محددا كما يلي: يشغل المفتاحان Kas و Kbs العاملين A و B على التوالي من أجل الاتصال الآمن مع S. لذا فإن لدينا الفرضيات التالية:

$A\rightarrow S:A,\{T_{A},K_{ab},B\}_{K_{as}}$

$S\rightarrow B:\{T_{S},K_{ab},A\}_{K_{bs}}$

ويريد العامل A بدء مناقشة آمنة مع B. ومن ثم فإنه يخترع مفتاحا وهو K_ab, والذي سيستخدمه من أجل الاتصال مع B. ويصدق A أن هذا المفتاح آمنا لأنه هو الذي قام بصنع هذا المفتاح بنفسه:

A يصدق المفتاح (K_as, A↔S)

S يصدق المفتاح (K_as, A↔S)

B يصدق المفتاح (K_bs, B↔S)

S يصدق المفتاح (K_bs, B↔S)

ويريد العامل A بدء مناقشة آمنة مع B. ومن ثم فإنه يخترع مفتاحا وهو K_ab, والذي سيستخدمه من أجل الاتصال مع B. ويصدق A أن هذا المفتاح آمنا لأنه هو الذي قام بصنع هذا المفتاح بنفسه:

A يصدق المفتاح (K_ab, A↔B)

B يريد أن يقبل هذا المفتاح طالما أنه من المؤكد أنه جاء من A:

B يصدق أن (A له سلطة على المفتاح (K, A↔B))

علاوة على ذلك، فإن B تريد الوثوق في S من للاعتماد الموثوق فيه على المفاتيح القادمة من A:

B يصدق أن (S له سلطة على (A يصدق المفتاح (K, A↔B)))

وهكذا فإنه إذا كان B يصدق أن S يصدق أن A يريد استخدام مفتاحا خاصا للاتصال مع B، من ثم فإن B سوق يثق في S ويصدقه أيضا. ويكون الهدف هو الوصول إلى أن

B يصدق المفتاح (K_ab, A↔B)

ويقرأ A الساعة، ويحصل على الوقت الحالي t ، ويرسل الرسالة التالية:

1 A->S: {t, key(K_ab, A↔B)}_Kas

وهكذا فإنه يرسل مفتاح الجلسة المختارة والوقت الحالي إلى S، ويعميه بمفتاح خادم الاستيثاق الخاص به K_as.

ونظرا لأن S يصدق المفتاح (K_as, A↔S), وS يرى {t, key(K_ab, A↔B)}_Kas,

ومن ثم فإن S تتوصل إلى أن A بالفعل قد قالت {t, key(K_ab, A↔B)}. (وعلى وجه الخصوص فإن S يصدق أن الرسالة لم يتم اصطناعها كلية من قبل بعض المهاجمين.)

ونظرا لأن الساعات متزامنة فإنه بإمكاننا أن نفترض أن

S believes fresh(t)

ونظرا لأن S يصدق جدية (t) وأن S يصدق أن A قد قالت {t, key(K_ab, A↔B)}, فإن S يصدق أن A يصدق فعليا المفتاح (K_ab, A↔B). (وعلى وجه الخصوص فإن S يصدق أن الرسالة لم يتم إعادة عرضها من قبل بعض المهاجمين الذين استولوا عليها في أحد الأوقات في الماضي.) ثم تقوم S بتمرير المفتاح إلى B:

2 S->B: {t, A, A believes key(K_ab, A↔B)}_Kbs

ونظرا لأن الرسالة 2 تمت تعميتها بـ K_bs, و B يصدق أن المفتاح(K_bs, B↔S), ، فإن B الآن يصدق أن S قد قالت {t, A, A يصدق المفتاح(K_ab, A↔B)}. ونظرا لأن الساعات متزامنة فإن B يصدق بجدية (t)، وكذلك بجدية (A believes key(K_ab, A↔B))، ونظرا لأن B يصدق أن بيان S جديد تماما، وأن B يصدق أن (A believes key(K_ab, A↔B)). ونظرا لأن B يصدق أن S ذو سلطة فيما يتعلق ببما يصدق به A، وأن B يصدق أن (A believes key(K_ab, A↔B)). ونظرا لأن ب تصدق أن A ذو سلطة بخصوص مفاتيح الجلسات بين A و B، وأن B تصدق المفتاح (K_ab, A↔B). ويمكن أن تتصل الآن B مباشرة بـ A، باستخدام K_ab كمفتاح جلسة سري.

والآن دعونا نفترض أننا نتخلي عن فرضية أن الساعات متزامنة. في هذه الحالة فإن S تحصل على الرسالة 1 من A مع {t, key(K_ab, A↔B)}, لكن لا يظل بإمكانه التوصل إلى أن ذلك كان أمرا جديدا. وهو يعرف أن A قد أرسلت هذه الرسالة في وقت ما في الماضي ( لأنها عميت مع K_as) ولكنها ليست رسالة حديثة الإرسال، لذلك فإن S لا تصدق أن A يحتاج بالضرورة إلى مواصلة استخدام المفتاح K_ab. ويشير ذلك مباشرة إلى هجمة على البروتوكول: أن المهاجم الذي يمكنه الاستيلاء على الرسائل يمكنه تخمين واحدة من مفاتيح جلسة قديمة K_ab. (ويمكن أن يستغرق ذلك وقتا أطول.)ثم يقوم المهاجم بإعادة عرض الرسالة القديمة {t, key(K_ab, A↔B)}، ويرسلها إلى S. وإذا لم تكن الساعات متزامنة (ربما كجزء من نفس الهجوم) فإن S قد تصدق هذه الرسالة القديمة وتطلب أن يستخدم B القديمة، وينتهى المفتاح مرة أخرى. إن الورقة الأصلية لمنطق الاستيثاق (لها رابط في الأسفل) تحتوي هذا المثال والعديد من الأمثلة الأخرى بما فيها تحليلات بروتوكول كاربيروس Kerberos للمصافحة بالأيدي، وإصدارين من مشروع أندرو Andrew Project RPC (أحدهما معيب ).

مراجع

• David Monniaux, Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief, in Proceedings of The 12th Computer Security Foundations Workshop, 1999. (Online).

وصلات خارجية

• A Logic of Authentication (mirror), the original paper by مايكل بروس, مارتين عبادي, and روجر مايكل نيدام ‏.
• Source: The Burrows–Abadi–Needham logic
• BAN logic in context, from UT Austin CS (PDF)