Обзор программных инструментов анализа протоколов аутентификации и авторизации

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

Обзор программных инструментов анализа протоколов аутентификации и авторизации

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

Аннотация

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

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

Annotation

In the given article, was conducted an overview of the current software tools for formal analysis of authentication and authorization protocols. There are considered such software tools as AVISPA, ProVerif, Tamarin Prover and Scyther as well as their applicability and performance for assessing the security of authentication and authorization protocols. Based on the analysis studies concluded that there is no universal protocol verification tool and the hypothesis of the possible increase of reliability level of the safety assessment of distributed systems authentication and authentication protocols by applying BAN-logic raised. The research was sponsored by RFBR, research project number № 18-37-00430.

Keywords: avispa; proverif; tamarin prover; scyther; formal verification of protocols; authentication; authorization; BAN-logic.

Устойчивой тенденцией 2017-2018 года является стремительное увеличение числа облачных приложений, использующих модификации открытых протоколов аутентификации [1], особенно протоколы OAuth 2.0 и OpenID Connect. Наибольшую эффективность применения данные протоколы получили в распределенных информационно-вычислительных системах [2], использующих технологию Single Sign-On. При этом зачастую для организации процессов аутентификации и авторизации РИВС используются не исходные, а модифицированные версии данных протоколов, в связи с чем возникает проблема анализа безопасности измененных версий.

Оценка корректности и безопасности протоколов осуществляется исследователями с помощью программных инструментов, основанных на применении различных формальных подходов. Наиболее распространенными являются AVISPA [3], ProVerif [4], Tamarin Prover [5] и Scyther [6]. Однако ни один из данных программных инструментов не является универсальным, а также не может гарантировать, что полученная оценка является объективной.

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

Постановка задачи. По состоянию на 2018 год актуальными (поддерживаемыми авторами и применяющимися в исследованиях протоколов) инструментами для верификации протоколов аутентификации и авторизации являются такие программные средства, как: AVISPA, ProVerif, Tamarin Prover и Scyther [7, 8]. В основе данных решений лежит использование одного или нескольких подходов к анализу безопасности протоколов, а для проведения данной процедуры предварительно необходимо описать верифицируемый протокол в рамках требуемых формализмов. В данной работе рассматриваются перечисленные программные инструменты для верификации протоколов аутентификации, оценивается их производительность и применимость, а также выдвигается гипотеза о повышении уровня достоверности оценки безопасности протоколов аутентификации и авторизации распределенных систем путем применения БАН-логики [9].

О программных инструментах верификации протоколов. Одним из важнейших аспектов верификации большинства сетевых протоколов является проверка уязвимости к атакам злоумышленников. Примерами данных атак являются [10]:

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

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

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

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

Каждый инструмент основан на использовании одного или комбинации подходов к верификации протоколов безопасности, таких как «проверка модели» (Model checking) или «логический вывод» (logical inference), а также имеет уникальную программную реализацию.

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

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

В рамках данной работы рассмотрены такие программные инструменты автоматизированной верификации протоколов безопасности, как AVISPA, Proverif, Tamarin prover и Scyther, а также приведены данные исследований их производительности.

Проект AVISPA (Automated Validation of Internet Security Protocols and Applications) разработан в 2005 году в рамках программы Future and Emerging Technologies. В создании данного средства участво­вали LORIA-INRIA (Франция), ЕТН Цюрих (Швейцария), университет г. Генуя (Ита­лия), Siemens AG (Германия). В рамках проекта AVISPA предпринята попытка создания комбинированного средства верификации протоколов. Данное средство позволяет создать описание протокола с помощью специализированного языка HLPLS (High Level Protocol Specification Language) и после преобразования его в промежуточное представление IF (Intermediate Format) вызывать одно из нескольких средств верификации, при этом проверяемые свойства записываются в терминах темпоральной логики.

Четыре средства верификации, доступные при работе с AVISPA:

- TA4SP (Tree Automata based on Automatic Approximations for the Analysis of Security Protocols) - реализует построение древовидных автоматов, основанных на перезаписи термов и аппроксимации, позволяющей выявлять уязвимость протокола в случае бесконечного количества сеансов. Для определения безопасности он может либо использовать подход чрезмерной, либо недостаточной аппроксимации, чтобы показать, что протокол защищен или безопасен для любого количества сеансов. Однако инструмент не предоставляет последовательность действий для осуществления атаки.

