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

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

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

Свойства безопасности

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

• Конфиденциальность (confidentiality, иногда secrecy) — обеспечение гарантий в том, что информация разделяется только авторизованными персонами или организациями. Конфиденциальная информация не должна быть доступной при неавторизованном доступе. Нарушения конфиденциальности могут произойти, когда данные обрабатываются неадекватным способом.
• Целостность (integrity) — обеспечение гарантий в том, что информация является подлинной и полной, что на информацию можно положиться. Термин «целостность» часто используется при рассмотрении информационной безопасности, поскольку она представляет один из первичных показателей безопасности. Целостность данных должна обеспечивать не только корректность данных, она должна отвечать на вопрос, можно ли доверять этим данным и полагаться на них. Защищённая информация не должна модифицироваться через неавторизованный доступ.
• Доступность (availability) — обеспечение быстрого доступа к информации и ресурсам. Информация не должна удерживаться неавторизованно. Это свойство можно понимать, как возможность получить необходимую информацию за приемлемое время.
• Аутентификация (authentication, иногда accountability) — установление подлинности агента при входе в систему.
• Неотказуемость (non-repudiation) — строгое выполнение обязательств.
• Авторизация (authorization) — проверка прав доступа к различным ресурсам.

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

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

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

Методы формальной верификации

Верификация на основе конечных автоматов

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

Методика анализа достижимости эффективна для определения корректности протокола по отношению к его спецификациям, однако она не гарантирует безопасности от активного злоумышленника.

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

Проверка модели

Криптографический протокол, подвергающийся воздействию противника, рассматривается как помеченная система переходов (LTS). Каждое состояние LTS представляется парой (S,K), где S — состояние вычисления протокола, а K — знания, доступные противнику. Переходы в LTS осуществляются на основании спецификации протокола и предположений о возможностях противника (модели противника). В результате переходов могут изменяться как состояния вычисления протокола, так и знания противника. Некоторые из переходов могут быть помечены действиями, которые выполняются при переходе. Проверяемое свойство протокола задаётся логической формулой. Для этой цели могут быть пригодны темпоральные логики, логики знаний и др. Таким образом, верификация криптографических протоколов сводится к классической задаче математической логики — проверке выполнимости формулы на модели. Проверка многих свойств сводится к проверке достижимости определённых состояний в LTS; для решения этой задачи разработаны многочисленные алгоритмы. Достоинством такого подхода является простота и универсальность, а также возможность применения многочисленных инструментальных средств решения задачи проверки моделей. Наибольшая трудность, с которой приходится сталкиваться при проверке реальных протоколов, состоит в том, что LTS могут иметь неограниченное число состояний. Для преодоления этой трудности используются символьные методы представления моделей, методы построения модели «на лету» (on-the-fly), различные виды абстракции данных.

Теоретико-доказательный подход

Описание (спецификация) протокола представляется в виде формулы Spec некоторого формального логического языка. Описание возможностей противника и проверяемого свойства протокола также представляются формулами Φ и Ψ. Задача верификации сводится к проверке выводимости формулы Ψ из формул Spec и Φ. Главное достоинство такого подхода состоит в том, что он позволяет проверять необходимые свойства для итеративных протоколов независимо от числа раундов их выполнения. Недостаток же заключается в том, что построение доказательства обычно весьма трудоемко и не может быть полностью автоматизировано. Обычно построение такого доказательства сводится к формированию специальной системы ограничений, в которой наряду с устройством протокола учитываются знания и возможности противника, и проверке разрешимости этой системы ограничений.

Проверка тестовой эквивалентности

В том случае, когда язык спецификации криптографических протоколов наделён формальной операционной семантикой (как это имеет место в случае spi-исчисления), на множестве протоколов можно ввести отношение трассовой или бисимуляционной эквивалентности ≈. Тогда для проверки некоторых свойств заданного параметризованного протокола P(M) достаточно проверить, что для любого процесса A, выступающего в роли противника, выполняется эквивалентность A|P(M)≈A|P(M′). В таком случае говорят, что процессы P(M) и P(M′) находятся в отношении тестовой эквивалентности. В было установлено, что задачи проверки свойств конфиденциальности и целостности протоколов сводятся к задаче проверки тестовой эквивалентности spi-процессов. Был предложен алгоритм проверки тестовой эквивалентности spi-процессов, свободных от репликации. Главная особенность этой задачи состоит в том, что эквивалентность A|P(M)≈A|P(M′) требуется проверять для произвольного процесса A (противника), и это приводит к необходимости анализировать бесконечно большое множество вычислений конечной длины. Отмечалось, что для эффективной проверки тестовой эквивалентности следует разработать методы символьного представления и анализа знаний противника. В настоящей заметке нами предлагается альтернативный метод представления и анализа знаний противника, который может быть применён для проверки тестовой эквивалентности процессов spi-исчисления.

