Поиск упрощенной модели протоколов инфраструктуры цифровой подписи с использованием верификаторов моделей

Важнейшим способом повышения безопасности информационных систем, использующих криптографические методы защиты информации, является эффективная декомпозиция кода криптографических сервисов на программные модули. Под эффективной декомпозицией понимается: 1) изоляция программных модулей разной степени критичности (т.е. имеющих разную степень опасности последствий от ошибок или программных закладок) друг от друга; 2) применимость одних и тех же программных модулей без модификации (и, как следствие, повторной верификации) в различных криптографических сервисах; 3) получение компактных, детерминированных, криптографически полных упрощенных моделей программных модулей. Одним из возможных подходов к решению проблемы эффективной декомпозиции является предварительный анализ набора протоколов, реализующих криптографический сервис, в рамках т.н. UC-моделей. В настоящей статье рассмотрена проблема декомпозиции криптографического сервиса “Цифровая подпись на базе PKI” в рамках указанного подхода и исследована возможность частичной автоматизации процедуры поиска его упрощенной модели с использованием верификатора моделей NuSMV.