- SATMC (SAT-based Model-Checker) - использует методы, разработанные в рамках теории решения задач планирования. Данное средство основано на сведении задачи выявления уязвимости протокола по отношению к атакам конечной длины к задаче разрешимости пропозициональной формулы.

- OFMC (Open-Source Fixed-Point Model-Checker) - основан на применении ленивого поиска по запросу для анализа криптографических протоколов. Первый подход в рамках данного средства основан на применении ленивых типов данных для создания эффективного средства проверки моделей «на лету» для протоколов с большим или даже неограниченным числом состояний. Второй подход заключается в интеграции символического анализа для моделирования «ленивого нарушителя» Долева-Яо, действия которого генерируются по запросу [11].

- CL-At.Se (Constraint-Logic- based Attack Searcher) - выполняет протокол всеми возможными способами через конечный набор сеансов. Результаты выполнения протокола упрощаются благодаря эвристике и методам устранения избыточности, позволяющим решить, были ли нарушены свойства безопасности или нет.

Программное средство ProVerif разработано в 2006 году коллективом под руководством Бруно Бланшета в рамках проекта, финансируемого INRIA (Франция). Данный инструмент позволяет реализовать анализ протоколов аутентификации и авторизации с использованием верхней аппроксимации и представления протокола с помощью хорновских выражений. Входные данные могут быть записаны либо в формате выражений Хорна, либо с использованием подмножества Pi-исчисления.

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

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

Инструмент Tamarin Prover был разработан в 2012 году командой программистов под руководством Дэвида Басина, и представляет собой инструмент для символьного моделирования и анализа протоколов безопасности. В качестве входной информации используется модель протокола безопасности, определяющая действия агентов, имеющих различные роли при выполнении протокола (например, инициатор протокола), спецификация противника и спецификация проверяемых утверждений. Протоколы и угрозы определяются при помощи формального языка, основанного на правилах многократного переписывания. Эти правила определяют систему перехода между состояниями, каждое состояние которой состоит из символьного представления знаний противника, сообщений в сети, информации о новых сгенерированных значениях и текущим состоянием протокола [12]. Атакующая сторона и протокол взаимодействуют путем обновления и создания новых сетевых сообщений.

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

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

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

Инструмент Scyther разработан в 2008 году в ЕТН (Цюрих) под руководством Каса Кремерса. Scyther позволяет верифицировать как ограниченное, так и неограниченное число сеансов протокола с гарантированным завершением работы программного инструмента. В основе анализа лежит использование обратного символьного поиска, основанного на частично упорядоченных шаблонах.

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

В отличие от ранее рассмотренных программных средств, Scyther не поддерживает XOR и Диффи-Хеллман, однако предоставляет противнику возможность переписывать формализмы в фиксированных подтермах, полученных из спецификации анализируемого протокола.

Сравнение программных инструментов анализа протоколов. Сравнивая основные программные инструменты следует упомянуть, что согласно базе данных Elsevier Scopus графики упоминания в научных публикациях описанных решений имеют тенденцию к росту, однако исходя из этих данных можно предположить, что недостаточная унификация инструментария, ведет к появлению и поддержке изысканий в области разработки новых инструментов (AVISPA с 2003, ProVerif с 2006, Scyther с 2008, Tamarin Prover с 2013).

Рисунок 1. Количество публикаций в Elsevier Scopus упоминающих рассматриваемые программные средства анализа протоколов (по состоянию на август 2018 года)

В рамках исследования Performance Evaluations of Cryptographic Protocols Verification Tools Dealing with Algebraic Properties 2016 года, авторов Lafourcade P., Puys M., приведены сравнительные данные производительности для обозреваемых инструментов верификации [14], подтверждающие отсутствие универсального программного средства для анализа безопасности протоколов аутентификации и авторизации.

Наиболее эффективным средством для получения обобщенной оценки является AVISPA за счет использования комбинированного подхода к верификации алгоритмов - модули CL-Atse, OFMC, TA4SP и SATMC по сути представляют реализацию различных подходов, объединенные в рамках одного инструмента.

