Автоматическая верификация протоколов

В 2005 г. появился новый программный продукт — AVISPA (Automated Validation of Internet Security Protocols and Applications) [1], разработанный в рамках международного проекта, в котором участвовали LORIA —INRIA (Франция), ЕТН (Цюрих, Швейцария),
Университет Генуи (Италия), Siemens AG (Германия). Судя по заявлениям его разработчиков, продукт AVISPA должен стать прорывом в области анализа криптопротоколов. Разработка данного средства рассматривается как единый европейский проект, реализуемый с участием многих ведущих институтов и организаций европейских стран. Он интегрирует различные современные подходы к анализу протоколов, такие как проверка на модели (model-checking), древовидные автоматы, временная логика. При этом используются разработки, созданные после 2000 г. Специально для него были разработаны версии языков LPSL ( igh-Level Protocols Specification Language) [2] и IF (Intermediate Format) [3], позволившие существенно расширить класс изучаемых протоколов, а также интегрировать в единую платформу сразу несколько различных методов.

Год: 2014
Город: Астана
Категория: Информатика