1.Алгебра процессов 2.Мультимножественная подстановка 3.Конечные автоматы 4.Модальные логики 5.Сети Петри 6.Графическое моделирование Методы формальной спецификации

Алгебры процессов (PA - Process algebras) - известная рамочная концепция, которая представляет семейство исчислений для описания распределенных и параллельных систем. Для описания свойств безопасности применяются расширения известных алгебр процессов: CCS (Calculus of Communicating Systems) R. Milner. Communication and Concurrency. Prentice-Hall, 1989 CSP (Communicating sequential processes) C. A. R. Hoare. Communicating sequential processes. In R. M. McKeag and A. M. Такие исчисления к протоколам защиты опирается на множества примитивов, которые выражаются в терминах языка алгебры процессов. Язык PA определяется следующей грамматикой: Parallel processes Q ::= 0 | Q || P | Q || !P Sequential processes P ::= 0 | a(t).P | (t).P | [t = t ] P | νn.P Параллельные процессы определяются как параллельная композиция, возможно дублированных, последовательных процессов. Последовательные процессы передают сообщения t через каналы: выводящий процесс (t).P готов послать кортеж термов t через канал a; принимающий процесс a(t). P готов принять кортеж сообщений, соответствующих форматам t. Запись [t = t ] P означает, что для того чтобы процесс P продолжался, необходимо, чтобы термы t и t совпадали. Создание нового процесса записывается как νn.P. Множество c(t). это множество констант, появляющихся в терме t, c(Q) это множество констант процесса Q

Первый вывод (реакция) показывает, как два последовательных процесса, соответственно, один готов совершить вывод термов t, другой готов совершить ввод термов t, реагируют, если унификация возможна между t и t. Второй вывод (репликация) говорит, что !P есть по существу фабрика процессов P. Следующие выводы описывают соответственно, рефлексивность перехода, генерацию нового имени, семантику совпадения и транзитивность отношения переходов. Алгебры процессов Операционная семантика дается следующими установками: Single interaction Q Q ; Iterated interaction Q * Q Они определяются следующим образом:

Протоколы как процессы. Протоколы защиты могут быть описаны с помощью некоторого подмножества языка PA, где каждое взаимодействие происходит через сеть (Pnet - процесс, управляющий сетью как открытым каналом, где каждый Pρ посылает и принимает сообщения). В системе присутствует злоумышленник с некоторыми начальными знаниями (Q !I с начальными знаниями Q I0 ), способный перехватывать и фальсифицировать сообщения передаваемые по сети. Каждый принципал стартует протокол, играя некоторую роль ρ. Протокол защиты, включающий набор ролей ρ, выражается в подмножестве языка PA как процесс Q0, определяемый параллельной композицией, состоящей из пяти компонентов: Алгебры процессов P net || Π P! P ρ || Q !I || Q I0 || Q !π где Π P означает параллельную композицию всех процессов в P, а именно:

Алгебры процессов Все агенты, участвующие в протоколе, включая взаимодействующих принципалов и злоумышленника, описываются в терминах CSP. Этот метод подходит для формализации сообщений, трасс, злоумышленников и т.п. Для верификации используется инструмент FDR (Failures Divergences Refinement checker. анализатор моделей для CSP), который является универсальным инструментом для установления того, что реализация уточняет спецификацию. Лоу (Lowe) продемонстрировал применение алгебры процессов CSP и универсального анализатора моделей FDR к криптографическому протоколу. G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proc. TACAS, (1996) , Springer Verlag.

Spi-исчисление. Абади (Abadi) и Гордон (Gordon) в предложили Spi, исчисление для описания криптографических протоколов на абстрактном уровне. Расширили π-исчисление, алгебру мобильных процессов, с тем, чтобы промоделировать некоторые свойства криптографических протоколов. Назначение π-исчисление разработано для описания примитивных коммуникационных каналов. Spi-исчисление дает возможность явно представлять применение криптографии в протоколах. Доказательство безопасности протокола устанавливается через проверку эквивалентности между двумя процессами двух различных принципалов, взаимодействующих друг с другом. Злоумышленник явно не моделируется, и в этом состоит главное преимущество этого подхода. Вместо этого злоумышленник представляется как процесс Spi-исчисления. Алгебры процессов R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (Parts I and II). Information and Computation, 100:1-77, 1992 M. Abadi and A. D. Gordon. A Calculus for Cryptographic Protocols: The Spi Calculus. In Proc. Fourth ACM Conference on Computer and Communications Security. ACM Press, April 1997

