Розширення моделі типізованої специфікації для формального аналізу криптографічних протоколів

Abstract

У статті розглянуті основи формального аналізу протоколів, властивості безпеки протоколів та модель типізованої специфікації для формального аналізу. Оскільки складність криптографічних систем росте та протоколи вже не можна розглядати уособлено, без урахування контексту, у якому вони виконуються, ми розширюємо модель типізованої спеціфікації таким чином, що стає можливим проводити аналіз суттєво інших протоколів. Як приклад, буде розглянуто, як за допомогою розширеної моделі вдається знайти атаки на протокол Нідхема-Шредера з симетричним ключем.