Формальная верификация криптографических протоколов

Формальная верификация криптографических протоколов — проверка криптографических протоколов на обеспечение требуемых свойств безопасности. Одной из составляющих такой проверки является определение стойкости протокола к атакам в предположении о надёжности криптографических примитивов, на которых он основывается. Для решения этой задачи разработан ряд подходов, основанных на различных формальных методах верификации. Общей чертой формальных методов является использование системного подхода к проблеме, позволяющего выполнять более обоснованную, точную и эффективную проверку свойств безопасности протокола.

Термин формальная верификация криптографических протоколов впервые был введён Кэтрин Медоус (Catherine Meadows) — главным исследователем англ. Center for High Assurance Computer Systems (CHACS) и Naval Research Laboratory (NRL).

Источник: Википедия