Protocol verification tools.pdf Приведем примеры средств автоматизированного анализа криптографических протоколов,которые в настоящее время можно отнести к наиболее эффективным, и рассмотримматематические аспекты работы этих систем. Подчеркнем, что данные средствапозволяют не только проверять заданные свойства протоколов, но и находитьконкретные атаки на протоколы в случае, когда эти свойства не выполнены. Посколькуинформация о конкретных механизмах работы этих систем не всегда доступна, топри их оценке будем опираться только на те сведения, которые опубликованы в печати.AV ISPAПрограммный продукт AVISPA появился в начале осени 2005 года. Разработка данногосредства проводилась в рамках единого европейского проекта, в котором участвовалиLORIA-INRIA (Франция), ETH Цюрих (Швейцария), университет г. Генуя (Италия),Siemens AG (Германия).Архитектура AVISPA допускает анализ протокола одним из четырех выходныхмодулей (TA4SP, SATMC, OFMC, CL-AtSe). Спецификация протокола, основаннаяна ролевом представлении, записывается на языке высокого уровня HLPSL, а затемтранслируется во внутренний язык IF. Проверяемые свойства записываются в терминахтемпоральной логики. Модуль TA4SP реализует технику, основанную на построениидревовидных автоматов и развитую для систем автоматического доказательства.Строится верхняя аппроксимация древовидного автомата, реализующего систему переписываниятермов, которая описывает максимальные знания нарушителя. Исследованиесвойства конфиденциальности теперь сводится к проверке наличия в этом множестветерма, содержащего секрет. Модули SATMC, OFMC, CL-AtSe осуществляютверификацию методом проверки на модели (model checking). Протокол представля-ется как бесконечная система переходов, а задача верификации сводится к проверкевыполнимости формулы, решения которой соответствуют атакам на протокол. Длясведения к конечному случаю применяются разные подходы. В модуле SATMC используютсяметоды, разработанные в рамках теории решения задач планирования,в модуле OFMC - символический метод, позволяющий группировать различные состоянияв бесконечные классы, а в CL-AtSe - применяется техника, основанная напостроении ограничений.С помощью AVISPA проанализировано большинство протоколов, встречающихсяв документах IETF. Полная информация о разработке и публикациях, лежащих в егооснове, а также исполняемый программный код этого средства вместе с удобной графическойоболочкой SPAN доступны на интернет-сайте http://www.avispa-project.org.ScytherСоздан в ETH (Цюрих). Верифицирует ограниченное и неограниченное число сеансовпротокола. Использует символический анализ в сочетании с обратным поиском, основанныйна частично упорядоченных шаблонах. Scyther не требует задания сценарияатаки. Он требует только задания параметров, ограничивающих либо максимальноечисло запусков, либо пространства перебираемых траекторий. В первом случае всегдадает результат и показывает найденные траектории атаки. Во втором случае завершениене гарантировано. В качестве ответа возможна одна из трех ситуаций: установлено,что проверяемое свойство выполнено; свойство не выполнено, так как найдена атака;свойство может быть корректно для заданного пространства траекторий.HERME SРазработан лабораторией VERIMAG из IMAG (Франция) в рамках объединенногопроекта EVA и PROUVE. Использует язык LaEva верхнего уровня для задания спецификацийпротоколов и их свойств, аналогичный языку HLPSL. Затем этот языктранслируется во внутреннее представление на языке cpl, которое является общимязыком для нескольких продуктов, таких, как Securify, Cpv и HERMES.Позволяет проверять свойства протокола при неограниченной длине сообщения инеограниченном числе участников. Дает на выходе условия на исходные знания противника,которые гарантируют, что он не сможет узнать секрета. HERMES не оцениваетзнания нарушителя, а исследует множество безопасных сообщений. Для аппроксимациибесконечного множества сообщений используется символическое представление,основанное на шаблонах. Если в результате найдена атака, то предоставляеттраекторию атаки. В случае, когда в результате получается ответ, что свойстводоказано, выдает также дерево полного доказательства, что бывает полезным присертификации протокола. Доступен в интерактивном онлайновом режиме на сайтеhttp://www.rverimag.imag.fr/~async/hermes/.P r oV e rifРазработан в рамках проекта, финасируемого INRIA (Франция). Анализируетнеограниченное число сеансов протокола с использованием верхней аппроксимации ипредставления протокола с помощью хорновских выражений. ProVerif предлагает дватипа входных файлов: хорновские выражения и подмножество Pi-исчисления. Прииспользовании Pi-исчисления ProVerif основывается на описании множества процессов,каждый из которых может выполняться неограниченное число раз. На выходевозможны четыре ситуации: свойство не выполнено; доказано, что свойство выполнено;свойство не может быть доказано, так как есть пример атаки (могут быть найденыложные атаки); работа не завершается. ProVerif корректно моделирует множество траекторий, соответствующих определенному сценарию, и осуществляет полный переборвозможных траекторий. Исходный код доступен по адресу http://www.proverif.ens.fr/.

Скачать электронную версию публикации