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

Размещено на http://www.allbest.ru/

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

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

В рамках данной статьи проведен обзор наиболее используемых подходов для формального анализа криптографических протоколов и программных инструментов, реализованных на основе данных подходов. В статье рассмотрены такие подходы, как проверка модели, доказательство теорем и логика доверия, приведен перечень известных инструментов автоматизации анализа криптографических протоколов в рамках каждого подхода. На основании проведенных исследований сделан вывод об отсутствии универсального средства верификации протоколов, и актуальности использования БАН-логики для формального анализа протоколов аутентификации. Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 18-37-00430.

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

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

In the given article, are reviewed the most used approaches for formal cryptographic protocols analysis and software tools implemented on these approaches basis. The article considers such approaches as model checking, theorem proving and the logic for trust, and a list of known tools for automating cryptographic protocols analysis within each approach basis. Based on conducted research was concluded that there is no universal protocol verification tool and the relevance of using BAN-logic for formal authentication protocols analysis. The research was sponsored by RFBR, research project number № 18-37-00430.

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

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

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

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

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

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

Определение уровня безопасности протокола. Протокол - описание распределенного алгоритма, в процессе выполнения которого два участника (или более) последовательно выполняют определенные действия и обмениваются сообщениями. Безопасность протокола выражается в обеспечении гарантий выполнения таких свойств, характеризующих безопасность, как доступность, конфиденциальность, целостность и др. [5].

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

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

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

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

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

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

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

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

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

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

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

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

Также стоит отметить возможность усложнения модели системы с поэтапным добавлением в нее новых состояний и правил, что позволит сделать модель приближенной к оригиналу и обнаружить «узкие места» и моменты их возникновения [6].

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

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

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

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

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

Подход «Проверка модели». Основной идеей данного подхода является построение поведенческой модели системы, обладающей конечным числом состояний и требованиям (свойствам), подлежащим проверке в рамках состояний модели.

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

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

Основные программные инструменты, реализованные на основе подхода «Проверка модели», приведены в таблице 1.

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

Таблица 1 - Программные инструменты, реализованные на основе подхода «Проверка модели»

Результатом применения подхода «Проверка модели» является сообщение об успешном прохождении верификации при соответствии модели поставленным требованиям, либо последовательность действий модели, при проведении которых возникает несоответствие условиям. Если в результате проверки модели достигнуто несоответствие, выносится вердикт о некорректности модели, либо некорректность формальных требований [10].

Подход «Логический вывод»

В общем случае, логический вывод представляет дедуктивный подход к построению и формальному обоснованию утверждений (инвариантов).

Требования, предъявляемые к инвариантам:

1. Каждый инвариант истинен на момент начала работы системы.

2. После каждого шага работы системы каждый инвариант сохраняет истинность.

3. Конъюнкция инвариантов представляет собой спецификацию системы.

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

При применении метода логического вывода для анализа криптографических протоколов различают средства, основанные на подходе автоматического доказательства теорем (theorem proving) и логике доверия (believe logic).

Подход «Доказательство теорем»

Данный подход представляет программную реализацию средства для доказательства утверждений на основании логики высказываний и логики предикатов. В основе данного подхода лежит использование аппарата математической логики для реализации итогового программного инструмента [12].

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

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

Основные программные инструменты, реализованные на основе подхода «Доказательство теорем» приведены в таблице 2.

Подход «Логика доверия»

Данный подход подразумевает использование набора формальных правил для определения правдивости (доверия) утверждения. На основании данного подхода существуют такие реализации специализированных инструментов анализа утверждений, как GNY, SvO и другие. В рамках данной статьи будет рассмотрена реализация BAN-логики, основанной на применении подхода «Логика доверия», поскольку именно инструмент BAN-логики позволяет проводить формальный анализ корректности протоколов аутентификации.

Таблица 2 - Программные инструменты, реализованные на основе подхода «Доказательство теорем»

Логика Бэрроуза-Абади-Нидхэма или BAN-логика представляет собой формальную логическую модель для анализа знания и доверия [13]. Данная логика является разрешимой, то есть существует алгоритм, проверяющий правильность выводов, сделанных из гипотез.

Данная модель представляет собой набор конструкций, или логический язык, и связанный с ним набор аксиом и правил для использования в этих конструкциях. Авторы БАН-логики определили основные конструкции для четырех действий: доверия (believing), управления (controlling), получения (seing) и отсылки (saying) сообщений [14]. Данные конструкции составляют язык для описания доверий между компонентами сети во время работы протокола. Правила и аксиомы БАН-логики позволяют производить вывод новых доверительных утверждений из уже существующих [15].

Основные правила и их следствия приведены ниже (P и Q -- клиенты сети, X -- передаваемое сообщение, K -- ключ шифрования):

1. P| ? X (P доверяет X). P принимает значение X за истину, и может утверждать X в других сообщениях.

2. P < X (P видит X). P принял сообщение X, может читать и передавать X.

