TA4SP
Ошибка скрипта: Модуля «Unsubst» не существует.
TA4SP (Tree Automata based on Automatic Approximations for the Analysis of Security Protocols) - инструмент доказательства свойств секретности протоколов безопасности, который позволяет производить доказательства при неограниченном числе сессий. Входит в состав проекта Avispa.
Описание модуля TA4SP[1][править]
Модуль TA4SP вычисляет для заданного начального состояния как верхнюю, так и нижнюю аппроксимацию знаний нарушителя с помощью правил переписывания с применением техники аппроксимации древовидных автоматов (языков) при неограниченном числе сессий.
TA4SP использует библиотеку древовидных автоматов Timbuk 2.0, созданную Th. Genet IRISA, Rennes France.
Верхняя оценка может привести к реальному доказательству проверяемого свойства безопасности для изучаемого протокола при неограниченном числе сессий.
В противном случае, в контексте верхней аппроксимацииTA4SP может только делать вывод, что свойство конфиденциальности выполняется только для данного начального состояния.
При нижней аппроксимации без каких-либо абстракций средство может показать, что протокол не удовлетворяет данному свойству безопасности.
Для проверки протокола с помощью TA4SP применяется следующая эмпирическая стратегия.
- Пользователь вычисляет верхнюю оценку и проверяет свойство безопасности.
- Если первый шаг не позволяет сделать вывод о выполнении свойства безопасности, то пользователь вычисляет нижнюю оценку до тех пор, пока не будет получена атака в приемлемое время. Однако эта эмпирическая стратегия не всегда приводит к ожидаемому результату.
Промежуточный результат на основе верхнего оценивания не позволяет сделать вывод, что атака действительно существует.
Сочетает преимущества систем автоматического доказательства теорем с формальной абстрактной интерпретацией, называемой аппроксимацией.
Обладает многими важными для практики свойствами:
- не требуется завершение работы систем переписывания;
- системы переписывания могут включать АС-символы;
- доказательства получаются с помощью выполнения операции пересечения с аппроксимирующим автоматом TR↑(A0) (что быстро выполняется в автоматическом режиме);
- построение TR↑(A0) также выполняется автоматически, монотонно, причём можно гарантировать его завершение при подходящем выборе аппроксимационной функции γ.
Параметры TA4SP[2][править]
При запуске инструмента пользователь может использовать следующие параметры (их можно установить в файле конфигурации ta4sp.config):
- Модель проверки (abstractions=<boolean> в файле ta4sp.config). Если этот параметр установлен в значение true, то будет смоделирована ситуация с участием только двух агентов (нарушитель и честный агент), что позволяет улучшить время вычислений.
- Знания нарушителя (level=<integer> в файле ta4sp.config). Значение этого параметра соответствует глубине обхода дерева состояний автомата. Если значение параметра равно 0, то будет построена верхняя аппроксимация знаний нарушителя.
Примечания[править]
- ↑ Страница Модуль:Citation/CS1/styles.css не имеет содержания.Шаблон:±. КРИПТОГРАФИЧЕСКИЕ ПРОТОКОЛЫ: ОСНОВНЫЕ СВОЙСТВА И УЯЗВИМОСТИ. — Изд. центр «Академия», 2009.
- ↑ AVISPA v1.1 User Manual
Литература[править]
Шаблон:Ambox Шаблон:Сортировка: изолированные статьиОшибка скрипта: Модуля «Unsubst» не существует.
This article "TA4SP" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:TA4SP. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.
