Using Scyther for analysis SKID3 security.pdf Применение стойких криптографических алгоритмов в коммуникационных протоколахеще не гарантирует выполнения свойств, характеризующих безопасность (конфиденциальность,целостность, доступность и др.) передаваемой информации, если ихне обеспечивает спецификация протокола. Поэтому актуальной является задача разработкиформальных методов анализа безопасности протоколов и их автоматизации [1].При построении математических моделей протоколов не учитывают особенности реализациииспользуемых в них криптографических примитивов, а также возможныедействия, выходящие за рамки данного протокола. Это позволяет сосредоточиться нанахождении слабостей самого протокола [2]. Одной из последних разработок в данномнаправлении является автоматизированное средство Scyther, предложенное впервыев 2006 г. в рамках диссертации К. Кремерса [3].Целью данной работы является изучение математического аппарата средстваScyther и его применение для анализа безопасности протокола двусторонней аутентификацииSKID3 [4].Scyther относится к средствам, основанным на методе проверки на модели (modelchecking [5]). Формальная модель протокола описывает множество состояний и системупереходов из одного состояния в другое. Состояния, достижимые из заданногоначального, проверяются на удовлетворение некоторым свойствам безопасности.Язык, на котором формулируется спецификация анализируемого протокола, достаточнопрост и интуитивен, однако недостаточно выразителен, что ограничиваетприменимость данного средства. В частности, существенным ограничением являетсяотсутствие каких-либо средств описания ветвлений, что не позволяет описать многиеиз существующих протоколов. Тем не менее есть большое количество протоколовбез ветвлений, которые могут быть проанализированы, в частности протоколы аутентификации.Кроме того, математическая модель Scyther не позволяет анализироватьпротоколы, в которых фигурирует понятие времени (например, в сообщения добавляютсявременные метки). Вводится только отношение порядка на множестве событий.Спецификация протокола представляет собой описание ролей и действий, которыевыполняют агенты, ассоциированныес этими ролями. Требования к безопасности являютсячастью спецификации протокола в виде особого класса ролевых действий. Теоретическаямодель предполагает возможность проверки секретности некоторого терма(Secrecy), а также четыре вида аутентификации (Injective Synchronisation, InjectiveAgreement, Non-Injective Synchronisation, Non-Injective Agreement).Протокол SKID3 - это протокол взаимной аутентификации двух участников. О существующихпопытках анализа безопасности данного протокола автору неизвестно.В [4] указано, что SKID3 уязвим к атаке «человек посередине», однако не удалосьнайти сведений о конкретной ее реализации, а в результате собственных теоретическихисследований не получилось установить возможность реализации такой атаки.Вместо этого протокол SKID3 промоделирован средством Scyther с целью проверкивыполнения свойств NISynch - существования коммуникационного партнера длякаждого экземпляра события-требования и NIAgree - согласованности всех переменныхв процессе исполнения протокола [3]. В результате моделирования установлено,что в этом протоколе ни для одной роли свойства NIAgree и NISynch не нарушаютсяв условиях компрометации одного из агентов и секретных ключей между ним и довереннымиучастниками протокола, что можно трактовать как то, что протокол SKID3,скорее всего, неуязвим к атаке «человек посередине».

Скачать электронную версию публикации