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

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