Компьютерная безопасность

Данный подход является наименее распространенным, поскольку его основная идея заключается в представлении криптопротокола как программы с последующей попыткой доказательства его корректности. Однако тут же необходимо отметить, что из доказательства корректности протокола не следует доказательство его безопасности. Наиболее успешными в данном направлении считаются формальные методы, автором которых является Кеммерер, и формальный язык LOTOS (Language of Temporal/Ordering Specification), созданный для анализа протоколов аутентификации. Кеммерер в своих работах выделил две цели, для достижения которых можно использовать формальные методы анализа криптопротоколов:
• формальный анализ того, что криптопротокол удовлетворяет требованиям безопасности;
• обнаружение уязвимостей в криптопротоколах.
Формальная модель построена на использовании конечных автоматов, по отношению к которым криптопротокол рассматривается как набор различных состояний, отличающихся друг от друга значениями переменных состояния. При этом значения переменных могут быть изменены только с помощью строго определенных процедур.
Примером использования конечных автоматов является анализ протоколов аутентификации. Для каждой процедуры (итерации криптопротокола)определяется состояние криптопротокола (системы), выражающееся в описании состояний участников и коммуникационных каналов между ними. После чего каждый набор состояний анализируется на предмет корректности и отсутствия тупиковых ситуаций.