WikiSort.ru - Не сортированное

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

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

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

Существует автоматический завершенный метод для верифицирования свойств конфиденциальности криптографических протоколов. Метод основан на надежной абстрактной интерпретации криптографических протоколов, в котором используется расширение древовидных автоматов, а именно 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). Он состоит в подтверждении того, что модель, описывающая поведение системы, которая реализует проверяемый протокол, эквивалентна модели, задающей требования безопасности для данного протокола.