Security Process Algebra. SPA (Security Process Algebra). Алгебры процессов R. Focardi, R. Gorrieri, Classification of Security Properties (Part I: Information Flow), in: R. Focardi, R. Gorrieri (Eds.), Foundations of Security Analysis and Design, Vol of LNCS, Springer-Verlag, 2001 Выражает концепции невлияния (Noninterference) и является вариантом алгебры процессов CCS (Milner.s Calculus of Communicating Systems) SPA предназначено для изучения свойств безопасности информационного потока на основе бисимуляции. Свойство Bisimulation-based non Deducibility on Compositions (BNDC): система обладает свойством BNDC, если пользователь низкого уровня не наблюдает модифицирование системы (в смысле бисимуляционной семантики) при выполнении любого процесса высокого уровня. R. Focardi, R. Gorrieri, A Classification of Security Properties for Process Algebras, Journal of Computer Security 3 (1) (1994/1995)

Алгебры процессов 1. С целью специфицировать многоуровневые системы множество наблюдаемых воздействий разделяется на два множества: высокого уровня и низкого уровня. 2. Синтаксис SPA основан на элементах CCS: множество =I O, где I = {a,b,…}. это множество входных воздействий, O = - это множество выходных воздействий, специальное воздействие τ моделирует внутренние вычисления, т.е. ненаблюдаемые извне, а также дополнительная функция (¯) :, такая что. Act = L {τ}. множество всех воздействий. 3. Множество наблюдаемых воздействий разделяется на два множества. H и L, высокого и низкого уровня соответственно. Выражения SPA: E ::= 0 | a.E | E + E | E||E | E\v | E[f] | Z, где a Act, v, E + E - недетерминированный выбор, E||E - параллельная композиция, E\v - ограничение, E[f] - переразметка (relabeling), Z - константа. Вводится E - набор всех SPA процессов, E H. процессы высокого уровня, т.е. процессы, использующие воздействия из H {τ}. Основные принципы SPA

Алгебры процессов Операционная семантика SPA 1. Операционная семантика SPA дается в терминах системы размеченных переходов (LTS. Labeled Transition Systems). LTS описывается триплетом (S, A, ), где S - множество состояний, A - множество разметок (воздействий), S × A × S - множество размеченных переходов. Нотация или S1 S2 означает, что система может перейти из состояния S1 в состояние S2 вследствие воздействия a. 2. Применяется концепция наблюдаемой эквивалентности (observation equivalence) для того, чтобы установить соотношения равенства между процессами. Две системы имеют одинаковую семантику тогда и только тогда, когда внешний наблюдатель не может их различить. Согласно отношению слабой бисимуляции (weak bisimulation) [Mil89], два процесса считаются равными, если их наблюдаемое поведение совпадает на каждом шаге выполнения. [Mil89] R. Milner. Communication and Concurrency. Prentice-Hall, 1989 главное преимущество BNDC по отношению к свойствам безопасности, основанных на трассах, состоит в том, что оно более мощное и позволяет обнаруживать информационные потоки, которые позволяют злоумышленным процессам высокого уровня блокировать или разблокировать систему. При этом такая система, построенная на основе трасс, будет считаться безопасной, и в ней нельзя обнаружить скрытые каналы. Свойства Noninterference обеспечивают формальное определение безопасности информационного потока, поэтому это свойство полезно для понимания безопасности систем и сетей

Security Process Language. F. Crazzolara and G. Winskel. Petri nets in cryptographic protocols. In Proc. 16th International Parallel & Distributed Processing Symposium - 6th International Workshop on Formal methods for Parallel Programming: Theory and Practice, San Francisco, April IEEE Press. Алгебры процессов SPL - язык процессов для протоколов защиты с семантикой в терминах множеств событий. Основной принцип SPL: Процесс представляется в виде множества событий, и т.к. каждое событие сопровождается наборами пред- и постусловий, это представление может быть описано как сеть Петри. В терминах сетей Петри правила Паульсона соответствуют определенному виду событий, где и сетевые, и управляющие условия являются постоянными условиями. В действительности, одиночные процессы, компоненты системы, можно рассматривать как стренды, и приведенные доказательства используют их, в основном, в этом смысле. Стренды, в свою очередь, близки к структурам событий. Для сетей с постоянными условиями, может быть доказано, что они соответствуют безопасным сетям. Приведенная в работе семантика сетей Петри описывается в соответствующем разделе Сети Петри. Расширение π-исчисления. В работе продемонстрировано использование анализа потока управления для исследования введения свойств безопасности модели Bell-LaPadula в π-исчисление. F. Thayer Fabrega, J. Herzog, and J. Guttman. Strand spaces: Why is a security protocol correct. In Proc IEEE Symposium on Security and Privacy, pp IEEE Computer Society Press, May 1998 C. Bodei, P. Degano, F. Nielson, and H. R. Nielson. Static analysis for the п-calculus with applications to security. Information and Computation, vol. 168, pp , 2001