Метод проверки типа

Самым новым подходом к формальному анализу протоколов является использование метода проверки типа (type checking), введённым Абади (Abadi). Абади ввёл тип untrusted (Un) для открытых сообщений, которые исходят от оппонента (в качестве оппонентов выступают все, кроме удостоверяющих принципалов). В методе проверки типа сообщениям и каналам присваиваются типы (например, единица данных приватного типа появляется на открытом канале). Метод проверки типа имеет существенное достоинство, состоящее в том, что он, как и метод проверки модели, является полностью автоматическим, но в отличие от последнего способен оперировать с несколькими классами бесконечных систем. Однако он имеет потенциальный недостаток, состоящий в том, что, так как нарушения безопасности определены в терминах несогласованностей типа, требования безопасности, которые должны быть доказаны, должны быть сформулированы в спецификации в процессе её написания. Это отличает метод проверки типов от метода проверки модели, для которого любое свойство безопасности, которое может быть выражено в терминах темпоральной логики, может специфицироваться независимо, уже после того, как сам протокол специфицирован.

Другие подходы

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

Метод обоснования на основе слабейшего предусловия (Weakest Precondition reasoning) предназначается для верификации программ. Эта методика рассматривает три компонента: состояние до выполнения инструкции программы, инструкция программы непосредственно и цель, которая должна быть истинна после того, как инструкция выполняется. Недостаток этой методики заключается в трудности доказательства для сложных предикатов. Для длинных программ, с большим количеством целей, доказательства могут быть невозможны. В работе, посвящённой интегрированной среде CPAL-ES (Cryptographic Protocol Analysis Language Evaluation System), для верификации применяется метод «слабейшего предусловия». Поскольку криптографические протоколы имеют тенденцию быть короткими, этот метод успешно применяется для этих протоколов.

Некоторые средства автоматической верификации криптографических протоколов

AVISPA/TA4SL

Средство автоматической верификации криптографических протоколов AVISPA, включающее в себя средство TA4SL, способно сделать анализ как ограниченного, так и неограниченного числа сеансов протокола с использованием OFMC, CL-ATSE и SATMC. AVISPA хорошо подходит для анализа свойств безопасности в случае ограниченного числа сеансов. В случае неограниченного числа сеансов AVISPA обеспечивает только ограниченную поддержку. Например, использование AVISPA является особенно проблематичным при отсутствии следов атаки.

ProVerif

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

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

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

Scyther

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

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

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

FDR2

В средстве FDR2, основанном на методе проверки модели, для описания поведения участников протокола используется нотация CSP (Communicating sequential processes). Каждый участник протокола моделируется с помощью процесса CSP, который находится либо в состоянии ожидания сообщения, либо посылает сообщение. Каналы используются для взаимодействия между процессами и моделирования противника. Противник описывается как параллельная композиция нескольких процессов, по одному на каждый факт или сообщение, из которых он может получить какие-либо сведения о выполнении протокола. FDR2 использует подход, который называется уточняющей проверкой модели (refinement model checking). Он состоит в подтверждении того, что модель, описывающая поведение системы, которая реализует проверяемый протокол, эквивалентна модели, задающей требования безопасности для данного протокола.

Литература

• Stinson, D. R. Cryptography: theory and practice. — Chapman and Hall/CRC, 2005. — ISBN 978-1584885085.
• Котенко, И. В. Верификация протоколов безопасности на основе комбинированного использования существующих методов и средств. — Труды СПИИРАН, 2009. — ISBN 978-307-115-2.
• Шаблон:Source
• Meadows, Catherine. Formal Verification of Cryptographic Protocols: A Survey // Proceedings of the 4th International Conference on the Theory and Applications of Cryptology: Advances in Cryptology (ASIACRYPT '94). — Springer-Verlag, 1995. — P. 135—150. — doi:647092.714095^{[Ошибка: Неверный DOI!]}.