TA4SP

TA4SP (Tree Automata based on Automatic Approximations for the Analysis of Security Protocols) - инструмент доказательства свойств секретности протоколов безопасности, который позволяет производить доказательства при неограниченном числе сессий. Входит в состав проекта Avispa.

Описание модуля TA4SP

Модуль TA4SP вычисляет для заданного начального состояния как верхнюю, так и нижнюю аппроксимацию знаний нарушителя с помощью правил переписывания с применением техники аппроксимации древовидных автоматов (языков) при неограниченном числе сессий.

TA4SP использует библиотеку древовидных автоматов Timbuk 2.0, созданную Th. Genet IRISA, Rennes France.

Верхняя оценка может привести к реальному доказательству проверяемого свойства безопасности для изучаемого протокола при неограниченном числе сессий.

В противном случае, в контексте верхней аппроксимацииTA4SP может только делать вывод, что свойство конфиденциальности выполняется только для данного начального состояния.

При нижней аппроксимации без каких-либо абстракций средство может показать, что протокол не удовлетворяет данному свойству безопасности.

Для проверки протокола с помощью TA4SP применяется следующая эмпирическая стратегия.

1. Пользователь вычисляет верхнюю оценку и проверяет свойство безопасности.
2. Если первый шаг не позволяет сделать вывод о выполнении свойства безопасности, то пользователь вычисляет нижнюю оценку до тех пор, пока не будет получена атака в приемлемое время. Однако эта эмпирическая стратегия не всегда приводит к ожидаемому результату.

Промежуточный результат на основе верхнего оценивания не позволяет сделать вывод, что атака действительно существует.

Сочетает преимущества систем автоматического доказательства теорем с формальной абстрактной интерпретацией, называемой аппроксимацией.

Обладает многими важными для практики свойствами:

• не требуется завершение работы систем переписывания;
• системы переписывания могут включать АС-символы;
• доказательства получаются с помощью выполнения операции пересечения с аппроксимирующим автоматом TR↑(A0) (что быстро выполняется в автоматическом режиме);
• построение TR↑(A0) также выполняется автоматически, монотонно, причём можно гарантировать его завершение при подходящем выборе аппроксимационной функции γ.

Параметры TA4SP

При запуске инструмента пользователь может использовать следующие параметры (их можно установить в файле конфигурации ta4sp.config):

1. Модель проверки (abstractions=<boolean> в файле ta4sp.config). Если этот параметр установлен в значение true, то будет смоделирована ситуация с участием только двух агентов (нарушитель и честный агент), что позволяет улучшить время вычислений.
2. Знания нарушителя (level=<integer> в файле ta4sp.config). Значение этого параметра соответствует глубине обхода дерева состояний автомата. Если значение параметра равно 0, то будет построена верхняя аппроксимация знаний нарушителя.