Vjylku

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)). Для читаемости множество предположений представляющих каждый экземпляр роли отображается в следующем синтаксисе:

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

Где σ{displaystyle 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∣Var∣Term.Term∣{Term}Terms∣{Term}Terma∣inv(Term)∣Term⊕Term∣Exp(Term,Product){displaystyle Term=Atommid Varmid Term.Termmid {Term}_{Term}^{s}mid {Term}_{Term}^{a}mid inv(Term)mid Termoplus Termmid Exp(Term,Product)}

Product=(Term)±1∣(Term)±1×Product{displaystyle Product=(Term)^{pm 1}mid (Term)^{pm 1}times Product}

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

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

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

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

State=Subst,Sets,ToDec,Knowns{displaystyle State=Subst,Sets,ToDec,Knowns}

ToDec=(Term,Term)∗{displaystyle ToDec=(Term,Term)^{*}}

Known=H(var)⊳Known∣D(Term)⊳Known∣e{displaystyle Known=H(var)vartriangleright Knownmid D(Term)vartriangleright Knownmid e}

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

Known=H(x)⊳H(y)⊳D({z}ks)⊳H(z)⊳D(a)⊳D(b)⊳e{displaystyle Known=H(x)vartriangleright H(y)vartriangleright D({z}_{k}^{s})vartriangleright H(z)vartriangleright D(a)vartriangleright D(b)vartriangleright e}

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

Протокольный шаг в CL-Atse представляет собой элементарное действие участника: при получении сообщения rcv{displaystyle rcv}, к которому приложены список CtrList{displaystyle CtrList}, содержащий предположения u=v{displaystyle u=v} или u≠v{displaystyle uneq v} над термами, и список SetTests{displaystyle SetTests}, содержащий предположения t∈set{displaystyle tin set} или t∉set{displaystyle tnotin set} над удовлетворяющими множествами, сторона отсылает сообщение snd{displaystyle snd} как ответ и добавляет или убирает операторы над множествами и элементами множеств, указанные в списке SetOperations{displaystyle SetOperations}.

step=iknows(rcv)&CtrList&SetTest⇒iknows(snd)&SetOperations{displaystyle step=iknows(rcv)&CtrList&SetTestRightarrow iknows(snd)&SetOperations}

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

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

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

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

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

Объединение по модулю (включая xor и экспоненту) |

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

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

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

−E⊳H(u,v)⊳F⟶E⊳H(u)⊳H(v)⊳F{displaystyle -Evartriangleright H(u,v)vartriangleright Flongrightarrow Evartriangleright 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