RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ЛИЧНЫЙ КАБИНЕТ
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2018, том 25, номер 6, страницы 589–606 (Mi mais651)  

Семантика, спецификация и верификация программ

Даже простые процессы $\pi$-исчисления трудны для анализа

М. М. Аббасa, В. А. Захаровbc

a Московский государственный университет им. М.В. Ломоносова, Ленинские горы, 1, г. Москва, 119991 Россия
b Национальный исследовательский университет «Высшая школа экономики», ул. Мясницкая, 20, г. Москва, 101000 Россия
c Институт системного программирования им. В.П. Иванникова РАН, ул. А. Солженицына, 25, 109004, г. Москва

Аннотация: Математические модели распределенных вычислений, построенные на основе исчисления мобильных процессов ($\pi$-исчисления), широко используются для проверки свойств информационной безопасности криптографических протоколов. Поскольку $\pi$-исчисление является полной по Тьюрингу моделью вычислений, эта задача в общем случае алгоритмически неразрешима. Поэтому ее исследование проводится лишь для некоторых специальных классов процессов $\pi$-исчисления с ограниченными вычислительными возможностями, например, для нерекурсивных процессов, в которых все вычисления имеют ограниченную длину, для процессов с ограниченным числом параллельных компонентов и др. Однако и в этих случаях предложенные разрешающие алгоритмы оказываются весьма трудоемкими. Мы полагаем, что это обусловлено самой природой процессов $\pi$-исчисления. Цель данной работы — показать, что даже для наиболее слабой модели пассивного противника и для сравнительно простых протоколов, в которых используются лишь базовые операции $\pi$-исчисления, задача проверки свойств информационной безопасности этих протоколов является co-NP-полной.

Ключевые слова: $\pi$-исчисление, протокол, безопасность, пассивный противник, верификация, сложность, NP-полнота.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 16-01-00714_а
18-01-00854_а
Работа выполнена при финансовой поддержке гранта РФФИ N 18-01-00854. Работа выполнена при финансовой поддержке гранта РФФИ N 16-01-00714.


DOI: https://doi.org/10.18255/1818-1015-589-606

Полный текст: PDF файл (526 kB)
Список литературы: PDF файл   HTML файл

Тип публикации: Статья
УДК: 517.9
Поступила в редакцию: 15.09.2018
Исправленный вариант: 30.10.2018

Образец цитирования: М. М. Аббас, В. А. Захаров, “Даже простые процессы $\pi$-исчисления трудны для анализа”, Модел. и анализ информ. систем, 25:6 (2018), 589–606

Цитирование в формате AMSBIB
\RBibitem{AbbZak18}
\by М.~М.~Аббас, В.~А.~Захаров
\paper Даже простые процессы $\pi$-исчисления трудны для анализа
\jour Модел. и анализ информ. систем
\yr 2018
\vol 25
\issue 6
\pages 589--606
\mathnet{http://mi.mathnet.ru/mais651}
\crossref{https://doi.org/10.18255/1818-1015-589-606}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais651
  • http://mi.mathnet.ru/rus/mais/v25/i6/p589

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:13
    Полный текст:3
    Литература:1

     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019