نموذج مهاجم Dolev-Yao والتشفير الرمزي

اقترحه Danny Dolev وAndrew Yao عام 1983، ويُعد نموذج Dolev-Yao نموذج الخصم القياسي لتحليل البروتوكولات الرمزية. ويتحكم المهاجم في الشبكة بأكملها.

يمكن لمهاجم Dolev-Yao: اعتراض أي رسالة، وتخزين الرسائل، وإعادة تشغيل الرسائل القديمة، وتزوير رسائل جديدة من المكوّنات المعروفة، لكنه لا يستطيع كسر البدائيات التشفيرية الأساسية.

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

تُمثَّل الرسائل على هيئة مصطلحات: enc(k, m)، sig(sk, m)، hash(m)، pair(a, b). يعرف المهاجم مصطلحات معينة ويشتق مصطلحات جديدة باستخدام قواعد محددة (قواعد الاستنتاج).

تكون معرفة المهاجم مغلقة تحت الاستنتاج: إذا كان يعرف enc(k,m) وk، فيمكنه اشتقاق m. وإذا كان يعرف pair(a,b)، فيمكنه اشتقاق a وb. إغلاق المعرفة الأولية = كل ما يمكن للمهاجم تعلّمه.

تُصاغ أمان البروتوكول على النحو التالي: «لا تحتوي معرفة المهاجم أبدًا على السر s في أي حالة قابلة للوصول». السرية = قابلية الوصول. المصادقة = غياب أنماط معينة من مسارات التنفيذ السيئة.

بروتوكول بين طرفين: A→B: {Na, A}_{K_B}؛ B→A: {Na, Nb}_{K_A}؛ A→B: {Nb}_{K_B}. في جبر المصطلحات: يرسل Alice ‏enc(pubkey_B, pair(Na, A)). نتحقق من أنه بعد التنفيذ لا يعرف Na سوى B.

حساب π التطبيقي (Abadi & Fournet 2001) هو جبر عمليات لنمذجة البروتوكولات. تتواصل العمليات عبر القنوات، ويتحكم المهاجم في القنوات العامة. يستخدم ProVerif وTamarin هذه الصياغة.

قد يظل البروتوكول الآمن في نموذج Dolev-Yao غير آمن حسابيًا إذا كان التطبيق التشفيري ضعيفًا. وتربط مبرهنة السلامة الحسابية (Cortier et al.) بين المجالين لفئات محددة من البدائيات التشفيرية.

لا يستطيع Dolev-Yao نمذجة: الخواص الجبرية (مثل تبديلية XOR)، أو هجمات القنوات الجانبية، أو أخطاء التنفيذ، أو الإخفاقات الاحتمالية. وتتعامل امتدادات مثل نموذج النظرية المعادلية مع بعض الخواص الجبرية.

يمنح Dolev-Yao المهاجم سيطرة كاملة على الشبكة، لكنه يفترض تشفيرًا مثاليًا. والرسائل مصطلحات في جبر؛ أما الأمان فهو خاصية قابلية للوصول. ويوفر حساب π التطبيقي اللغة الرسمية. ومن حدوده أنه لا يستطيع نمذجة العلاقات الجبرية أو القنوات الجانبية أو أخطاء التنفيذ.