3. P| ~ X (P однажды высказал X). P в определенный момент времени послал сообщение, в котором содержится X.

4. P| => X (P имеет права на X). Утверждениям P на счёт X нужно доверять.

5. #X (X получено недавно). Сообщение X было послано недавно (как правило означает, что после запуска протокола).

6. Key (K, P-Q). Связь между P и Q производится при помощи ключа K.

7. {X}K. Данные X зашифрованы ключом K.

В соответствии с основным положением BAN-логики, метод анализа состоит из четырех шагов [14]:

Шаг 1. Идеализация протокола, приведение исходных данных в предикаты логики BAN.

Шаг 2. Обозначение начального состояния системы, используя формализмы BAN-логики.

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

Шаг 4. Проверка корректности протокола аутентификации с использованием правил вывода, начального состояния в сочетании с идеализированной моделью протокола.

Заключение

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

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

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

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

Список литературы

1. Cisco Systems, Inc. Годовой отчет по информационной безопасности 2017 г [Электронный ресурс] // ReportUKR. URL: http://nncit.tneu.edu.ua/wp-content/uploads/2017/10/ReportUKR.pdf (Дата обращения 24.08.2018).

2. S. A. Lazarev, A. V. Demidov, V. N. Volkov, A. A.Stychuk, D. A. Polovinkin. Analysis of applicability of open single sign-on protocols in distributed information-computing environment // Application of Information and Communication Technologies (AICT), 2016 IEEE 10th International Conference. - 2016. - INSPEC Accession Number: 17061734. - DOI: 10.1109/ICAICT.2016.7991757. URL: http://ieeexplore.ieee.org/document/7991757/ (Дата обращения 24.08.2018).

3. I.S. Konstantinov, S.A. Lazarev, O.V. Mihalev, V.E. Kiselev, A. V. Demidov. The model of management access to the resources of the closed discretionary information computation environment in the form of corporate portal network // Application of Information and Communication Technologies (AICT), 2016 IEEE 10th International Conference. - 2016. - INSPEC Accession Number: 17061734. - DOI: 10.1109/ICAICT.2016.7991744. URL: http://ieeexplore.ieee.org/document/7991744/?part=1 (Дата обращения 24.08.2018).

4. S.A Lazarev, I.S. Konstantinov, O.V. Mihalev, V.E. Kiselev. Implementation of unified session access model in a closed virtual environment of distributed information-computational resource system as a secured portal network // Research Journal of Applied Science. - 2015. - 10 (10): 629-632.

5. Черемушкин А. В. Автоматизированные средства анализа протоколов // ПДМ, 2009, приложение № 1, 34-36.

6. Черемушкин А. В. Криптографические протоколы: основные свойства и уязвимости // ПДМ, 2009, приложение № 2, 115-150.

7. B. Smyth. Formal verification of cryptographic protocols with automated reasoning // University of Birmingham. - 2011. - 189 с.

8. Кравцова А.С., Маро Е.А. КЛАССИФИКАЦИЯ СРЕДСТВ ВЕРИФИКАЦИИ ПРОТОКОЛОВ [Электронный ресурс] // Материалы VIII Международной студенческой электронной научной конференции «Студенческий научный форум»: [сайт]. [2016]. URL: https://www.scienceforum.ru/2016/1758/22207 (Дата обращения 24.08.2018).

9. K. Kogos, S. Zapechnikov. Studying formal security proofs for cryptographic protocols // WISE 2017. IFIP Advances in Information and Communication Technology, vol 503. Springer, Cham, pp 63-73.

10. Лепендин А. А., Уберт А. В. Метод верификации моделей в приложении к анализу протоколов аутентификации [Электронный ресурс] // Известия Алтайского государственного университета: [сайт]. [2012]. URL: https://cyberleninka.ru/article/n/metod-verifikatsii-modeley-v-prilozhenii-k-analizu-protokolov-autentifikatsii (Дата обращения 24.08.2018).

11. Анализ подходов к верификации функций безопасности // Москва: Российская Академия Наук. Институт Системного программирования, 2004. - 101 с.

12. J.Harrison. The LCF Approach to Theorem Proving [Электронный ресурс] // Intel Corporation: [сайт]. [2001]. URL: https://www.cl.cam.ac.uk/~jrh13/slides/manchester-12sep01/slides.pdf (дата обращения 24.08.2018).

13. Burrows M., Abadi M., Needham R. A Logic of Authentication // Proc. R. Soc. Lond. A 1989 426 233-271; DOI: 10.1098/rspa.1989.0125; pp.3-5.

14. Bleeker A., Meertens L. A semantics for BAN logic // Proceeding of DIMACS Workshop on Design and Formal Verification of Crypto Protocols, 1997.

15. Abadi M., Needham R. Prudent engineering practice for cryptographic protocols // Proceedings of IEEE Computer Society Symposium on Research in Security and Privacy. - 1994. - pp.122-136.

Размещено на Allbest.ru