Выявление уязвимостей в известных криптопротоколах, которые до определенного момента считались надежными, предполагает разработку формальных методов их анализа. Из существующих на сегодняшний день подходов к этому вопросу можно выделить четыре основных:
- моделирование и проверка работы протокола. Для этой цели полезно использовать специализированные языки и инструментарии, которые не создавались для анализа криптопротоколов;
- создание экспертных систем, которые разработчики криптопротоколов могут применить для апробирования различных сценариев функционирования криптопротокола;
- моделирование требований к семейству криптопротоколов. При этом можно употребить логику, разработанную специально для анализа таких свойств криптопротокола, как «знание» и «доверие»;
- разработка формальных моделей, основанных на алгебраических свойствах криптографических систем.
Каждый из перечисленных подходов не привязан к лежащим в основе криптопротоколов механизмам, а направлен только на анализ логики работы протокола.
