Уразливість кріптопротокола полягає в тому, що якщо сеансовий ключ До попередньої сесії був скомпрометований, то зловмисник (позначимо його через С), що одержав можливість контролю мережевого трафіку на кроці 3 нової (іескомпрометірованной) сесії, перехоплює повідомлення (А -* В: (Kal) , A) Kbs) і замість нього посилає повідомлення (З -* В: (Кдь, А) ш). Учасник В відповідає повідомленням (В -* | A: (Nb) K * b), вважаючи, що А хоче встановити з ним нову сесію з ключем ЮаЬ. С, отримуючи дане повідомлення, розшифровує його і відправляє У повідомлення (С-> В : (Nb - 1) К1!, ь) - Таким чином, С встановлює сесію з В від імені А.

З точки зору розуміння можливих наслідків, що виникають при виявленні недоробок в логіці роботи кріптопротокола, цей приклад є дуже показовим. Для усунення подібних проблем були спеціально розроблені засоби і методи аналізу коректності побудови логіки роботи кріптопротоколов. Застосування формальних методів дозволяє також виявити комунікаційну надмірність у кріптопротоколах, що є важливим плюсом в умовах постійно зростаючих вимог до оперативності обробки інформації в сучасних мережах передачі даних.