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

С точки зрения понимания возможных последствий, возникающих при обнаружении недоработок в логике работы криптопротокола, этот пример является очень показательным. Для устранения подобных проблем были специально разработаны средства и методы анализа корректности построения логики работы криптопротоколов. Применение формальных методов позволяет также обнаружить коммуникационную избыточность в криптопротоколах, что является немаловажным плюсом в условиях постоянно возрастающих требований к оперативности обработки информации в современных сетях передачи данных.