Методы анализа криптографических протоколов

Обновлено: 17.05.2024

Обзор наиболее используемых подходов для формального анализа криптографических протоколов и программных инструментов, реализованных на основе данных подходов. Сделан вывод об актуальности использования БАН-логики для анализа протоколов аутентификации.

Рубрика Программирование, компьютеры и кибернетика
Вид статья
Язык русский
Дата добавления 01.02.2019
Размер файла 25,7 K

Студенты, аспиранты, молодые ученые, использующие базу знаний в своей учебе и работе, будут вам очень благодарны.

Подходы к анализу безопасности протоколов аутентификации и авторизации

А.В. Демидов, В.Е. Киселев

Ключевые слова: формальная верификация протоколов; аутентификация; проверка модели; доказательство теорем; логический вывод; БАН-логика.

Approaches to security analysis of authentication and authorization protocols. A.V. Demidov, V.E. Kiselev

Keywords: formal verification of protocols; authentication; model checking; theorem proving; logical inference; BAN-logic.

В годовом отчете по информационной безопасности Cisco за 2017 год отмечен стремительный рост использования облачных приложений, использующих модификации открытого протокола аутентификации OAuth 2.0 [1]. Учитывая данный факт и устойчивую тенденцию к использованию распределенных информационно-вычислительных систем (РИВС) [2], существует потребность разработчиков РИВС в инструменте для автоматизированного анализа безопасности протоколов аутентификации.

В настоящее время для оценки корректности и безопасности протоколов существует несколько основных формальных подходов, на основании которых реализованы программные инструменты. Однако открытым остается вопрос о применимости данных решений для анализа безопасности открытых протоколов аутентификации, и в особенности их модификаций, используемых в облачных и распределенных информационно-вычислительных системах 3.

В данной статье приведено исследование актуальных подходов для формального анализа криптографических протоколов, программных инструментов, реализованных на основе данных подходов, и проанализирована применимость данных решений для анализа корректности и безопасности открытых протоколов аутентификации и авторизации.

Постановка задачи. Наиболее используемыми подходами для верификации протоколов являются: проверка модели (model checking), и логический вывод (logical inference), в том числе включающий в себя доказательство теорем (theorem proving) и логику доверия (believe logic). На основании данных подходов реализованы программные инструменты автоматизации анализа протоколов, приведенные в работах [5]. В основе данных решений использованы один или несколько из перечисленных подходов, вследствие чего каждое из данных программных инструментов имеет свою специализированную область применения, что вызывает логичную проблему определения оптимального метода для формального анализа корректности и безопасности открытых протоколов аутентификации.

В рамках данной работы исследуются существующие подходы для формальной верификации протоколов, программные инструменты, основанные на применении данных подходов, и исследуется применимость данных подходов и инструментов, в частности БАН-логики, для оценки корректности и безопасности протоколов аутентификации.

Стремительное увеличение интеграции облачных приложений сотрудниками в распределенные сети организаций [1] негативно сказывается на уязвимости распределенных систем, в связи с чем верификация протоколов аутентификации и авторизации пользователей распределенных систем становится одним из важнейших аспектов безопасной работы.

Стоит отметить, что помимо проверки корректного функционирования распределённых систем, верификация протокола включает определение уровня специальных свойств информационной безопасности. Наиболее важными из них являются:

1. Конфиденциальность - передаваемая информация недоступна при неавторизованном доступе.

2. Целостность - гарантия предоставления подлинной и полной информации авторизованному пользователю.

3. Доступность - обеспечение быстрого доступа к информации и ресурсам для авторизованного пользователя.

4. Аутентификация - установление подлинности пользователя при входе в систему.

5. Авторизация - проверка прав доступа пользователя к информации и ресурсам системы.

Применение подхода моделирования к верификации протоколов аутентификации и авторизации распределенных систем обладает рядом неоспоримых преимуществ:

1. Удобство применения - использование моделирования для верификации протоколов позволяет оценить уровень безопасности протокола не нарушая работу системы.

2. Вариативность модели - разработчик определяет модель, не включая в нее несущественные для проверки данного условия особенности моделируемой системы.

3. Возможность дальнейшего изменения и отладки - в зависимости от применяемого подхода, в качестве результата проверки разработчик получает отчет соответствия модели поставленным требованиям, помогающий обнаружить ошибочность построенной модели или предъявляемых к ней условий.

Недостатками моделирования являются:

1. Сложность процесса - разработчик модели должен выделить необходимые составляющие моделируемой системы, чтобы модель соответствовала реальной системе.

2. Сложность формализации представления - разработчик модели должен формализовать ее представление в терминах логики выбранного инструмента проверки.

3. Сложность постановки требований - разработчик модели должен корректно и исчерпывающе сформулировать требования, предъявляемые к моделируемой системе.

Несмотря на данные недостатки, моделирование является современным и эффективным методом верификации протоколов, а различные подходы к представлению и проверке моделей позволяют получать наиболее корректный результат оценки [7].

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

Алгоритмы проверки моделей базируются на полном просмотре пространства состояний модели: для каждого состояния проверяется, удовлетворяет ли оно сформулированным требованиям. Алгоритмы гарантированно завершаются, так как модель конечна [8, 9]. Метод верификации, основанный на проверке модели, использует представление системы, как набор состояний. При этом выделяется подмножество состояний с каким-либо нарушенным критерием безопасности. Для верификации в этом случае необходимо доказать, что такое множество в данной модели пустое, иначе система не попадает ни в одно из множеств.

безопасность протокол аутентификация авторизация

Читайте также: