CL-ATSE

CL-Atse (англ. Constraint-Logic-based ATtack SEarcher) — это инструмент, который преобразует любое описание протокола безопасности на языке IF во множество предположений, которое затем может быть проанализировано на наличие атак на протокол.

Общее описание

CL-Atse имеет следующие характеристики:

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

Каждый шаг протокола моделируется предположениями о знании наблюдателя. Например, сообщение полученное честным участником является невыводимым предположением для наблюдателя. Такие выражения, как равенство, неравенство, (не)принадлежность элемента списку также являются предположениями. Для интерпретации IF отношения, каждая роль частично выполняется для того, чтобы извлечь точный и минимальный список предположений, которые моделируют ее. Состояния и знания участников уничтожаются, благодаря использованию глобальных переменных. Каждый шаг протокола выполняется путем добавления новых предположений в систему и сокращением/уничтожением других предположений. Наконец, на каждом шаге состояние системы проверяется согласно предоставленному множеству параметров безопасности.

Алгоритм анализа, который используется в CL-Atse, спроектирован для конечного числа циклов, т.е. для конечного числа протокольных шагов. Так что, если описание протокола не имеет циклов, то все описание и анализируется, в противном случае пользователь должен предоставить целочисленное ограничение на максимальное число циклов.

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

Экземпляры ролей: В CL-Atse каждая роль должна быть независима от других и использовать другие имена переменных. Отсюда следует, что каждая роль в IF файле обрабатывается во множество ролей, по одной на каждый “state_” факт в начальном состоянии. Эта обработка в действительности «запускает» роль участника, генерирует новые имена переменных и извлекает (минимальное) множество предположений, описывающее эту роль. Например, переменная GX у роли “Server” может стать GX(1) и GX(2) в двух экземплярах ролей этого “Server”’а. Также каждый одноразовый номер (Скажем, Na) генерируемый в описании заменяется различной константой в каждому экземпляре роли (Скажем, n1(Na) и n2(Na)). Для читаемости множество предположений представляющих каждый экземпляр роли отображается в следующем синтаксисе:

Шаг: Полученное сообщение => Отправленное сообщение [$\sigma$] &Неравенства &IF факты

Где $\sigma$ – объединение предположений (т.е. множество равенств). Для краткости, символ & обозначает новую строку. Любой недетерминизм в выполнении роли представляется точкой выбора из множества ролей. Когда наступает точка выбора, система (В действительности, нарушитель) выбирает, какая ветвь будет исполняться. Наконец, роль образует дерево, где унарные вершины – протокольные шаги, а n-арные вершины - точки выборов. Выполнение роли – это путь в этом дереве.

IF факты: Каждый протокольный шаг содержит все факты, найденные для этого шага в IF файле (Исключая состояние). Тогда как их синтаксис может немного отличаться от оригинальных IF фактов из-за внутреннего представления CL-Atse, их семантика аналогична. Главные отличия:

• Факты Contains(term, set) заменены на “Test term in set”, “Test term not in set”, “Add term to set” и “Remove term from set” в зависимости от позиции факта contains(..) в правиле. В остальном они следуют семантике contains(..).
• Secret(term, mark, set) стали “Secret (term, set)”

Внутреннее устройство

$Term=Atom\mid Var\mid Term.Term\mid \{Term\}_{Term}^{s}\mid \{Term\}_{Term}^{a}\mid inv(Term)\mid Term\oplus Term\mid Exp(Term,Product)$

$Product=(Term)^{\pm 1}\mid (Term)^{\pm 1}\times Product$

Термы могут быть атомами, переменными, конкатенацией (или парой), симметричным или асимметричным шифром (Обозначенные как $s$ и $a$). Также здесь $inv(k)$ - инверсия для асимметричного шифра. Операторы $\oplus$ и $Exp(...)$ моделируют сложение по модулю 2 и показательную функцию.

Возможности злоумышленника в CL-Atse совпадают с такими в модели угроз Долева - Яо, расширенные до xor и показательной функции. За $Forge(E)$ обозначается бесконечное множество сообщений, которое злоумышленник может сгенерировать из множества базовых термов $E$. В частности он способен строить пары, шифры, xor и экспоненты и разлагать на составные термы пары, дешифровать (Если возможно) и т.д.

Протоколы и системные состояния

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

$State=Subst,Sets,ToDec,Knowns$

$ToDec=(Term,Term)^{*}$

$Known=H(var)\vartriangleright Known\mid D(Term)\vartriangleright Known\mid e$

$Subst$ - подстановка, $Sets$ - список фактов $t\in set$ и $\{t,set\}\subset Term$, который означает, что в этом состоянии элемент $t$ находится во множестве $set$ и $ToDec$ - список возможностей для вывода знаний: если $(m,k)\in ToDec$, то злоумышленник получит $m$ как только сможет вывести $k$. Наконец, $Knowns$ - список элементарных разложенных знаний $D(t)$ и гипотез $H(v)$ в порядке создания в ходе исполнения. Например:

$Known=H(x)\vartriangleright H(y)\vartriangleright D(\{z\}_{k}^{s})\vartriangleright H(z)\vartriangleright D(a)\vartriangleright D(b)\vartriangleright e$

означает, что злоумышленник знает $\{z\}_{k}^{s}$, $a$, $b$, но должен вывести значение $z$ из $\{a,b\}$ и значения $x$ и $y$ из $\{\{z\}_{k}^{s},a,b\}$. За $E_{|D}$ обозначается множество термов $t$ таких, что $D(t)\in E$. Выше описанное символьное представление состояния моделирует бесконечное множество базовых состояний $\sigma (Known_{|D},Sets)$ такое, что $\sigma$ - базовый экземпляр $Subst$ и $\sigma (v)\in Forge(\sigma (F_{|D}))$ при $Known=E\vartriangleright H(v)\vartriangleright F$.

Протокольный шаг в CL-Atse представляет собой элементарное действие участника: при получении сообщения $rcv$, к которому приложены список $CtrList$, содержащий предположения $u=v$ или $u\neq v$ над термами, и список $SetTests$, содержащий предположения $t\in set$ или $t\notin set$ над удовлетворяющими множествами, сторона отсылает сообщение $snd$ как ответ и добавляет или убирает операторы над множествами и элементами множеств, указанные в списке $SetOperations$.

$step=iknows(rcv)\&CtrList\&SetTest\Rightarrow iknows(snd)\&SetOperations$

IF факты конвертируются в предположения над множествами. Шаг заключается в следующем: злоумышленнику дано знание $E$, заполненный список именованных множеств и базовая подстановка $\sigma$. Если $\sigma (rcv)\in Forge(E)$, если $\sigma (u)=\sigma (v)$ или $\sigma (s)\neq \sigma (t)$ для любых предположений $u=v$ или $u\neq t$ в $CtrList$ и если $\sigma (t)\in \sigma (set)$ (Соответственно, $\sigma (t)\notin \sigma (set)$) для любого теста $t\in set$ (Соответственно, $t\notin set$) в $SetTests$, тогда $\sigma (snd)$ добавляется в $E$ и все операции добавления или удаления в $SetOperations$ применяются по модулю $\sigma$.

Упрощение и оптимизация протоколов

Упрощение протокола уменьшает итоговый объем протокола. В частности число шагов, совмещая вместе как можно больше шагов или отмечая их к исполнению как наиболее ранние или наиболее поздние. Шаг, отмеченный к исполнению как наиболее ранний, будет выполнен как только выполнится его предок. CL-Atse может принимать решения по упрощению только будучи уверен, что это не уберет уязвимости протокола, т.е. если протокол скомпрометированный, то по крайней мере одна атака должна быть. Для обеспечения этого CL-Atse задает множества невыводимых для нарушителя термов (атомов, ключей и т.д.).

Способ анализа

CL-Atse выполняет протокол в каждой возможной последовательности шагов. Для того, что бы рассмотреть все возможные способы исполнения, алгоритм анализа полагается на 2 компонента: алгоритм объединения по модулю операций, таких как xor и экспонента, который предлагает все необходимые для каждого типа термов вычисления, и управление состояниями и предположениями при выполнении протокольного шага.

Ядро: выполнение протокольного шага

Целью данного модуля является выполнения протокольного шага на символьное системное состояние, добавляя новые предположения,сокращая их к элементарным предположениям, проверяя их правильность и т.д.

Сокращение гипотез: гипотеза $H(t)$ называется несокращенной, если $t$ не является переменной. Это полученное сообщение протокольного шага. Положим $s=(E\vartriangleright H(t)\vartriangleright F\vartriangleright e,td,set,\sigma )$ - системное состояние, где $t\notin Var$ и $F$ уже сокращено. Тогда мы сокращаем $H(t)$ в зависимости от $t$, переписывая правила $E\vartriangleright H(t)\vartriangleright F\vartriangleright e$ (и $\sigma$). Например:

$-E\vartriangleright H(u,v)\vartriangleright F\longrightarrow E\vartriangleright H(u)\vartriangleright H(v)\vartriangleright F$

Ссылки

• The CL-Atse Protocol Analyser. Mathieu Turuani. Frank Pfenning. 17th International Conference on Term Rewriting and Applications - RTA 2006, Aug 2006, Seattle, WA/USA, Springer, 4098, pp.277–286, 2006, Lecture Notes in Computer Science
• AVISPA Paper and Documentation