Однако более новые программные средства зарекомендовали себя как более производительные (ProVerif), или имеющие расширенный функционал анализа (обработка темпоральных параметров при помощи Tamarin Prover и использование частично упорядоченных шаблонов в Scyther).

Резюмируя, можно отметить, что каждое из рассмотренных программных средств позволяет оценить безопасность протоколов, используя один или несколько подходов моделирования, в связи с чем каждый инструмент обладает различными показателями производительности [15, 16]. Для получения наиболее объективной оценки требуется использовать комбинированный подход, поскольку ни одно из программных решений не является универсальным. В большей части отсутствие универсального средства связано с сложность приведения анализируемого протокола к требуемому формальному виду. Так, в работе Operational Semantics and Verification of Security Protocols 2012 года, за авторством К. Кремерса (являющимся одним из разработчиков Tamarin Prover и Scyther) и С. Маува, произведен анализ проблематики формализации протоколов, а также даются общие методические указания по построению моделей протоколов и их верификации [17].

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

Заключение

В рамках данного обзора были рассмотрены такие актуальные программные инструменты верификации протоколов аутентификации и верификации, как AVISPA, ProVerif, Tamarin Prover и Scyther. Каждое из данных средств позволяет оценить безопасность протоколов, используя один или несколько подходов моделирования, в связи с чем данные программы обладают различными показателями производительности, и в целом ни одно из них не является универсальным, что позволяет выдвинуть гипотезу о повышении уровня достоверности оценки безопасности протоколов аутентификации и авторизации распределенных систем путем применения БАН-логики.

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

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

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. The AVISPA Project [Электронный ресурс] // The AVISPA Project: [сайт]. URL: http://www.avispa-project.org/ (Дата обращения 24.08.2018).

4. ProVerif [Электронный ресурс] // ProVerif: [сайт]. URL: http://prosecco.gforge.inria.fr/personal/bblanche/proverif/ (Дата обращения 24.08.2018).

5. Tamarin Prover [Электронный ресурс] // Tamarin Prover: [сайт]. URL: https://tamarin-prover.github.io/ (Дата обращения 24.08.2018).

6. Scyther tool [Электронный ресурс] // Scyther tool: [сайт]. URL: https://people.cispa.io/cas.cremers/scyther/ (Дата обращения 24.08.2018).

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

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

9. 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.

10. Перевышина Е.А. Методы и средства верификации криптографических протоколов // Материалы VIII Международной студенческой электронной научной конференции «Студенческий научный форум»: [сайт]. [2017]. URL: http://www.scienceforum.ru/2017/2323/33304 (дата обращения: 24.08.2018).

11. D. Basin, S. MoЁdersheim, L. Vigan`o. An On-The-Fly Model-Checker for Security Protocol Analysis // In Proc. of ESORICS'03, volume 2808 of LNCS, pages 253-270. Springer-Verlag, 2003.

12. D. Basin, S. MoЁdersheim, L. Vigan`o. Ofmc: A symbolic model checker for security protocols // Int. J. Inf. Sec., 4(3):181- 208, 2005.

13. J. Bull, D. J. Otway. The authentication protocol. Technical Report DRA/CIS3/PROJ/CORBA/SC/1/CSM/436-04/03 // Defence Research Agency, 1997.

14. P. Lafourcade, M. Puys. Performance Evaluations of Cryptographic Protocols Verification Tools Dealing with Algebraic Properties // In: Garcia-Alfaro J., Kranakis E., Bonfante G. (eds) Foundations and Practice of Security. FPS 2015. Lecture Notes in Computer Science, vol 9482. Springer, Cham.

15. M. Cheminod, I. C. Bertolotti, L. Durante, R. Sisto, A. Valenzano. Experimental comparison of automatic tools for the formal analysis of cryptographic protocols // In DepCoS-RELCOMEX 2007, June 14-16, 2007, Szklarska Poreba, Poland, pages 153-160. IEEE Computer Society, 2007.

16. 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.

17. C. Cremers, S. Mauw. Operational Semantics and Verification of Security Protocols // Information Security and Cryptography, Springer-Verlag Berlin Heidelberg. - 2012. - pp. 67-105.

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

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