Формальные методы анализа криптопротоколов

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