Поиск упрощенной модели протоколов инфраструктурыцифровой подписи с использованием верификаторов моделей | Прикладная дискретная математика. 2009. № 1(3).

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