Показана возможность применения метода model checking для верификации криптографических протоколов. На примере протокола Нидхема-Шрёдера продемонстрирован подход к моделированию взаимодействующих сторон как параллельно исполняемых процессов, обменивающихся сообщениями. Приведен пример формализации и проверки свойств протокола с помощью формул линейной темпоральной логики. Найдена классическая уязвимость протокола Нидхема-Шрёдера - атака Лоу.

Ключевые слова: криптографический протокол, аутентификация, метод model checking, линейная темпоральная логика, автоматическая верификация.