2.2.6. Методы анализа протоколов распределения ключей

и обилием предъявляемых к ним требований. Тем более сложным является анализ соответствия предложенных протоколов этим тре-бованиям.

Известны три группы методов анализа стойкости протоколов распределения ключей:

Эвристический (ad-hoc) анализ - это традиционный способ, характерный для классической криптографии.

Формальные методы анализа. Эта группа методов характеризуется тем, что готовые протоколы подвергаются анализу при по-мощи специальных математических и логических методов. Но ана-лизируется не содержательная, а формальная сторона протокола, форма его построения, признаки и свойства, появляющиеся на каждом шаге выполнения протокола. Хорошо разработаны и широко известны специальные формальные логики для анализа криптогра-фических протоколов, такие, как В AN-логика и GNY-логика. Безус-ловным преимуществом этих методов является то, что они хорошо алгоритмизуются, что позволяет создавать автоматические про-граммные анализаторы криптографических протоколов. Однако принципиальное их ограничение заключается в том, что они обна-руживают не все ошибки в анализируемых протоколах. Если при формальном анализе ошибки в протоколе обнаружены, это означает, что они в протоколе действительно есть и позволяют противнику строить соответствующие атаки на протокол. Если же они не обна-ружены, это еще не значит, что их в протоколе действительно нет.

Методы доказательства безопасности. Эта группа методов - частный случай общего подхода, на котором базируется современная доказательно безопасная криптография. Напомним, что эта ме-тодология позволяет, в отличие от двух предыдущих, конструировать криптографические протоколы с заранее заданными свойствами безопасности.