Мультимножественная подстановка MSR. Multiset Rewriting основана на теории параллельных процессов и логике подстановок. Область применения: изучение фундаментальных вопросов протоколов защиты. Он также играет практическую роль в качестве языка промежуточного уровня CIL в системе для анализа протоколов CASPL. G. Denker, J. Millen, and H. Ruess. The CAPSL integrated protocol environment. Technical Report SRI-CSL , SRI International, Язык мультимножественной подстановки MSR первого порядка определяется следующей грамматикой: Elements Rewriting Rules Rule sets Элементы мультимножеств выбираются как атомарные формулы a(t) для термов t = (t1,.,tn) над некоей сигнатурой Σ первого порядка. Записывается (x) и, соответственно, t(x), чтобы подчеркнуть, что переменные из x появляются в мультимножестве (и соответственно в терме t). Символ "," означает объединение мультимножеств, которое неявно рассматривается как коммутативное и ассоциативное, в то время как " " означает пустое мультимножество, которое действует как нейтральный элемент, разрешающий покидать его, когда это удобно.

Операционная семантика MSR выражается следующими установками: Мультимножественная подстановка Single rule application Iterated rule application Мультимножества и называются состояниями и всегда являются основными формулами. Стрелка означает переход. Эти установки определяются следующим образом: Первый вывод показывает, как используется правило подстановки r = (x) n. (x,n) для преобразования состояния в последующее состояние: находится основной экземпляр (t) предшественника, и он замещается экземпляром (t, k), где k. это новые константы. Здесь [t/x] означает подстановку, замещающую каждое появление переменной x в x с соответствующим термом t в t. Эти правила реализуют недетерминированную, но последовательную вычислительную модель (одно правило за раз). Параллельность улавливается через перестановочность (permutability) некоторых применяемых правил. В остальных правилах * определяется как рефлексивное и транзитивное замыкание.

Протоколы как мультимножественная подстановка. Мультимножественная подстановка Язык MSR опирается наследующие предикатные символы: I. Cervesato, N. A. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov. Relating strands and multiset rewriting for security protocol analysis. In Proc. of the 13th IEEE Computer Security Foundations Workshop (CSFW '00), pp IEEE, Сетевые сообщения (Ñ) - это предикаты для моделирования сети, где N(t) означает, что t располагается в сети. Состояния ролей (Ã ). это предикаты для моделирования ролей. Пусть множество идентификаторов ролей есть R = { ρ 1,., ρ n }, тогда семейство предикатов состояний ролей {A ρi (t) : i = 0.l ρ }, предназначено для хранения внутреннего состояния, t, принципала в роли ρ R во время выполнения шагов протокола. Поведение каждой роли ρ описывается через конечное число правил, индексированных от 0 до l ρ. Злоумышленник ( Ĩ). это предикаты для моделирования злоумышленника I, где I(t) означает, что злоумышленник знает сообщение t. Постоянные предикаты ( ˜ ) - это базовые предикаты для хранения данных, которыене изменяются во время разворачивания протокола. Правила используют эти предикаты для доступа к значениям постоянных данных. π

представляются как множество правил подстановок специального формата, называемого теорией протоколов защиты. Если R -это множество ролей, тогда можно записать, что = ρ R ( ρ ), I, где ρ и I описывает поведение роли ρ R и злоумышленника I. Для каждой роли ρ, правила в ρ состоят из:. правила с одной конкретизацией r ρ0 : (x) n.A ρ0 (n; x), (x). нуль или больше (i = 1 … l ρ ) правил обмена сообщениями: send r ρi : A ρi- 1 (x) A ρi (x), N(t(x)) receive r ρi : A ρi-1 (x), N(t(x,y)) A ρi (x, y) Протокол защиты выражается в языке MSR r ˜ r ˜ r ˜ r ˜ r ˜ r ˜ r ˜ π ˜ π ˜ Правила в I являются стандартными правилами, описывающими злоумышленника в стиле Dolev-Yao, чьи способности состоят в перехвате, анализировании, синтезировании и создании сообщений с возможностью доступа к долговременным данным. r ˜